Home | Metamath
Proof Explorer Theorem List (p. 222 of 426) | < Previous Next > |
Browser slow? Try the
Unicode 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. |
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 CauFiluUnifSt | ||
Theorem | iscusp 22103* | The predicate " is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017.) |
CUnifSp UnifSp CauFiluUnifSt | ||
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.) |
CUnifSp CauFiluUnifSt | ||
Theorem | iscusp2 22106* | The predicate " is a complete uniform space." (Contributed by Thierry Arnoux, 15-Dec-2017.) |
UnifSt CUnifSp UnifSp CauFilu | ||
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.) |
UnifSt CUnifSp ↾t CauFilu CnExt | ||
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.) |
UnifSt UnifSt ↾s UnifSt UnifSp CUnifSp Cnu CnExt | ||
Theorem | ispsmet 22109* | Express the predicate " is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
Theorem | psmetdmdm 22110 | Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
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 | ||
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 | ||
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 | ||
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.) |
PsMet | ||
Syntax | cxme 22122 | Extend class notation with the class of all extended metric spaces. |
Syntax | cmt 22123 | Extend class notation with the class of all metric spaces. |
Syntax | ctmt 22124 | Extend class notation with the function mapping a metric to a metric space. |
toMetSp | ||
Definition | df-xms 22125 | Define the (proper) class of all extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
Definition | df-ms 22126 | Define the (proper) class of all metric spaces. (Contributed by NM, 27-Aug-2006.) |
Definition | df-tms 22127 | Define the function mapping a metric to a metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
toMetSp sSet TopSet | ||
Theorem | ismet 22128* | Express the predicate " is a metric." (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Theorem | isxmet 22129* | Express the predicate " is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | ismeti 22130* | Properties that determine a metric. (Contributed by NM, 17-Nov-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Theorem | isxmetd 22131* | Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
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: satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | metflem 22133* | Lemma for metf 22135 and others. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Theorem | xmetf 22134 | Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | metf 22135 | Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) |
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.) |
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.) |
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.) |
Theorem | metxmet 22139 | A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmetdmdm 22140 | Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015.) |
Theorem | metdmdm 22141 | Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.) |
Theorem | xmetunirn 22142 | Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
Theorem | xmeteq0 22143 | The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015.) |
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.) |
Theorem | xmettri2 22145 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
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.) |
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.) |
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.) |
Theorem | xmetge0 22149 | The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
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.) |
Theorem | xmetlecl 22151 | Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmetsym 22152 | The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmetpsmet 22153 | An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet | ||
Theorem | xmettpos 22154 | The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
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.) |
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.) |
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.) |
Theorem | xmettri3 22158 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | mettri3 22159 | Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007.) |
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.) |
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.) |
Theorem | metrtri 22162 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.) |
Theorem | xmetgt0 22163 | The distance function of an extended metric space is positive for unequal points. (Contributed by Mario Carneiro, 20-Aug-2015.) |
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.) |
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.) |
Theorem | xmetres2 22166 | Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | metreslem 22167 | Lemma for metres 22170. (Contributed by Mario Carneiro, 24-Aug-2015.) |
Theorem | metres2 22168 | Lemma for metres 22170. (Contributed by FL, 12-Oct-2006.) (Proof shortened by Mario Carneiro, 14-Aug-2015.) |
Theorem | xmetres 22169 | A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015.) |
Theorem | metres 22170 | A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Theorem | 0met 22171 | The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.) |
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.) |
s | ||
Theorem | prdsxmetlem 22173* | The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
Theorem | prdsxmet 22174* | The product metric is an extended metric. Eliminate disjoint variable conditions from prdsxmetlem 22173. (Contributed by Mario Carneiro, 26-Sep-2015.) |
s | ||
Theorem | prdsmet 22175* | The product metric is a metric when the index set is finite. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
Theorem | ressprdsds 22176* | Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015.) |
s s ↾s | ||
Theorem | resspwsds 22177 | Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015.) |
s ↾s s | ||
Theorem | imasdsf1olem 22178* | Lemma for imasdsf1o 22179. (Contributed by Mario Carneiro, 21-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.) |
s ↾s g | ||
Theorem | imasdsf1o 22179 | The distance function is transferred across an image structure under a bijection. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
Theorem | imasf1oxmet 22180 | The image of an extended metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
Theorem | imasf1omet 22181 | The image of a metric is a metric. (Contributed by Mario Carneiro, 21-Aug-2015.) |
s | ||
Theorem | xpsdsfn 22182 | Closure of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
Theorem | xpsdsfn2 22183 | Closure of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
Theorem | xpsxmetlem 22184* | Lemma for xpsxmet 22185. (Contributed by Mario Carneiro, 21-Aug-2015.) |
s Scalars | ||
Theorem | xpsxmet 22185 | A product metric of extended metrics is an extended metric. (Contributed by Mario Carneiro, 21-Aug-2015.) |
s | ||
Theorem | xpsdsval 22186 | Value of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
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 | ||
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 | ||
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.) |
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 | ||
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.) |
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 | ||
Theorem | elbl 22193 | Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
Theorem | elbl2ps 22194 | Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | elbl2 22195 | Membership in a ball. (Contributed by NM, 9-Mar-2007.) |
Theorem | elbl3ps 22196 | Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.) |
PsMet | ||
Theorem | elbl3 22197 | Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.) |
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 | ||
Theorem | blcom 22199 | Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.) |
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 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |