Home | Metamath
Proof Explorer Theorem List (p. 222 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | ccusp 22101 | Extend class notation with the class of all complete uniform spaces. |
class CUnifSp | ||
Definition | df-cusp 22102* | 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 22103* | The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017.) |
⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘(Base‘𝑊))(𝑐 ∈ (CauFilu‘(UnifSt‘𝑊)) → ((TopOpen‘𝑊) fLim 𝑐) ≠ ∅))) | ||
Theorem | cuspusp 22104 | A complete uniform space is an uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
⊢ (𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp) | ||
Theorem | cuspcvg 22105 | 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 22106* | The predicate "𝑊 is a complete uniform space." (Contributed by Thierry Arnoux, 15-Dec-2017.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑈 = (UnifSt‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ (𝑊 ∈ CUnifSp ↔ (𝑊 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘𝐵)(𝑐 ∈ (CauFilu‘𝑈) → (𝐽 fLim 𝑐) ≠ ∅))) | ||
Theorem | cnextucn 22107* | 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 22108 | 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 22109* | Express the predicate "𝐷 is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝑋 ∈ 𝑉 → (𝐷 ∈ (PsMet‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ((𝑥𝐷𝑥) = 0 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | ||
Theorem | psmetdmdm 22110 | Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) | ||
Theorem | psmetf 22111 | The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) | ||
Theorem | psmetcl 22112 | Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*) | ||
Theorem | psmet0 22113 | 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 22114 | Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) | ||
Theorem | psmetsym 22115 | The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) | ||
Theorem | psmettri 22116 | Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵))) | ||
Theorem | psmetge0 22117 | The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) | ||
Theorem | psmetxrge0 22118 | 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 22119 | Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅)) | ||
Theorem | psmetlecl 22120 | Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ) | ||
Theorem | distspace 22121 | A structure 𝐺 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 non-negative, symmetric and equal to 0 if the two elements are equal. (Contributed by AV, 15-Oct-2021.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ (𝐴𝐷𝐴) = 0) ∧ (0 ≤ (𝐴𝐷𝐵) ∧ (𝐴𝐷𝐵) = (𝐵𝐷𝐴)))) | ||
Syntax | cxme 22122 | Extend class notation with the class of all extended metric spaces. |
class ∞MetSp | ||
Syntax | cmt 22123 | Extend class notation with the class of all metric spaces. |
class MetSp | ||
Syntax | ctmt 22124 | Extend class notation with the function mapping a metric to a metric space. |
class toMetSp | ||
Definition | df-xms 22125 | Define the (proper) class of all extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ ∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpen‘𝑓) = (MetOpen‘((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))))} | ||
Definition | df-ms 22126 | Define the (proper) class of all metric spaces. (Contributed by NM, 27-Aug-2006.) |
⊢ MetSp = {𝑓 ∈ ∞MetSp ∣ ((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))) ∈ (Met‘(Base‘𝑓))} | ||
Definition | df-tms 22127 | Define the function mapping a metric to a metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ toMetSp = (𝑑 ∈ ∪ ran ∞Met ↦ ({〈(Base‘ndx), dom dom 𝑑〉, 〈(dist‘ndx), 𝑑〉} sSet 〈(TopSet‘ndx), (MetOpen‘𝑑)〉)) | ||
Theorem | ismet 22128* | Express the predicate "𝐷 is a metric." (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))) | ||
Theorem | isxmet 22129* | Express the predicate "𝐷 is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) | ||
Theorem | ismeti 22130* | Properties that determine a metric. (Contributed by NM, 17-Nov-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝑋 ∈ V & ⊢ 𝐷:(𝑋 × 𝑋)⟶ℝ & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) | ||
Theorem | isxmetd 22131* | Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | ||
Theorem | isxmet2d 22132* | 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.) |
⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (𝑥𝐷𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | ||
Theorem | metflem 22133* | Lemma for metf 22135 and others. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))) | ||
Theorem | xmetf 22134 | Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) | ||
Theorem | metf 22135 | Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) |
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ) | ||
Theorem | xmetcl 22136 | 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 22137 | 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 22138 | 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 22139 | A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | ||
Theorem | xmetdmdm 22140 | Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = dom dom 𝐷) | ||
Theorem | metdmdm 22141 | Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 = dom dom 𝐷) | ||
Theorem | xmetunirn 22142 | 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 22143 | The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
Theorem | meteq0 22144 | 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 22145 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) | ||
Theorem | mettri2 22146 | 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 22147 | 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 22148 | 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 22149 | The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) | ||
Theorem | metge0 22150 | 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 22151 | Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ) | ||
Theorem | xmetsym 22152 | The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) | ||
Theorem | xmetpsmet 22153 | An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) | ||
Theorem | xmettpos 22154 | The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → tpos 𝐷 = 𝐷) | ||
Theorem | metsym 22155 | 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 22156 | 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 22157 | 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 22158 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) | ||
Theorem | mettri3 22159 | Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007.) |
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) | ||
Theorem | xmetrtri 22160 | 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 22161 | 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 19790 defined on the extended real structure. (Contributed by Mario Carneiro, 4-Sep-2015.) |
⊢ 𝐾 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶)𝐾(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵)) | ||
Theorem | metrtri 22162 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.) |
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) | ||
Theorem | xmetgt0 22163 | The distance function of an extended metric space is positive for unequal points. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≠ 𝐵 ↔ 0 < (𝐴𝐷𝐵))) | ||
Theorem | metgt0 22164 | 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 22165 | 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 22166 | Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘𝑅)) | ||
Theorem | metreslem 22167 | Lemma for metres 22170. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ (dom 𝐷 = (𝑋 × 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) = (𝐷 ↾ ((𝑋 ∩ 𝑅) × (𝑋 ∩ 𝑅)))) | ||
Theorem | metres2 22168 | Lemma for metres 22170. (Contributed by FL, 12-Oct-2006.) (Proof shortened by Mario Carneiro, 14-Aug-2015.) |
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘𝑅)) | ||
Theorem | xmetres 22169 | A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘(𝑋 ∩ 𝑅))) | ||
Theorem | metres 22170 | 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 22171 | The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ ∅ ∈ (Met‘∅) | ||
Theorem | prdsdsf 22172* | 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 22173* | The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) | ||
Theorem | prdsxmet 22174* | The product metric is an extended metric. Eliminate disjoint variable conditions from prdsxmetlem 22173. (Contributed by Mario Carneiro, 26-Sep-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) | ||
Theorem | prdsmet 22175* | 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‘𝐵)) | ||
Theorem | ressprdsds 22176* | Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))) & ⊢ (𝜑 → 𝐻 = (𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴)))) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐴 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐸 = (𝐷 ↾ (𝐵 × 𝐵))) | ||
Theorem | resspwsds 22177 | Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ (𝜑 → 𝑌 = (𝑅 ↑s 𝐼)) & ⊢ (𝜑 → 𝐻 = ((𝑅 ↾s 𝐴) ↑s 𝐼)) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ 𝐸 = (dist‘𝐻) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐸 = (𝐷 ↾ (𝐵 × 𝐵))) | ||
Theorem | imasdsf1olem 22178* | Lemma for imasdsf1o 22179. (Contributed by Mario Carneiro, 21-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ 𝑊 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) & ⊢ 𝑆 = {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} & ⊢ 𝑇 = ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))) ⇒ ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌)) | ||
Theorem | imasdsf1o 22179 | The distance function is transferred across an image structure under a bijection. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌)) | ||
Theorem | imasf1oxmet 22180 | The image of an extended metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) | ||
Theorem | imasf1omet 22181 | The image of a metric is a metric. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ (Met‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) | ||
Theorem | xpsdsfn 22182 | Closure of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) ⇒ ⊢ (𝜑 → 𝑃 Fn ((𝑋 × 𝑌) × (𝑋 × 𝑌))) | ||
Theorem | xpsdsfn2 22183 | Closure of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) ⇒ ⊢ (𝜑 → 𝑃 Fn ((Base‘𝑇) × (Base‘𝑇))) | ||
Theorem | xpsxmetlem 22184* | Lemma for xpsxmet 22185. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) & ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) & ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) ⇒ ⊢ (𝜑 → (dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) | ||
Theorem | xpsxmet 22185 | A product metric of extended metrics is an extended metric. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) & ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) & ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌))) | ||
Theorem | xpsdsval 22186 | Value of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) & ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) & ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) | ||
Theorem | xpsmet 22187 | The direct product of two metric spaces. Definition 14-1.5 of [Gleason] p. 225. (Contributed by NM, 20-Jun-2007.) (Revised by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) & ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) & ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → 𝑀 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑌)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (Met‘(𝑋 × 𝑌))) | ||
Theorem | blfvalps 22188* | The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) | ||
Theorem | blfval 22189* | The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Proof shortened by Thierry Arnoux, 11-Feb-2018.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) | ||
Theorem | blvalps 22190* | The ball around a point 𝑃 is the set of all points whose distance from 𝑃 is less than the ball's radius 𝑅. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}) | ||
Theorem | blval 22191* | The ball around a point 𝑃 is the set of all points whose distance from 𝑃 is less than the ball's radius 𝑅. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}) | ||
Theorem | elblps 22192 | Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅))) | ||
Theorem | elbl 22193 | Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅))) | ||
Theorem | elbl2ps 22194 | Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅)) | ||
Theorem | elbl2 22195 | Membership in a ball. (Contributed by NM, 9-Mar-2007.) |
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅)) | ||
Theorem | elbl3ps 22196 | Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.) |
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) | ||
Theorem | elbl3 22197 | Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.) |
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) | ||
Theorem | blcomps 22198 | Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅))) | ||
Theorem | blcom 22199 | Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.) |
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅))) | ||
Theorem | xblpnfps 22200 | The infinity ball in an extended metric is the set of all points that are a finite distance from the center. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝐴 ∈ (𝑃(ball‘𝐷)+∞) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) ∈ ℝ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |