HomeTheorem List (p. 246 of 509)
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. 246 of 509) | < 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-31400) |
Hilbert Space Explorer
(31401-32923) |
Users' Mathboxes
(32924-50825) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | tususp 24501 | A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| ⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ UnifSp) | ||
| Theorem | tustps 24502 | A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
| ⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ TopSp) | ||
| Theorem | uspreg 24503 | If a uniform space is Hausdorff, it is regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
| ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ ((𝑊 ∈ UnifSp ∧ 𝐽 ∈ Haus) → 𝐽 ∈ Reg) | ||
| Syntax | cucn 24504 | Extend class notation with the uniform continuity operation. |
| class Cnu | ||
| Definition | df-ucn 24505* | Define a function on two uniform structures which value is the set of uniformly continuous functions from the first uniform structure to the second. A function 𝑓 is uniformly continuous if, roughly speaking, it is possible to guarantee that (𝑓‘𝑥) and (𝑓‘𝑦) be as close to each other as we please by requiring only that 𝑥 and 𝑦 are sufficiently close to each other; unlike ordinary continuity, the maximum distance between (𝑓‘𝑥) and (𝑓‘𝑦) cannot depend on 𝑥 and 𝑦 themselves. This formulation is the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| ⊢ Cnu = (𝑢 ∈ ∪ ran UnifOn, 𝑣 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (dom ∪ 𝑣 ↑m dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))}) | ||
| Theorem | ucnval 24506* | The set of all uniformly continuous function from uniform space 𝑈 to uniform space 𝑉. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cnu𝑉) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))}) | ||
| Theorem | isucn 24507* | The predicate "𝐹 is a uniformly continuous function from uniform space 𝑈 to uniform space 𝑉". (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))))) | ||
| Theorem | isucn2 24508* | The predicate "𝐹 is a uniformly continuous function from uniform space 𝑈 to uniform space 𝑉", expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018.) |
| ⊢ 𝑈 = ((𝑋 × 𝑋)filGen𝑅) & ⊢ 𝑉 = ((𝑌 × 𝑌)filGen𝑆) & ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝑅 ∈ (fBas‘(𝑋 × 𝑋))) & ⊢ (𝜑 → 𝑆 ∈ (fBas‘(𝑌 × 𝑌))) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦))))) | ||
| Theorem | ucnimalem 24509* | Reformulate the 𝐺 function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ⇒ ⊢ 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ ⟨(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))⟩) | ||
| Theorem | ucnima 24510* | An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊) | ||
| Theorem | ucnprima 24511* | The preimage by a uniformly continuous function 𝐹 of an entourage 𝑊 of 𝑌 is an entourage of 𝑋. Note of the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ⇒ ⊢ (𝜑 → (◡𝐺 “ 𝑊) ∈ 𝑈) | ||
| Theorem | iducn 24512 | The identity is uniformly continuous from a uniform structure to itself. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝑈 Cnu𝑈)) | ||
| Theorem | cstucnd 24513 | A constant function is uniformly continuous. Deduction form. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝐴 ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝑋 × {𝐴}) ∈ (𝑈 Cnu𝑉)) | ||
| Theorem | ucncn 24514 | Uniform continuity implies continuity. Deduction form. Proposition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝐾 = (TopOpen‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ UnifSp) & ⊢ (𝜑 → 𝑆 ∈ UnifSp) & ⊢ (𝜑 → 𝑅 ∈ TopSp) & ⊢ (𝜑 → 𝑆 ∈ TopSp) & ⊢ (𝜑 → 𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
| Syntax | ccfilu 24515 | Extend class notation with the set of Cauchy filter bases. |
| class CauFilu | ||
| Definition | df-cfilu 24516* | Define the set of Cauchy filter bases on a uniform space. A Cauchy filter base is a filter base on the set such that for every entourage 𝑣, there is an element 𝑎 of the filter "small enough in 𝑣 " i.e. such that every pair {𝑥, 𝑦} of points in 𝑎 is related by 𝑣". Definition 2 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| ⊢ CauFilu = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (fBas‘dom ∪ 𝑢) ∣ ∀𝑣 ∈ 𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣}) | ||
| Theorem | iscfilu 24517* | The predicate "𝐹 is a Cauchy filter base on uniform space 𝑈". (Contributed by Thierry Arnoux, 18-Nov-2017.) |
| ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐹 ∈ (CauFilu‘𝑈) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ 𝐹 (𝑎 × 𝑎) ⊆ 𝑣))) | ||
| Theorem | cfilufbas 24518 | A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈)) → 𝐹 ∈ (fBas‘𝑋)) | ||
| Theorem | cfiluexsm 24519* | For a Cauchy filter base and any entourage 𝑉, there is an element of the filter small in 𝑉. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈) ∧ 𝑉 ∈ 𝑈) → ∃𝑎 ∈ 𝐹 (𝑎 × 𝑎) ⊆ 𝑉) | ||
| Theorem | fmucndlem 24520* | Lemma for fmucnd 24521. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝐴 × 𝐴)) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) | ||
| Theorem | fmucnd 24521* | The image of a Cauchy filter base by an uniformly continuous function is a Cauchy filter base. Deduction form. Proposition 3 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) & ⊢ (𝜑 → 𝐶 ∈ (CauFilu‘𝑈)) & ⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉)) | ||
| Theorem | cfilufg 24522 | The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.) |
| ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈)) → (𝑋filGen𝐹) ∈ (CauFilu‘𝑈)) | ||
| Theorem | trcfilu 24523 | Condition for the trace of a Cauchy filter base to be a Cauchy filter base for the restricted uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018.) |
| ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐹 ∈ (CauFilu‘𝑈) ∧ ¬ ∅ ∈ (𝐹 ↾t 𝐴)) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾t 𝐴) ∈ (CauFilu‘(𝑈 ↾t (𝐴 × 𝐴)))) | ||
| Theorem | cfiluweak 24524 | A Cauchy filter base is also a Cauchy filter base on any coarser uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018.) |
| ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ (CauFilu‘(𝑈 ↾t (𝐴 × 𝐴)))) → 𝐹 ∈ (CauFilu‘𝑈)) | ||
| Theorem | neipcfilu 24525 | In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.) |
| ⊢ 𝑋 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝑈 = (UnifSt‘𝑊) ⇒ ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) ∈ (CauFilu‘𝑈)) | ||
| Syntax | ccusp 24526 | Extend class notation with the class of all complete uniform spaces. |
| class CUnifSp | ||
| Definition | df-cusp 24527* | Define the class of all complete uniform spaces. Definition 3 of [BourbakiTop1] p. II.15. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
| ⊢ CUnifSp = {𝑤 ∈ UnifSp ∣ ∀𝑐 ∈ (Fil‘(Base‘𝑤))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)} | ||
| Theorem | iscusp 24528* | The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| ⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘(Base‘𝑊))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅))) | ||
| Theorem | cuspusp 24529 | A complete uniform space is an uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| ⊢ (𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp) | ||
| Theorem | cuspcvg 24530 | In a complete uniform space, any Cauchy filter 𝐶 has a limit. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ ((𝑊 ∈ CUnifSp ∧ 𝐶 ∈ (CauFilu‘(UnifSt‘𝑊)) ∧ 𝐶 ∈ (Fil‘𝐵)) → (𝐽 fLim 𝐶) ≠ ∅) | ||
| Theorem | iscusp2 24531* | The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 15-Dec-2017.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑈 = (UnifSt‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘𝐵)(𝑐 ∈ (CauFilu‘𝑈) → (𝐽 fLim 𝑐) ≠ ∅))) | ||
| Theorem | cnextucn 24532* | Extension by continuity. Proposition 11 of [BourbakiTop1] p. II.20. Given a topology 𝐽 on 𝑋, a subset 𝐴 dense in 𝑋, this states a condition for 𝐹 from 𝐴 to a space 𝑌 Hausdorff and complete to be extensible by continuity. (Contributed by Thierry Arnoux, 4-Dec-2017.) |
| ⊢ 𝑋 = (Base‘𝑉) & ⊢ 𝑌 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑉) & ⊢ 𝐾 = (TopOpen‘𝑊) & ⊢ 𝑈 = (UnifSt‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ TopSp) & ⊢ (𝜑 → 𝑊 ∈ TopSp) & ⊢ (𝜑 → 𝑊 ∈ CUnifSp) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑌) & ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈ (CauFilu‘𝑈)) ⇒ ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | ucnextcn 24533 | Extension by continuity. Theorem 2 of [BourbakiTop1] p. II.20. Given an uniform space on a set 𝑋, a subset 𝐴 dense in 𝑋, and a function 𝐹 uniformly continuous from 𝐴 to 𝑌, that function can be extended by continuity to the whole 𝑋, and its extension is uniformly continuous. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
| ⊢ 𝑋 = (Base‘𝑉) & ⊢ 𝑌 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑉) & ⊢ 𝐾 = (TopOpen‘𝑊) & ⊢ 𝑆 = (UnifSt‘𝑉) & ⊢ 𝑇 = (UnifSt‘(𝑉 ↾s 𝐴)) & ⊢ 𝑈 = (UnifSt‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ TopSp) & ⊢ (𝜑 → 𝑉 ∈ UnifSp) & ⊢ (𝜑 → 𝑊 ∈ TopSp) & ⊢ (𝜑 → 𝑊 ∈ CUnifSp) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ (𝑇 Cnu𝑈)) & ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋) ⇒ ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | ispsmet 24534* | Express the predicate "𝐷 is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝐷 ∈ (PsMet‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐷𝑥) = 0 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | ||
| Theorem | psmetdmdm 24535 | Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) | ||
| Theorem | psmetf 24536 | The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) | ||
| Theorem | psmetcl 24537 | Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*) | ||
| Theorem | psmet0 24538 | The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) | ||
| Theorem | psmettri2 24539 | Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) | ||
| Theorem | psmetsym 24540 | The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) | ||
| Theorem | psmettri 24541 | Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵))) | ||
| Theorem | psmetge0 24542 | The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) | ||
| Theorem | psmetxrge0 24543 | The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) | ||
| Theorem | psmetres2 24544 | Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅)) | ||
| Theorem | psmetlecl 24545 | Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ) | ||
| Theorem | distspace 24546 | A set 𝑋 together with a (distance) function 𝐷 which is a pseudometric is a distance space (according to E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006), i.e. a (base) set 𝑋 equipped with a distance 𝐷, which is a mapping of two elements of the base set to the (extended) reals and which is nonnegative, symmetric and equal to 0 if the two elements are equal. (Contributed by AV, 15-Oct-2021.) (Revised by AV, 5-Jul-2022.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ (𝐴𝐷𝐴) = 0) ∧ (0 ≤ (𝐴𝐷𝐵) ∧ (𝐴𝐷𝐵) = (𝐵𝐷𝐴)))) | ||
| Syntax | cxms 24547 | Extend class notation with the class of extended metric spaces. |
| class ∞MetSp | ||
| Syntax | cms 24548 | Extend class notation with the class of metric spaces. |
| class MetSp | ||
| Syntax | ctms 24549 | Extend class notation with the function mapping a metric to the metric space it defines. |
| class toMetSp | ||
| Definition | df-xms 24550 | Define the (proper) class of extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ ∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpen‘𝑓) = (MetOpen‘((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))))} | ||
| Definition | df-ms 24551 | Define the (proper) class of metric spaces. (Contributed by NM, 27-Aug-2006.) |
| ⊢ MetSp = {𝑓 ∈ ∞MetSp ∣ ((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))) ∈ (Met‘(Base‘𝑓))} | ||
| Definition | df-tms 24552 | Define the function mapping a metric to the metric space which it defines. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ toMetSp = (𝑑 ∈ ∪ ran ∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩)) | ||
| Theorem | ismet 24553* | Express the predicate "𝐷 is a metric." (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))) | ||
| Theorem | isxmet 24554* | Express the predicate "𝐷 is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | ||
| Theorem | ismeti 24555* | Properties that determine a metric. (Contributed by NM, 17-Nov-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ 𝑋 ∈ V & ⊢ 𝐷:(𝑋 × 𝑋)⟶ℝ & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) | ||
| Theorem | isxmetd 24556* | Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 9-Apr-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | ||
| Theorem | isxmet2d 24557* | It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: 𝐷(𝑥, 𝑦) = if(𝑥 = 𝑦, 0, -∞) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (𝑥𝐷𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | ||
| Theorem | metflem 24558* | Lemma for metf 24560 and others. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))) | ||
| Theorem | xmetf 24559 | Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) | ||
| Theorem | metf 24560 | Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ) | ||
| Theorem | xmetcl 24561 | Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*) | ||
| Theorem | metcl 24562 | Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ) | ||
| Theorem | ismet2 24563 | An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐷:(𝑋 × 𝑋)⟶ℝ)) | ||
| Theorem | metxmet 24564 | A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | ||
| Theorem | xmetdmdm 24565 | Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = dom dom 𝐷) | ||
| Theorem | metdmdm 24566 | Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 = dom dom 𝐷) | ||
| Theorem | xmetunirn 24567 | Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
| ⊢ (𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ (∞Met‘dom dom 𝐷)) | ||
| Theorem | xmeteq0 24568 | The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
| Theorem | meteq0 24569 | The value of a metric is zero iff its arguments are equal. Property M2 of [Kreyszig] p. 4. (Contributed by NM, 30-Aug-2006.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
| Theorem | xmettri2 24570 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) | ||
| Theorem | mettri2 24571 | Triangle inequality for the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵))) | ||
| Theorem | xmet0 24572 | The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) | ||
| Theorem | met0 24573 | The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by NM, 30-Aug-2006.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) | ||
| Theorem | xmetge0 24574 | The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) | ||
| Theorem | metge0 24575 | The distance function of a metric space is nonnegative. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) | ||
| Theorem | xmetlecl 24576 | Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ) | ||
| Theorem | xmetsym 24577 | The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) | ||
| Theorem | xmetpsmet 24578 | An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) | ||
| Theorem | xmettpos 24579 | The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → tpos 𝐷 = 𝐷) | ||
| Theorem | metsym 24580 | The distance function of a metric space is symmetric. Definition 14-1.1(c) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) | ||
| Theorem | xmettri 24581 | Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵))) | ||
| Theorem | mettri 24582 | Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐶𝐷𝐵))) | ||
| Theorem | xmettri3 24583 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) | ||
| Theorem | mettri3 24584 | Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) | ||
| Theorem | xmetrtri 24585 | One half of the reverse triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶) +𝑒 -𝑒(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵)) | ||
| Theorem | xmetrtri2 24586 | The reverse triangle inequality for the distance function of an extended metric. In order to express the "extended absolute value function", we use the distance function xrsdsval 21628 defined on the extended real structure. (Contributed by Mario Carneiro, 4-Sep-2015.) |
| ⊢ 𝐾 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶)𝐾(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵)) | ||
| Theorem | metrtri 24587 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) | ||
| Theorem | xmetgt0 24588 | The distance function of an extended metric space is positive for unequal points. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≠ 𝐵 ↔ 0 < (𝐴𝐷𝐵))) | ||
| Theorem | metgt0 24589 | The distance function of a metric space is positive for unequal points. Definition 14-1.1(b) of [Gleason] p. 223 and its converse. (Contributed by NM, 27-Aug-2006.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≠ 𝐵 ↔ 0 < (𝐴𝐷𝐵))) | ||
| Theorem | metn0 24590 | A metric space is nonempty iff its base set is nonempty. (Contributed by NM, 4-Oct-2007.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷 ≠ ∅ ↔ 𝑋 ≠ ∅)) | ||
| Theorem | xmetres2 24591 | Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘𝑅)) | ||
| Theorem | metreslem 24592 | Lemma for metres 24595. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ (dom 𝐷 = (𝑋 × 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) = (𝐷 ↾ ((𝑋 ∩ 𝑅) × (𝑋 ∩ 𝑅)))) | ||
| Theorem | metres2 24593 | Lemma for metres 24595. (Contributed by FL, 12-Oct-2006.) (Proof shortened by Mario Carneiro, 14-Aug-2015.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘𝑅)) | ||
| Theorem | xmetres 24594 | A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘(𝑋 ∩ 𝑅))) | ||
| Theorem | metres 24595 | A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘(𝑋 ∩ 𝑅))) | ||
| Theorem | 0met 24596 | The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ ∅ ∈ (Met‘∅) | ||
| Theorem | prdsdsf 24597* | The product metric is a function into the nonnegative extended reals. In general this means that it is not a metric but rather an *extended* metric (even when all the factors are metrics), but it will be a metric when restricted to regions where it does not take infinite values. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞)) | ||
| Theorem | prdsxmetlem 24598* | The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) | ||
| Theorem | prdsxmet 24599* | The product metric is an extended metric. Eliminate disjoint variable conditions from prdsxmetlem 24598. (Contributed by Mario Carneiro, 26-Sep-2015.) |
| ⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) | ||
| Theorem | prdsmet 24600* | The product metric is a metric when the index set is finite. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |