HomeTheorem List (p. 235 of 465)
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. 235 of 465) | < 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-29259) |
Hilbert Space Explorer
(29260-30782) |
Users' Mathboxes
(30783-46465) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | tusbas 23401 | The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| ⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾)) | ||
| Theorem | tusunif 23402 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| ⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾)) | ||
| Theorem | tususs 23403 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
| ⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSt‘𝐾)) | ||
| Theorem | tustopn 23404 | The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| ⊢ 𝐾 = (toUnifSp‘𝑈) & ⊢ 𝐽 = (unifTop‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = (TopOpen‘𝐾)) | ||
| Theorem | tususp 23405 | A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| ⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ UnifSp) | ||
| Theorem | tustps 23406 | A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
| ⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ TopSp) | ||
| Theorem | uspreg 23407 | 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 23408 | Extend class notation with the uniform continuity operation. |
| class Cnu | ||
| Definition | df-ucn 23409* | 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 23410* | 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 23411* | 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 23412* | 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 23413* | Reformulate the 𝐺 function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ⇒ ⊢ 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ ⟨(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))⟩) | ||
| Theorem | ucnima 23414* | An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊) | ||
| Theorem | ucnprima 23415* | 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 23416 | 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 23417 | 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 23418 | 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 23419 | Extend class notation with the set of Cauchy filter bases. |
| class CauFilu | ||
| Definition | df-cfilu 23420* | 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 23421* | The predicate "𝐹 is a Cauchy filter base on uniform space 𝑈". (Contributed by Thierry Arnoux, 18-Nov-2017.) |
| ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐹 ∈ (CauFilu‘𝑈) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ 𝐹 (𝑎 × 𝑎) ⊆ 𝑣))) | ||
| Theorem | cfilufbas 23422 | A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐹 ∈ (CauFilu‘𝑈)) → 𝐹 ∈ (fBas‘𝑋)) | ||
| Theorem | cfiluexsm 23423* | 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 23424* | Lemma for fmucnd 23425. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| ⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝐴 × 𝐴)) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) | ||
| Theorem | fmucnd 23425* | 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 23426 | 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 23427 | 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 23428 | 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 23429 | 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 23430 | Extend class notation with the class of all complete uniform spaces. |
| class CUnifSp | ||
| Definition | df-cusp 23431* | 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 23432* | The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| ⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘(Base‘𝑊))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅))) | ||
| Theorem | cuspusp 23433 | A complete uniform space is an uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| ⊢ (𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp) | ||
| Theorem | cuspcvg 23434 | 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 23435* | The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 15-Dec-2017.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑈 = (UnifSt‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘𝐵)(𝑐 ∈ (CauFilu‘𝑈) → (𝐽 fLim 𝑐) ≠ ∅))) | ||
| Theorem | cnextucn 23436* | 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 23437 | 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 23438* | Express the predicate "𝐷 is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝐷 ∈ (PsMet‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐷𝑥) = 0 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | ||
| Theorem | psmetdmdm 23439 | Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) | ||
| Theorem | psmetf 23440 | The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) | ||
| Theorem | psmetcl 23441 | Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*) | ||
| Theorem | psmet0 23442 | 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 23443 | Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) | ||
| Theorem | psmetsym 23444 | The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) | ||
| Theorem | psmettri 23445 | Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵))) | ||
| Theorem | psmetge0 23446 | The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) | ||
| Theorem | psmetxrge0 23447 | 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 23448 | Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅)) | ||
| Theorem | psmetlecl 23449 | Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ) | ||
| Theorem | distspace 23450 | 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 23451 | Extend class notation with the class of extended metric spaces. |
| class ∞MetSp | ||
| Syntax | cms 23452 | Extend class notation with the class of metric spaces. |
| class MetSp | ||
| Syntax | ctms 23453 | Extend class notation with the function mapping a metric to the metric space it defines. |
| class toMetSp | ||
| Definition | df-xms 23454 | 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 23455 | Define the (proper) class of metric spaces. (Contributed by NM, 27-Aug-2006.) |
| ⊢ MetSp = {𝑓 ∈ ∞MetSp ∣ ((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))) ∈ (Met‘(Base‘𝑓))} | ||
| Definition | df-tms 23456 | 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 23457* | Express the predicate "𝐷 is a metric." (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))) | ||
| Theorem | isxmet 23458* | Express the predicate "𝐷 is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | ||
| Theorem | ismeti 23459* | Properties that determine a metric. (Contributed by NM, 17-Nov-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ 𝑋 ∈ V & ⊢ 𝐷:(𝑋 × 𝑋)⟶ℝ & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) | ||
| Theorem | isxmetd 23460* | Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 9-Apr-2024.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | ||
| Theorem | isxmet2d 23461* | 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 23462* | Lemma for metf 23464 and others. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))) | ||
| Theorem | xmetf 23463 | Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) | ||
| Theorem | metf 23464 | Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ) | ||
| Theorem | xmetcl 23465 | 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 23466 | 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 23467 | 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 23468 | A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | ||
| Theorem | xmetdmdm 23469 | Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = dom dom 𝐷) | ||
| Theorem | metdmdm 23470 | Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 = dom dom 𝐷) | ||
| Theorem | xmetunirn 23471 | 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 23472 | The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
| Theorem | meteq0 23473 | 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 23474 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) | ||
| Theorem | mettri2 23475 | 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 23476 | 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 23477 | 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 23478 | The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) | ||
| Theorem | metge0 23479 | 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 23480 | Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ) | ||
| Theorem | xmetsym 23481 | The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) | ||
| Theorem | xmetpsmet 23482 | An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) | ||
| Theorem | xmettpos 23483 | The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → tpos 𝐷 = 𝐷) | ||
| Theorem | metsym 23484 | 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 23485 | 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 23486 | 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 23487 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) | ||
| Theorem | mettri3 23488 | Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) | ||
| Theorem | xmetrtri 23489 | 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 23490 | 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 20623 defined on the extended real structure. (Contributed by Mario Carneiro, 4-Sep-2015.) |
| ⊢ 𝐾 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶)𝐾(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵)) | ||
| Theorem | metrtri 23491 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) | ||
| Theorem | xmetgt0 23492 | The distance function of an extended metric space is positive for unequal points. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≠ 𝐵 ↔ 0 < (𝐴𝐷𝐵))) | ||
| Theorem | metgt0 23493 | 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 23494 | 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 23495 | Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘𝑅)) | ||
| Theorem | metreslem 23496 | Lemma for metres 23499. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ (dom 𝐷 = (𝑋 × 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) = (𝐷 ↾ ((𝑋 ∩ 𝑅) × (𝑋 ∩ 𝑅)))) | ||
| Theorem | metres2 23497 | Lemma for metres 23499. (Contributed by FL, 12-Oct-2006.) (Proof shortened by Mario Carneiro, 14-Aug-2015.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘𝑅)) | ||
| Theorem | xmetres 23498 | A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘(𝑋 ∩ 𝑅))) | ||
| Theorem | metres 23499 | 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 23500 | The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ ∅ ∈ (Met‘∅) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |