Home | Metamath
Proof Explorer Theorem List (p. 328 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | welb 32701* | A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 We 𝐴 ∧ (𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → (◡𝑅 Or 𝐵 ∧ ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))) | ||
Theorem | supex2g 32702 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ 𝐶 → sup(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | supclt 32703* | Closure of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Or 𝐴 ∧ ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supubt 32704* | Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Or 𝐴 ∧ ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | filbcmb 32705* | Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦 ≤ 𝑧 → 𝜑) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦 ≤ 𝑧 → ∀𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | rdr 32706 | Two ways of expressing the remainder when 𝐴 is divided by 𝐵. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) = (⌊‘(𝐴 / 𝐵))) | ||
Theorem | fzmul 32707 | Membership of a product in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (𝐽 ∈ (𝑀...𝑁) → (𝐾 · 𝐽) ∈ ((𝐾 · 𝑀)...(𝐾 · 𝑁)))) | ||
Theorem | sdclem2 32708* | Lemma for sdc 32710. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏)) & ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) & ⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) & ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} & ⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) & ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐺:𝑍⟶𝐽) & ⊢ (𝜑 → (𝐺‘𝑀):(𝑀...𝑀)⟶𝐴) & ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺‘𝑤))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) | ||
Theorem | sdclem1 32709* | Lemma for sdc 32710. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏)) & ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) & ⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) & ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} & ⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) | ||
Theorem | sdc 32710* | Strong dependent choice. Suppose we may choose an element of 𝐴 such that property 𝜓 holds, and suppose that if we have already chosen the first 𝑘 elements (represented here by a function from 1...𝑘 to 𝐴), we may choose another element so that all 𝑘 + 1 elements taken together have property 𝜓. Then there exists an infinite sequence of elements of 𝐴 such that the first 𝑛 terms of this sequence satisfy 𝜓 for all 𝑛. This theorem allows us to construct infinite seqeunces where each term depends on all the previous terms in the sequence. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 3-Jun-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏)) & ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) & ⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) | ||
Theorem | fdc 32711* | Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice. (Contributed by Jeff Madsen, 18-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ 𝑀 ∈ ℤ & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒)) & ⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏)) & ⊢ (𝜂 → 𝐶 ∈ 𝐴) & ⊢ (𝜂 → 𝑅 Fr 𝐴) & ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑)) & ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎) ⇒ ⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) | ||
Theorem | fdc1 32712* | Variant of fdc 32711 with no specified base value. (Contributed by Jeff Madsen, 18-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ 𝑀 ∈ ℤ & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (𝑎 = (𝑓‘𝑀) → (𝜁 ↔ 𝜎)) & ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒)) & ⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏)) & ⊢ (𝜂 → ∃𝑎 ∈ 𝐴 𝜁) & ⊢ (𝜂 → 𝑅 Fr 𝐴) & ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑)) & ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎) ⇒ ⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) | ||
Theorem | seqpo 32713* | Two ways to say that a sequence respects a partial order. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) → (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ↔ ∀𝑚 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛))) | ||
Theorem | incsequz 32714* | An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ≥‘𝐴)) | ||
Theorem | incsequz2 32715* | An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ (ℤ≥‘𝐴)) | ||
Theorem | nnubfi 32716* | A bounded above set of positive integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.) |
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) → {𝑥 ∈ 𝐴 ∣ 𝑥 < 𝐵} ∈ Fin) | ||
Theorem | nninfnub 32717* | An infinite set of positive integers is unbounded above. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.) |
⊢ ((𝐴 ⊆ ℕ ∧ ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ ℕ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅) | ||
Theorem | subspopn 32718 | An open set is open in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ∈ (𝐽 ↾t 𝐴)) | ||
Theorem | neificl 32719 | Neighborhoods are closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Nov-2013.) |
⊢ (((𝐽 ∈ Top ∧ 𝑁 ⊆ ((nei‘𝐽)‘𝑆)) ∧ (𝑁 ∈ Fin ∧ 𝑁 ≠ ∅)) → ∩ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | lpss2 32720 | Limit points of a subset are limit points of the larger set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((limPt‘𝐽)‘𝐵) ⊆ ((limPt‘𝐽)‘𝐴)) | ||
Theorem | metf1o 32721* | Use a bijection with a metric space to construct a metric on a set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑁 = (𝑥 ∈ 𝑌, 𝑦 ∈ 𝑌 ↦ ((𝐹‘𝑥)𝑀(𝐹‘𝑦))) ⇒ ⊢ ((𝑌 ∈ 𝐴 ∧ 𝑀 ∈ (Met‘𝑋) ∧ 𝐹:𝑌–1-1-onto→𝑋) → 𝑁 ∈ (Met‘𝑌)) | ||
Theorem | blssp 32722 | A ball in the subspace metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jan-2014.) |
⊢ 𝑁 = (𝑀 ↾ (𝑆 × 𝑆)) ⇒ ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+)) → (𝑌(ball‘𝑁)𝑅) = ((𝑌(ball‘𝑀)𝑅) ∩ 𝑆)) | ||
Theorem | mettrifi 32723* | Generalized triangle inequality for arbitrary finite sums. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐹‘𝑀)𝐷(𝐹‘𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) | ||
Theorem | lmclim2 32724* | A sequence in a metric space converges to a point iff the distance between the point and the elements of the sequence converges to 0. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)𝐷𝑌)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑌 ↔ 𝐺 ⇝ 0)) | ||
Theorem | geomcau 32725* | If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 < 1) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵↑𝑘))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) | ||
Theorem | caures 32726 | The restriction of a Cauchy sequence to an upper set of integers is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm ℂ)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ↾ 𝑍) ∈ (Cau‘𝐷))) | ||
Theorem | caushft 32727* | A shifted Cauchy sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝑁)) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘(𝑘 + 𝑁))) & ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) & ⊢ (𝜑 → 𝐺:𝑊⟶𝑋) ⇒ ⊢ (𝜑 → 𝐺 ∈ (Cau‘𝐷)) | ||
Theorem | constcncf 32728* | A constant function is a continuous function on ℂ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved into main set.mm as cncfmptc 22522 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐴) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | idcncf 32729 | The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 22523 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝑥) ⇒ ⊢ 𝐹 ∈ (ℂ–cn→ℂ) | ||
Theorem | sub1cncf 32730* | Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐴)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | sub2cncf 32731* | Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 − 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | cnres2 32732* | The restriction of a continuous function to a subset is continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐾 ↾t 𝐵))) | ||
Theorem | cnresima 32733 | A continuous function is continuous onto its image. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝐽 Cn (𝐾 ↾t ran 𝐹))) | ||
Theorem | cncfres 32734* | A continuous function on complex numbers restricted to a subset. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐴 ⊆ ℂ & ⊢ 𝐵 ⊆ ℂ & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) & ⊢ 𝐹 ∈ (ℂ–cn→ℂ) & ⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) & ⊢ 𝐾 = (MetOpen‘((abs ∘ − ) ↾ (𝐵 × 𝐵))) ⇒ ⊢ 𝐺 ∈ (𝐽 Cn 𝐾) | ||
Syntax | ctotbnd 32735 | Extend class notation with the class of totally bounded metric spaces. |
class TotBnd | ||
Syntax | cbnd 32736 | Extend class notation with the class of bounded metric spaces. |
class Bnd | ||
Definition | df-totbnd 32737* | Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))}) | ||
Theorem | istotbnd 32738* | The predicate "is a totally bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
Theorem | istotbnd2 32739* | The predicate "is a totally bounded metric space." (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ (Met‘𝑋) → (𝑀 ∈ (TotBnd‘𝑋) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
Theorem | istotbnd3 32740* | A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) | ||
Theorem | totbndmet 32741 | The predicate "totally bounded" implies 𝑀 is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Met‘𝑋)) | ||
Theorem | 0totbnd 32742 | The metric (there is only one) on the empty set is totally bounded. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ (𝑋 = ∅ → (𝑀 ∈ (TotBnd‘𝑋) ↔ 𝑀 ∈ (Met‘𝑋))) | ||
Theorem | sstotbnd2 32743* | Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) | ||
Theorem | sstotbnd 32744* | Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
Theorem | sstotbnd3 32745* | Use a net that is not necessarily finite, but for which only finitely many balls meet the subset. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ 𝒫 𝑋(𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ∧ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ≠ ∅} ∈ Fin))) | ||
Theorem | totbndss 32746 | A subset of a totally bounded metric space is totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ ((𝑀 ∈ (TotBnd‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (TotBnd‘𝑆)) | ||
Theorem | equivtotbnd 32747* | If the metric 𝑀 is "strongly finer" than 𝑁 (meaning that there is a positive real constant 𝑅 such that 𝑁(𝑥, 𝑦) ≤ 𝑅 · 𝑀(𝑥, 𝑦)), then total boundedness of 𝑀 implies total boundedness of 𝑁. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is totally bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ (𝜑 → 𝑀 ∈ (TotBnd‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦))) ⇒ ⊢ (𝜑 → 𝑁 ∈ (TotBnd‘𝑋)) | ||
Definition | df-bnd 32748* | Define the class of bounded metrics. A metric space is bounded iff it can be covered by a single ball. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ Bnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)}) | ||
Theorem | isbnd 32749* | The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | ||
Theorem | bndmet 32750 | A bounded metric space is a metric space. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 ∈ (Met‘𝑋)) | ||
Theorem | isbndx 32751* | A "bounded extended metric" (meaning that it satisfies the same condition as a bounded metric, but with "metric" replaced with "extended metric") is a metric and thus is bounded in the conventional sense. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | ||
Theorem | isbnd2 32752* | The predicate "is a bounded metric space". Uses a single point instead of an arbitrary point in the space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟))) | ||
Theorem | isbnd3 32753* | A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))) | ||
Theorem | isbnd3b 32754* | A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦𝑀𝑧) ≤ 𝑥)) | ||
Theorem | bndss 32755 | A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (Bnd‘𝑆)) | ||
Theorem | blbnd 32756 | A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 15-Jan-2014.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ) → (𝑀 ↾ ((𝑌(ball‘𝑀)𝑅) × (𝑌(ball‘𝑀)𝑅))) ∈ (Bnd‘(𝑌(ball‘𝑀)𝑅))) | ||
Theorem | ssbnd 32757* | A subset of a metric space is bounded iff it is contained in a ball around 𝑃, for any 𝑃 in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ (Bnd‘𝑌) ↔ ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑))) | ||
Theorem | totbndbnd 32758 | A totally bounded metric space is bounded. This theorem fails for extended metrics - a bounded extended metric is a metric, but there are totally bounded extended metrics that are not metrics (if we were to weaken istotbnd 32738 to only require that 𝑀 be an extended metric). A counterexample is the discrete extended metric (assigning distinct points distance +∞) on a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Bnd‘𝑋)) | ||
Theorem | equivbnd 32759* | If the metric 𝑀 is "strongly finer" than 𝑁 (meaning that there is a positive real constant 𝑅 such that 𝑁(𝑥, 𝑦) ≤ 𝑅 · 𝑀(𝑥, 𝑦)), then boundedness of 𝑀 implies boundedness of 𝑁. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ (𝜑 → 𝑀 ∈ (Bnd‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦))) ⇒ ⊢ (𝜑 → 𝑁 ∈ (Bnd‘𝑋)) | ||
Theorem | bnd2lem 32760 | Lemma for equivbnd2 32761 and similar theorems. (Contributed by Jeff Madsen, 16-Sep-2015.) |
⊢ 𝐷 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝐷 ∈ (Bnd‘𝑌)) → 𝑌 ⊆ 𝑋) | ||
Theorem | equivbnd2 32761* | If balls are totally bounded in the metric 𝑀, then balls are totally bounded in the equivalent metric 𝑁. (Contributed by Mario Carneiro, 15-Sep-2015.) |
⊢ (𝜑 → 𝑀 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝑆 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑀𝑦) ≤ (𝑆 · (𝑥𝑁𝑦))) & ⊢ 𝐶 = (𝑀 ↾ (𝑌 × 𝑌)) & ⊢ 𝐷 = (𝑁 ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝑌) ↔ 𝐶 ∈ (Bnd‘𝑌))) ⇒ ⊢ (𝜑 → (𝐷 ∈ (TotBnd‘𝑌) ↔ 𝐷 ∈ (Bnd‘𝑌))) | ||
Theorem | prdsbnd 32762* | The product metric over finite index set is bounded if all the factors are bounded. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘(𝑅‘𝑥)) & ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Bnd‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (Bnd‘𝐵)) | ||
Theorem | prdstotbnd 32763* | The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘(𝑅‘𝑥)) & ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (TotBnd‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (TotBnd‘𝐵)) | ||
Theorem | prdsbnd2 32764* | If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘(𝑅‘𝑥)) & ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) ⇒ ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴))) | ||
Theorem | cntotbnd 32765 | A subset of the complex numbers is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋)) | ||
Theorem | cnpwstotbnd 32766 | A subset of 𝐴↑𝐼, where 𝐴 ⊆ ℂ, is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝑌 = ((ℂfld ↾s 𝐴) ↑s 𝐼) & ⊢ 𝐷 = ((dist‘𝑌) ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐼 ∈ Fin) → (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋))) | ||
Syntax | cismty 32767 | Extend class notation with the class of metric space isometries. |
class Ismty | ||
Definition | df-ismty 32768* | Define a function which takes two metric spaces and returns the set of isometries between the spaces. An isometry is a bijection which preserves distance. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ Ismty = (𝑚 ∈ ∪ ran ∞Met, 𝑛 ∈ ∪ ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))}) | ||
Theorem | ismtyval 32769* | The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) = {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))}) | ||
Theorem | isismty 32770* | The condition "is an isometry". (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) ↔ (𝐹:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝐹‘𝑥)𝑁(𝐹‘𝑦))))) | ||
Theorem | ismtycnv 32771 | The inverse of an isometry is an isometry. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) → ◡𝐹 ∈ (𝑁 Ismty 𝑀))) | ||
Theorem | ismtyima 32772 | The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014.) |
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) ∧ (𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*)) → (𝐹 “ (𝑃(ball‘𝑀)𝑅)) = ((𝐹‘𝑃)(ball‘𝑁)𝑅)) | ||
Theorem | ismtyhmeolem 32773 | Lemma for ismtyhmeo 32774. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝑀) & ⊢ 𝐾 = (MetOpen‘𝑁) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑀 Ismty 𝑁)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | ismtyhmeo 32774 | An isometry is a homeomorphism on the induced topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝑀) & ⊢ 𝐾 = (MetOpen‘𝑁) ⇒ ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) ⊆ (𝐽Homeo𝐾)) | ||
Theorem | ismtybndlem 32775 | Lemma for ismtybnd 32776. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 19-Jan-2014.) |
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) → 𝑁 ∈ (Bnd‘𝑌))) | ||
Theorem | ismtybnd 32776 | Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 19-Jan-2014.) |
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) ↔ 𝑁 ∈ (Bnd‘𝑌))) | ||
Theorem | ismtyres 32777 | A restriction of an isometry is an isometry. The condition 𝐴 ⊆ 𝑋 is not necessary but makes the proof easier. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐵 = (𝐹 “ 𝐴) & ⊢ 𝑆 = (𝑀 ↾ (𝐴 × 𝐴)) & ⊢ 𝑇 = (𝑁 ↾ (𝐵 × 𝐵)) ⇒ ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ (𝑀 Ismty 𝑁) ∧ 𝐴 ⊆ 𝑋)) → (𝐹 ↾ 𝐴) ∈ (𝑆 Ismty 𝑇)) | ||
Theorem | heibor1lem 32778 | Lemma for heibor1 32779. A compact metric space is complete. This proof works by considering the collection cls(𝐹 “ (ℤ≥‘𝑛)) for each 𝑛 ∈ ℕ, which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain (𝐹 “ (ℤ≥‘𝑚)) for some 𝑚. Thus, by compactness, the intersection contains a point 𝑦, which must then be the convergent point of 𝐹. (Contributed by Jeff Madsen, 17-Jan-2014.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
Theorem | heibor1 32779 | One half of heibor 32790, that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet 22924 and total boundedness here, which follows trivially from the fact that the set of all 𝑟-balls is an open cover of 𝑋, so finitely many cover 𝑋. (Contributed by Jeff Madsen, 16-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) → (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋))) | ||
Theorem | heiborlem1 32780* | Lemma for heibor 32790. We work with a fixed open cover 𝑈 throughout. The set 𝐾 is the set of all subsets of 𝑋 that admit no finite subcover of 𝑈. (We wish to prove that 𝐾 is empty.) If a set 𝐶 has no finite subcover, then any finite cover of 𝐶 must contain a set that also has no finite subcover. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐾) → ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝐾) | ||
Theorem | heiborlem2 32781* | Lemma for heibor 32790. Substitutions for the set 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴𝐺𝐶 ↔ (𝐶 ∈ ℕ0 ∧ 𝐴 ∈ (𝐹‘𝐶) ∧ (𝐴𝐵𝐶) ∈ 𝐾)) | ||
Theorem | heiborlem3 32782* | Lemma for heibor 32790. Using countable choice ax-cc 9140, we have fixed in advance a collection of finite 2↑-𝑛 nets (𝐹‘𝑛) for 𝑋 (note that an 𝑟-net is a set of points in 𝑋 whose 𝑟 -balls cover 𝑋). The set 𝐺 is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set 𝐾). If the theorem was false, then 𝑋 would be in 𝐾, and so some ball at each level would also be in 𝐾. But we can say more than this; given a ball (𝑦𝐵𝑛) on level 𝑛, since level 𝑛 + 1 covers the space and thus also (𝑦𝐵𝑛), using heiborlem1 32780 there is a ball on the next level whose intersection with (𝑦𝐵𝑛) also has no finite subcover. Now since the set 𝐺 is a countable union of finite sets, it is countable (which needs ax-cc 9140 via iunctb 9275), and so we can apply ax-cc 9140 to 𝐺 directly to get a function from 𝐺 to itself, which points from each ball in 𝐾 to a ball on the next level in 𝐾, and such that the intersection between these balls is also in 𝐾. (Contributed by Jeff Madsen, 18-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) ⇒ ⊢ (𝜑 → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) | ||
Theorem | heiborlem4 32783* | Lemma for heibor 32790. Using the function 𝑇 constructed in heiborlem3 32782, construct an infinite path in 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ0) → (𝑆‘𝐴)𝐺𝐴) | ||
Theorem | heiborlem5 32784* | Lemma for heibor 32790. The function 𝑀 is a set of point-and-radius pairs suitable for application to caubl 22914. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) ⇒ ⊢ (𝜑 → 𝑀:ℕ⟶(𝑋 × ℝ+)) | ||
Theorem | heiborlem6 32785* | Lemma for heibor 32790. Since the sequence of balls connected by the function 𝑇 ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most 3 / 2 times the size of the larger, and so if we expand each ball by a factor of 3 we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘))) | ||
Theorem | heiborlem7 32786* | Lemma for heibor 32790. Since the sizes of the balls decrease exponentially, the sequence converges to zero. (Contributed by Jeff Madsen, 23-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) ⇒ ⊢ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ (2nd ‘(𝑀‘𝑘)) < 𝑟 | ||
Theorem | heiborlem8 32787* | Lemma for heibor 32790. The previous lemmas establish that the sequence 𝑀 is Cauchy, so using completeness we now consider the convergent point 𝑌. By assumption, 𝑈 is an open cover, so 𝑌 is an element of some 𝑍 ∈ 𝑈, and some ball centered at 𝑌 is contained in 𝑍. But the sequence contains arbitrarily small balls close to 𝑌, so some element ball(𝑀‘𝑛) of the sequence is contained in 𝑍. And finally we arrive at a contradiction, because {𝑍} is a finite subcover of 𝑈 that covers ball(𝑀‘𝑛), yet ball(𝑀‘𝑛) ∈ 𝐾. For convenience, we write this contradiction as 𝜑 → 𝜓 where 𝜑 is all the accumulated hypotheses and 𝜓 is anything at all. (Contributed by Jeff Madsen, 22-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ 𝑌 ∈ V & ⊢ (𝜑 → 𝑌 ∈ 𝑍) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → (1st ∘ 𝑀)(⇝𝑡‘𝐽)𝑌) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | heiborlem9 32788* | Lemma for heibor 32790. Discharge the hypotheses of heiborlem8 32787 by applying caubl 22914 to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) & ⊢ (𝜑 → 𝐶𝐺0) & ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))) & ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → ∪ 𝑈 = 𝑋) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | heiborlem10 32789* | Lemma for heibor 32790. The last remaining piece of the proof is to find an element 𝐶 such that 𝐶𝐺0, i.e. 𝐶 is an element of (𝐹‘0) that has no finite subcover, which is true by heiborlem1 32780, since (𝐹‘0) is a finite cover of 𝑋, which has no finite subcover. Thus, the rest of the proof follows to a contradiction, and thus there must be a finite subcover of 𝑈 that covers 𝑋, i.e. 𝑋 is compact. (Contributed by Jeff Madsen, 22-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) ⇒ ⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈)) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 = ∪ 𝑣) | ||
Theorem | heibor 32790 | Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 32779 and heiborlem1 32780 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) ↔ (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋))) | ||
Theorem | bfplem1 32791* | Lemma for bfp 32793. The sequence 𝐺, which simply starts from any point in the space and iterates 𝐹, satisfies the property that the distance from 𝐺(𝑛) to 𝐺(𝑛 + 1) decreases by at least 𝐾 after each step. Thus, the total distance from any 𝐺(𝑖) to 𝐺(𝑗) is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point ((⇝𝑡‘𝐽)‘𝐺) since the space is complete. (Contributed by Jeff Madsen, 17-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐾 ∈ ℝ+) & ⊢ (𝜑 → 𝐾 < 1) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴})) ⇒ ⊢ (𝜑 → 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺)) | ||
Theorem | bfplem2 32792* | Lemma for bfp 32793. Using the point found in bfplem1 32791, we show that this convergent point is a fixed point of 𝐹. Since for any positive 𝑥, the sequence 𝐺 is in 𝐵(𝑥 / 2, 𝑃) for all 𝑘 ∈ (ℤ≥‘𝑗) (where 𝑃 = ((⇝𝑡‘𝐽)‘𝐺)), we have 𝐷(𝐺(𝑗 + 1), 𝐹(𝑃)) ≤ 𝐷(𝐺(𝑗), 𝑃) < 𝑥 / 2 and 𝐷(𝐺(𝑗 + 1), 𝑃) < 𝑥 / 2, so 𝐹(𝑃) is in every neighborhood of 𝑃 and 𝑃 is a fixed point of 𝐹. (Contributed by Jeff Madsen, 5-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐾 ∈ ℝ+) & ⊢ (𝜑 → 𝐾 < 1) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴})) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) | ||
Theorem | bfp 32793* | Banach fixed point theorem, also known as contraction mapping theorem. A contraction on a complete metric space has a unique fixed point. We show existence in the lemmas, and uniqueness here - if 𝐹 has two fixed points, then the distance between them is less than 𝐾 times itself, a contradiction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐾 ∈ ℝ+) & ⊢ (𝜑 → 𝐾 < 1) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) ⇒ ⊢ (𝜑 → ∃!𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) | ||
Syntax | crrn 32794 | Extend class notation with the n-dimensional Euclidean space. |
class ℝn | ||
Definition | df-rrn 32795* | Define n-dimensional Euclidean space as a metric space with the standard Euclidean norm given by the quadratic mean. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ℝn = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑𝑚 𝑖), 𝑦 ∈ (ℝ ↑𝑚 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))) | ||
Theorem | rrnval 32796* | The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑𝑚 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))) | ||
Theorem | rrnmval 32797* | The value of the Euclidean metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑𝑚 𝐼) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝn‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | ||
Theorem | rrnmet 32798 | Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝑋 = (ℝ ↑𝑚 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) ∈ (Met‘𝑋)) | ||
Theorem | rrndstprj1 32799 | The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑𝑚 𝐼) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ (((𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝐴)𝑀(𝐺‘𝐴)) ≤ (𝐹(ℝn‘𝐼)𝐺)) | ||
Theorem | rrndstprj2 32800* | Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 32799 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = (ℝ ↑𝑚 𝐼) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝn‘𝐼)𝐺) < (𝑅 · (√‘(#‘𝐼)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |