HomeTheorem List (p. 378 of 491)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 378 of 491) | < 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-30946) |
Hilbert Space Explorer
(30947-32469) |
Users' Mathboxes
(32470-49035) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cover2 37701* | Two ways of expressing the statement "there is a cover of 𝐴 by elements of 𝐵 such that for each set in the cover, 𝜑". Note that 𝜑 and 𝑥 must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010.) |
| ⊢ 𝐵 ∈ V & ⊢ 𝐴 = ∪ 𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)) | ||
| Theorem | cover2g 37702* | Two ways of expressing the statement "there is a cover of 𝐴 by elements of 𝐵 such that for each set in the cover, 𝜑". Note that 𝜑 and 𝑥 must be distinct. (Contributed by Jeff Madsen, 21-Jun-2010.) |
| ⊢ 𝐴 = ∪ 𝐵 ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))) | ||
| Theorem | brabg2 37703* | Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} & ⊢ (𝜒 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝐵 ∈ 𝐷 → (𝐴𝑅𝐵 ↔ 𝜒)) | ||
| Theorem | opelopab3 37704* | Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.) |
| ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝐵 ∈ 𝐷 → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒)) | ||
| Theorem | cocanfo 37705 | Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
| ⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → 𝐺 = 𝐻) | ||
| Theorem | brresi2 37706 | Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝑅 ↾ 𝐶)𝐵 → 𝐴𝑅𝐵) | ||
| Theorem | fnopabeqd 37707* | Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.) |
| ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}) | ||
| Theorem | fvopabf4g 37708* | Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
| ⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑m 𝐷) ↦ 𝐵) ⇒ ⊢ ((𝐷 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ∧ 𝐴:𝐷⟶𝑅) → (𝐹‘𝐴) = 𝐶) | ||
| Theorem | fnopabco 37709* | Composition of a function with a function abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} & ⊢ 𝐺 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐻‘𝐵))} ⇒ ⊢ (𝐻 Fn 𝐶 → 𝐺 = (𝐻 ∘ 𝐹)) | ||
| Theorem | opropabco 37710* | Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
| ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑅) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑆) & ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = ⟨𝐵, 𝐶⟩)} & ⊢ 𝐺 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐵𝑀𝐶))} ⇒ ⊢ (𝑀 Fn (𝑅 × 𝑆) → 𝐺 = (𝑀 ∘ 𝐹)) | ||
| Theorem | cocnv 37711 | Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ((𝐹 ∘ 𝐺) ∘ ◡𝐺) = (𝐹 ↾ ran 𝐺)) | ||
| Theorem | f1ocan1fv 37712 | Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
| ⊢ ((Fun 𝐹 ∧ 𝐺:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝐹 ∘ 𝐺)‘(◡𝐺‘𝑋)) = (𝐹‘𝑋)) | ||
| Theorem | f1ocan2fv 37713 | Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((Fun 𝐹 ∧ 𝐺:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ ◡𝐺)‘(𝐺‘𝑋)) = (𝐹‘𝑋)) | ||
| Theorem | inixp 37714* | Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶) = X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) | ||
| Theorem | upixp 37715* | Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
| ⊢ 𝑋 = X𝑏 ∈ 𝐴 (𝐶‘𝑏) & ⊢ 𝑃 = (𝑤 ∈ 𝐴 ↦ (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑤))) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → ∃!ℎ(ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) | ||
| Theorem | abrexdom 37716* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑦 ∈ 𝐴 → ∃*𝑥𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝜑} ≼ 𝐴) | ||
| Theorem | abrexdom2 37717* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = 𝐵} ≼ 𝐴) | ||
| Theorem | ac6gf 37718* | Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
| Theorem | indexa 37719* | If for every element of an indexing set 𝐴 there exists a corresponding element of another set 𝐵, then there exists a subset of 𝐵 consisting only of those elements which are indexed by 𝐴. Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) | ||
| Theorem | indexdom 37720* | If for every element of an indexing set 𝐴 there exists a corresponding element of another set 𝐵, then there exists a subset of 𝐵 consisting only of those elements which are indexed by 𝐴, and which is dominated by the set 𝐴. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) | ||
| Theorem | frinfm 37721* | A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) | ||
| Theorem | welb 37722* | A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑅 We 𝐴 ∧ (𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → (◡𝑅 Or 𝐵 ∧ ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))) | ||
| Theorem | supex2g 37723 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 ∈ 𝐶 → sup(𝐵, 𝐴, 𝑅) ∈ V) | ||
| Theorem | supclt 37724* | Closure of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑅 Or 𝐴 ∧ ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
| Theorem | supubt 37725* | Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑅 Or 𝐴 ∧ ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
| Theorem | filbcmb 37726* | Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦 ≤ 𝑧 → 𝜑) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦 ≤ 𝑧 → ∀𝑥 ∈ 𝐴 𝜑))) | ||
| Theorem | fzmul 37727 | Membership of a product in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (𝐽 ∈ (𝑀...𝑁) → (𝐾 · 𝐽) ∈ ((𝐾 · 𝑀)...(𝐾 · 𝑁)))) | ||
| Theorem | sdclem2 37728* | Lemma for sdc 37730. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏)) & ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) & ⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) & ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} & ⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) & ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐺:𝑍⟶𝐽) & ⊢ (𝜑 → (𝐺‘𝑀):(𝑀...𝑀)⟶𝐴) & ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺‘𝑤))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) | ||
| Theorem | sdclem1 37729* | Lemma for sdc 37730. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏)) & ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) & ⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) & ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} & ⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) | ||
| Theorem | sdc 37730* | 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 to construct infinite sequences 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 37731* | 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 37732* | Variant of fdc 37731 with no specified base value. (Contributed by Jeff Madsen, 18-Jun-2010.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝑀 ∈ ℤ & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (𝑎 = (𝑓‘𝑀) → (𝜁 ↔ 𝜎)) & ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒)) & ⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏)) & ⊢ (𝜂 → ∃𝑎 ∈ 𝐴 𝜁) & ⊢ (𝜂 → 𝑅 Fr 𝐴) & ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑)) & ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎) ⇒ ⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) | ||
| Theorem | seqpo 37733* | Two ways to say that a sequence respects a partial order. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) → (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ↔ ∀𝑚 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛))) | ||
| Theorem | incsequz 37734* | An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ≥‘𝐴)) | ||
| Theorem | incsequz2 37735* | An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ (ℤ≥‘𝐴)) | ||
| Theorem | nnubfi 37736* | 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 37737* | 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 37738 | 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 37739 | 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 37740 | Limit points of a subset are limit points of the larger set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((limPt‘𝐽)‘𝐵) ⊆ ((limPt‘𝐽)‘𝐴)) | ||
| Theorem | metf1o 37741* | 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 37742 | 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 37743* | 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 37744* | 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 37745* | 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 37746 | 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 37747* | 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 37748* | A constant function is a continuous function on ℂ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved into main set.mm as cncfmptc 24951 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐴) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
| Theorem | cnres2 37749* | 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 37750 | 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 37751* | 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 37752 | Extend class notation with the class of totally bounded metric spaces. |
| class TotBnd | ||
| Syntax | cbnd 37753 | Extend class notation with the class of bounded metric spaces. |
| class Bnd | ||
| Definition | df-totbnd 37754* | 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 37755* | The predicate "is a totally bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
| Theorem | istotbnd2 37756* | The predicate "is a totally bounded metric space." (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑀 ∈ (Met‘𝑋) → (𝑀 ∈ (TotBnd‘𝑋) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
| Theorem | istotbnd3 37757* | 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 37758 | The predicate "totally bounded" implies 𝑀 is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Met‘𝑋)) | ||
| Theorem | 0totbnd 37759 | The metric (there is only one) on the empty set is totally bounded. (Contributed by Mario Carneiro, 16-Sep-2015.) |
| ⊢ (𝑋 = ∅ → (𝑀 ∈ (TotBnd‘𝑋) ↔ 𝑀 ∈ (Met‘𝑋))) | ||
| Theorem | sstotbnd2 37760* | 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 37761* | 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 37762* | 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 37763 | 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 37764* | 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 37765* | 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 37766* | 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 37767 | A bounded metric space is a metric space. (Contributed by Mario Carneiro, 16-Sep-2015.) |
| ⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 ∈ (Met‘𝑋)) | ||
| Theorem | isbndx 37768* | 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 37769* | 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 37770* | 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 37771* | 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 37772 | A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (Bnd‘𝑆)) | ||
| Theorem | blbnd 37773 | 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 37774* | 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 37775 | 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 37755 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 37776* | 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 37777 | Lemma for equivbnd2 37778 and similar theorems. (Contributed by Jeff Madsen, 16-Sep-2015.) |
| ⊢ 𝐷 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝐷 ∈ (Bnd‘𝑌)) → 𝑌 ⊆ 𝑋) | ||
| Theorem | equivbnd2 37778* | 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 37779* | 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 37780* | 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 37781* | 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 37782 | 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 37783 | 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 37784 | Extend class notation with the class of metric space isometries. |
| class Ismty | ||
| Definition | df-ismty 37785* | 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 37786* | The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) = {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))}) | ||
| Theorem | isismty 37787* | The condition "is an isometry". (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) ↔ (𝐹:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝐹‘𝑥)𝑁(𝐹‘𝑦))))) | ||
| Theorem | ismtycnv 37788 | The inverse of an isometry is an isometry. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) → ◡𝐹 ∈ (𝑁 Ismty 𝑀))) | ||
| Theorem | ismtyima 37789 | 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 37790 | Lemma for ismtyhmeo 37791. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
| ⊢ 𝐽 = (MetOpen‘𝑀) & ⊢ 𝐾 = (MetOpen‘𝑁) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑀 Ismty 𝑁)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | ismtyhmeo 37791 | 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 37792 | Lemma for ismtybnd 37793. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 19-Jan-2014.) |
| ⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) → 𝑁 ∈ (Bnd‘𝑌))) | ||
| Theorem | ismtybnd 37793 | Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 19-Jan-2014.) |
| ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) ↔ 𝑁 ∈ (Bnd‘𝑌))) | ||
| Theorem | ismtyres 37794 | 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 37795 | Lemma for heibor1 37796. 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 37796 | One half of heibor 37807, that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet 25366 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 37797* | Lemma for heibor 37807. 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 37798* | Lemma for heibor 37807. Substitutions for the set 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴𝐺𝐶 ↔ (𝐶 ∈ ℕ0 ∧ 𝐴 ∈ (𝐹‘𝐶) ∧ (𝐴𝐵𝐶) ∈ 𝐾)) | ||
| Theorem | heiborlem3 37799* | Lemma for heibor 37807. Using countable choice ax-cc 10472, 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 37797 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 10472 via iunctb 10611), and so we can apply ax-cc 10472 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 37800* | Lemma for heibor 37807. Using the function 𝑇 constructed in heiborlem3 37799, 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) → (𝑆‘𝐴)𝐺𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |