![]() |
Metamath
Proof Explorer Theorem List (p. 243 of 480) | < 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: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | setsmsbas 24201 | The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof shortened by AV, 12-Nov-2024.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) β β’ (π β π = (BaseβπΎ)) | ||
Theorem | setsmsbasOLD 24202 | Obsolete proof of setsmsbas 24201 as of 12-Nov-2024. The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) β β’ (π β π = (BaseβπΎ)) | ||
Theorem | setsmsds 24203 | The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof shortened by AV, 11-Nov-2024.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) β β’ (π β (distβπ) = (distβπΎ)) | ||
Theorem | setsmsdsOLD 24204 | Obsolete proof of setsmsds 24203 as of 11-Nov-2024. The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) β β’ (π β (distβπ) = (distβπΎ)) | ||
Theorem | setsmstset 24205 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) & β’ (π β π β π) β β’ (π β (MetOpenβπ·) = (TopSetβπΎ)) | ||
Theorem | setsmstopn 24206 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) & β’ (π β π β π) β β’ (π β (MetOpenβπ·) = (TopOpenβπΎ)) | ||
Theorem | setsxms 24207 | The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) & β’ (π β π β π) β β’ (π β (πΎ β βMetSp β π· β (βMetβπ))) | ||
Theorem | setsms 24208 | The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) & β’ (π β π β π) β β’ (π β (πΎ β MetSp β π· β (Metβπ))) | ||
Theorem | tmsval 24209 | For any metric there is an associated metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©} & β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) | ||
Theorem | tmslem 24210 | Lemma for tmsbas 24212, tmsds 24213, and tmstopn 24214. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©} & β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β (π = (BaseβπΎ) β§ π· = (distβπΎ) β§ (MetOpenβπ·) = (TopOpenβπΎ))) | ||
Theorem | tmslemOLD 24211 | Obsolete version of tmslem 24210 as of 28-Oct-2024. Lemma for tmsbas 24212, tmsds 24213, and tmstopn 24214. (Contributed by Mario Carneiro, 2-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©} & β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β (π = (BaseβπΎ) β§ π· = (distβπΎ) β§ (MetOpenβπ·) = (TopOpenβπΎ))) | ||
Theorem | tmsbas 24212 | The base set of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β π = (BaseβπΎ)) | ||
Theorem | tmsds 24213 | The metric of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β π· = (distβπΎ)) | ||
Theorem | tmstopn 24214 | The topology of a constructed metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) & β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ = (TopOpenβπΎ)) | ||
Theorem | tmsxms 24215 | The constructed metric space is an extended metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β πΎ β βMetSp) | ||
Theorem | tmsms 24216 | The constructed metric space is a metric space given a metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) β β’ (π· β (Metβπ) β πΎ β MetSp) | ||
Theorem | imasf1obl 24217 | The image of a metric space ball. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβ1-1-ontoβπ΅) & β’ (π β π β π) & β’ πΈ = ((distβπ ) βΎ (π Γ π)) & β’ π· = (distβπ) & β’ (π β πΈ β (βMetβπ)) & β’ (π β π β π) & β’ (π β π β β*) β β’ (π β ((πΉβπ)(ballβπ·)π) = (πΉ β (π(ballβπΈ)π))) | ||
Theorem | imasf1oxms 24218 | The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβ1-1-ontoβπ΅) & β’ (π β π β βMetSp) β β’ (π β π β βMetSp) | ||
Theorem | imasf1oms 24219 | The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβ1-1-ontoβπ΅) & β’ (π β π β MetSp) β β’ (π β π β MetSp) | ||
Theorem | prdsbl 24220* |
A ball in the product metric for finite index set is the Cartesian
product of balls in all coordinates. For infinite index set this is no
longer true; instead the correct statement is that a *closed ball* is
the product of closed balls in each coordinate (where closed ball means
a set of the form in blcld 24234) - for a counterexample the point π in
βββ whose π-th
coordinate is 1 β 1 / π is in
Xπ β βball(0, 1) but is not
in the 1-ball of the
product (since π(0, π) = 1).
The last assumption, 0 < π΄, is needed only in the case πΌ = β , when the right side evaluates to {β } and the left evaluates to β if π΄ β€ 0 and {β } if 0 < π΄. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXs(π₯ β πΌ β¦ π )) & β’ π΅ = (Baseβπ) & β’ π = (Baseβπ ) & β’ πΈ = ((distβπ ) βΎ (π Γ π)) & β’ π· = (distβπ) & β’ (π β π β π) & β’ (π β πΌ β Fin) & β’ ((π β§ π₯ β πΌ) β π β π) & β’ ((π β§ π₯ β πΌ) β πΈ β (βMetβπ)) & β’ (π β π β π΅) & β’ (π β π΄ β β*) & β’ (π β 0 < π΄) β β’ (π β (π(ballβπ·)π΄) = Xπ₯ β πΌ ((πβπ₯)(ballβπΈ)π΄)) | ||
Theorem | mopni 24221* | An open set of a metric space includes a ball around each of its points. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΄ β π½ β§ π β π΄) β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄)) | ||
Theorem | mopni2 24222* | An open set of a metric space includes a ball around each of its points. (Contributed by NM, 2-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΄ β π½ β§ π β π΄) β βπ₯ β β+ (π(ballβπ·)π₯) β π΄) | ||
Theorem | mopni3 24223* | An open set of a metric space includes an arbitrarily small ball around each of its points. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
β’ π½ = (MetOpenβπ·) β β’ (((π· β (βMetβπ) β§ π΄ β π½ β§ π β π΄) β§ π β β+) β βπ₯ β β+ (π₯ < π β§ (π(ballβπ·)π₯) β π΄)) | ||
Theorem | blssopn 24224 | The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β ran (ballβπ·) β π½) | ||
Theorem | unimopn 24225 | The union of a collection of open sets of a metric space is open. Theorem T2 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΄ β π½) β βͺ π΄ β π½) | ||
Theorem | mopnin 24226 | The intersection of two open sets of a metric space is open. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΄ β π½ β§ π΅ β π½) β (π΄ β© π΅) β π½) | ||
Theorem | mopn0 24227 | The empty set is an open set of a metric space. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β β β π½) | ||
Theorem | rnblopn 24228 | A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΅ β ran (ballβπ·)) β π΅ β π½) | ||
Theorem | blopn 24229 | A ball of a metric space is an open set. (Contributed by NM, 9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π ) β π½) | ||
Theorem | neibl 24230* | The neighborhoods around a point π of a metric space are those subsets containing a ball around π. Definition of neighborhood in [Kreyszig] p. 19. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π β π) β (π β ((neiβπ½)β{π}) β (π β π β§ βπ β β+ (π(ballβπ·)π) β π))) | ||
Theorem | blnei 24231 | A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π β π β§ π β β+) β (π(ballβπ·)π ) β ((neiβπ½)β{π})) | ||
Theorem | lpbl 24232* | Every ball around a limit point π of a subset π includes a member of π (even if π β π). (Contributed by NM, 9-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π½ = (MetOpenβπ·) β β’ (((π· β (βMetβπ) β§ π β π β§ π β ((limPtβπ½)βπ)) β§ π β β+) β βπ₯ β π π₯ β (π(ballβπ·)π )) | ||
Theorem | blsscls2 24233* | A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ π = {π§ β π β£ (ππ·π§) β€ π } β β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β* β§ π β β* β§ π < π)) β π β (π(ballβπ·)π)) | ||
Theorem | blcld 24234* | A "closed ball" in a metric space is actually closed. (Contributed by Mario Carneiro, 31-Dec-2013.) (Revised by Mario Carneiro, 24-Aug-2015.) |
β’ π½ = (MetOpenβπ·) & β’ π = {π§ β π β£ (ππ·π§) β€ π } β β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β π β (Clsdβπ½)) | ||
Theorem | blcls 24235* | The closure of an open ball in a metric space is contained in the corresponding closed ball. (Equality need not hold; for example, with the discrete metric, the closed ball of radius 1 is the whole space, but the open ball of radius 1 is just a point, whose closure is also a point.) (Contributed by Mario Carneiro, 31-Dec-2013.) |
β’ π½ = (MetOpenβπ·) & β’ π = {π§ β π β£ (ππ·π§) β€ π } β β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β ((clsβπ½)β(π(ballβπ·)π )) β π) | ||
Theorem | blsscls 24236 | If two concentric balls have different radii, the closure of the smaller one is contained in the larger one. (Contributed by Mario Carneiro, 5-Jan-2014.) |
β’ π½ = (MetOpenβπ·) β β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β* β§ π β β* β§ π < π)) β ((clsβπ½)β(π(ballβπ·)π )) β (π(ballβπ·)π)) | ||
Theorem | metss 24237* | Two ways of saying that metric π· generates a finer topology than metric πΆ. (Contributed by Mario Carneiro, 12-Nov-2013.) (Revised by Mario Carneiro, 24-Aug-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β (π½ β πΎ β βπ₯ β π βπ β β+ βπ β β+ (π₯(ballβπ·)π ) β (π₯(ballβπΆ)π))) | ||
Theorem | metequiv 24238* | Two ways of saying that two metrics generate the same topology. Two metrics satisfying the right-hand side are said to be (topologically) equivalent. (Contributed by Jeff Hankins, 21-Jun-2009.) (Revised by Mario Carneiro, 12-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β (π½ = πΎ β βπ₯ β π (βπ β β+ βπ β β+ (π₯(ballβπ·)π ) β (π₯(ballβπΆ)π) β§ βπ β β+ βπ β β+ (π₯(ballβπΆ)π) β (π₯(ballβπ·)π)))) | ||
Theorem | metequiv2 24239* | If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β (βπ₯ β π βπ β β+ βπ β β+ (π β€ π β§ (π₯(ballβπΆ)π ) = (π₯(ballβπ·)π )) β π½ = πΎ)) | ||
Theorem | metss2lem 24240* | Lemma for metss2 24241. (Contributed by Mario Carneiro, 14-Sep-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) β β’ ((π β§ (π₯ β π β§ π β β+)) β (π₯(ballβπ·)(π / π )) β (π₯(ballβπΆ)π)) | ||
Theorem | metss2 24241* | If the metric π· is "strongly finer" than πΆ (meaning that there is a positive real constant π such that πΆ(π₯, π¦) β€ π Β· π·(π₯, π¦)), then π· generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) β β’ (π β π½ β πΎ) | ||
Theorem | comet 24242* | The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π β π· β (βMetβπ)) & β’ (π β πΉ:(0[,]+β)βΆβ*) & β’ ((π β§ π₯ β (0[,]+β)) β ((πΉβπ₯) = 0 β π₯ = 0)) & β’ ((π β§ (π₯ β (0[,]+β) β§ π¦ β (0[,]+β))) β (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) & β’ ((π β§ (π₯ β (0[,]+β) β§ π¦ β (0[,]+β))) β (πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) β β’ (π β (πΉ β π·) β (βMetβπ)) | ||
Theorem | stdbdmetval 24243* | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π , (π₯πΆπ¦), π )) β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = if((π΄πΆπ΅) β€ π , (π΄πΆπ΅), π )) | ||
Theorem | stdbdxmet 24244* | The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π , (π₯πΆπ¦), π )) β β’ ((πΆ β (βMetβπ) β§ π β β* β§ 0 < π ) β π· β (βMetβπ)) | ||
Theorem | stdbdmet 24245* | The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π , (π₯πΆπ¦), π )) β β’ ((πΆ β (βMetβπ) β§ π β β+) β π· β (Metβπ)) | ||
Theorem | stdbdbl 24246* | The standard bounded metric corresponding to πΆ generates the same balls as πΆ for radii less than π . (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π , (π₯πΆπ¦), π )) β β’ (((πΆ β (βMetβπ) β§ π β β* β§ 0 < π ) β§ (π β π β§ π β β* β§ π β€ π )) β (π(ballβπ·)π) = (π(ballβπΆ)π)) | ||
Theorem | stdbdmopn 24247* | The standard bounded metric corresponding to πΆ generates the same topology as πΆ. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π , (π₯πΆπ¦), π )) & β’ π½ = (MetOpenβπΆ) β β’ ((πΆ β (βMetβπ) β§ π β β* β§ 0 < π ) β π½ = (MetOpenβπ·)) | ||
Theorem | mopnex 24248* | The topology generated by an extended metric can also be generated by a true metric. Thus, "metrizable topologies" can equivalently be defined in terms of metrics or extended metrics. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β βπ β (Metβπ)π½ = (MetOpenβπ)) | ||
Theorem | methaus 24249 | The topology generated by a metric space is Hausdorff. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ β Haus) | ||
Theorem | met1stc 24250 | The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ β 1stΟ) | ||
Theorem | met2ndci 24251 | A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β π½ β 2ndΟ) | ||
Theorem | met2ndc 24252* | A metric space is second-countable iff it is separable (has a countable dense subset). (Contributed by Mario Carneiro, 13-Apr-2015.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β (π½ β 2ndΟ β βπ₯ β π« π(π₯ βΌ Ο β§ ((clsβπ½)βπ₯) = π))) | ||
Theorem | metrest 24253 | Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.) |
β’ π· = (πΆ βΎ (π Γ π)) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π β π) β (π½ βΎt π) = πΎ) | ||
Theorem | ressxms 24254 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((πΎ β βMetSp β§ π΄ β π) β (πΎ βΎs π΄) β βMetSp) | ||
Theorem | ressms 24255 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((πΎ β MetSp β§ π΄ β π) β (πΎ βΎs π΄) β MetSp) | ||
Theorem | prdsmslem1 24256 | Lemma for prdsms 24260. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β Fin) & β’ π· = (distβπ) & β’ π΅ = (Baseβπ) & β’ (π β π :πΌβΆMetSp) β β’ (π β π· β (Metβπ΅)) | ||
Theorem | prdsxmslem1 24257 | Lemma for prdsms 24260. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β Fin) & β’ π· = (distβπ) & β’ π΅ = (Baseβπ) & β’ (π β π :πΌβΆβMetSp) β β’ (π β π· β (βMetβπ΅)) | ||
Theorem | prdsxmslem2 24258* | Lemma for prdsxms 24259. The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β Fin) & β’ π· = (distβπ) & β’ π΅ = (Baseβπ) & β’ (π β π :πΌβΆβMetSp) & β’ π½ = (TopOpenβπ) & β’ π = (Baseβ(π βπ)) & β’ πΈ = ((distβ(π βπ)) βΎ (π Γ π)) & β’ πΎ = (TopOpenβ(π βπ)) & β’ πΆ = {π₯ β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π )βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen β π )βπ)) β§ π₯ = Xπ β πΌ (πβπ))} β β’ (π β π½ = (MetOpenβπ·)) | ||
Theorem | prdsxms 24259 | The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) β β’ ((π β π β§ πΌ β Fin β§ π :πΌβΆβMetSp) β π β βMetSp) | ||
Theorem | prdsms 24260 | The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) β β’ ((π β π β§ πΌ β Fin β§ π :πΌβΆMetSp) β π β MetSp) | ||
Theorem | pwsxms 24261 | A power of an extended metric space is an extended metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π βs πΌ) β β’ ((π β βMetSp β§ πΌ β Fin) β π β βMetSp) | ||
Theorem | pwsms 24262 | A power of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π βs πΌ) β β’ ((π β MetSp β§ πΌ β Fin) β π β MetSp) | ||
Theorem | xpsxms 24263 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β βMetSp β§ π β βMetSp) β π β βMetSp) | ||
Theorem | xpsms 24264 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β MetSp β§ π β MetSp) β π β MetSp) | ||
Theorem | tmsxps 24265 | Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) β β’ (π β π β (βMetβ(π Γ π))) | ||
Theorem | tmsxpsmopn 24266 | Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ π½ = (MetOpenβπ) & β’ πΎ = (MetOpenβπ) & β’ πΏ = (MetOpenβπ) β β’ (π β πΏ = (π½ Γt πΎ)) | ||
Theorem | tmsxpsval 24267 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (β¨π΄, π΅β©πβ¨πΆ, π·β©) = sup({(π΄ππΆ), (π΅ππ·)}, β*, < )) | ||
Theorem | tmsxpsval2 24268 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (β¨π΄, π΅β©πβ¨πΆ, π·β©) = if((π΄ππΆ) β€ (π΅ππ·), (π΅ππ·), (π΄ππΆ))) | ||
Theorem | metcnp3 24269* | Two ways to express that πΉ is continuous at π for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)))) | ||
Theorem | metcnp 24270* | Two ways to say a mapping from metric πΆ to metric π· is continuous at point π. (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+ βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) | ||
Theorem | metcnp2 24271* | Two ways to say a mapping from metric πΆ to metric π· is continuous at point π. The distance arguments are swapped compared to metcnp 24270 (and Munkres' metcn 24272) for compatibility with df-lm 22953. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+ βπ€ β π ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦)))) | ||
Theorem | metcn 24272* | Two ways to say a mapping from metric πΆ to metric π· is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" π¦ there is a positive "delta" π§ such that a distance less than delta in πΆ maps to a distance less than epsilon in π·. (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π βπ¦ β β+ βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πΉβπ₯)π·(πΉβπ€)) < π¦)))) | ||
Theorem | metcnpi 24273* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 24270. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β βπ₯ β β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π΄)) | ||
Theorem | metcnpi2 24274* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 24271. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β βπ₯ β β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π΄)) | ||
Theorem | metcnpi3 24275* | Epsilon-delta property of a metric space function continuous at π. A variation of metcnpi2 24274 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β βπ₯ β β+ βπ¦ β π ((π¦πΆπ) β€ π₯ β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) | ||
Theorem | txmetcnp 24276* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ πΏ = (MetOpenβπΈ) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β (πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©) β (πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+ βπ’ β π βπ£ β π (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§)))) | ||
Theorem | txmetcn 24277* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ πΏ = (MetOpenβπΈ) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β (πΉ β ((π½ Γt πΎ) Cn πΏ) β (πΉ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β β+ βπ€ β β+ βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§)))) | ||
Theorem | metuval 24278* | Value of the uniform structure generated by metric π·. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ (π· β (PsMetβπ) β (metUnifβπ·) = ((π Γ π)filGenran (π β β+ β¦ (β‘π· β (0[,)π))))) | ||
Theorem | metustel 24279* | Define a filter base πΉ generated by a metric π·. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ (π· β (PsMetβπ) β (π΅ β πΉ β βπ β β+ π΅ = (β‘π· β (0[,)π)))) | ||
Theorem | metustss 24280* | Range of the elements of the filter base generated by the metric π·. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β π΄ β (π Γ π)) | ||
Theorem | metustrel 24281* | Elements of the filter base generated by the metric π· are relations. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β Rel π΄) | ||
Theorem | metustto 24282* | Any two elements of the filter base generated by the metric π· can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ β§ π΅ β πΉ) β (π΄ β π΅ β¨ π΅ β π΄)) | ||
Theorem | metustid 24283* | The identity diagonal is included in all elements of the filter base generated by the metric π·. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β ( I βΎ π) β π΄) | ||
Theorem | metustsym 24284* | Elements of the filter base generated by the metric π· are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β β‘π΄ = π΄) | ||
Theorem | metustexhalf 24285* | For any element π΄ of the filter base generated by the metric π·, the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ (((π β β β§ π· β (PsMetβπ)) β§ π΄ β πΉ) β βπ£ β πΉ (π£ β π£) β π΄) | ||
Theorem | metustfbas 24286* | The filter base generated by a metric π·. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π β β β§ π· β (PsMetβπ)) β πΉ β (fBasβ(π Γ π))) | ||
Theorem | metust 24287* | The uniform structure generated by a metric π·. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π β β β§ π· β (PsMetβπ)) β ((π Γ π)filGenπΉ) β (UnifOnβπ)) | ||
Theorem | cfilucfil 24288* | Given a metric π· and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 25013. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π β β β§ π· β (PsMetβπ)) β (πΆ β (CauFiluβ((π Γ π)filGenπΉ)) β (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | metuust 24289 | The uniform structure generated by metric π· is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (PsMetβπ)) β (metUnifβπ·) β (UnifOnβπ)) | ||
Theorem | cfilucfil2 24290* | Given a metric π· and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 25013. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (PsMetβπ)) β (πΆ β (CauFiluβ(metUnifβπ·)) β (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | blval2 24291 | The ball around a point π, alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
β’ ((π· β (PsMetβπ) β§ π β π β§ π β β+) β (π(ballβπ·)π ) = ((β‘π· β (0[,)π )) β {π})) | ||
Theorem | elbl4 24292 | Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
β’ (((π· β (PsMetβπ) β§ π β β+) β§ (π΄ β π β§ π΅ β π)) β (π΅ β (π΄(ballβπ·)π ) β π΅(β‘π· β (0[,)π ))π΄)) | ||
Theorem | metuel 24293* | Elementhood in the uniform structure generated by a metric π· (Contributed by Thierry Arnoux, 8-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (PsMetβπ)) β (π β (metUnifβπ·) β (π β (π Γ π) β§ βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π))) | ||
Theorem | metuel2 24294* | Elementhood in the uniform structure generated by a metric π· (Contributed by Thierry Arnoux, 24-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ π = (metUnifβπ·) β β’ ((π β β β§ π· β (PsMetβπ)) β (π β π β (π β (π Γ π) β§ βπ β β+ βπ₯ β π βπ¦ β π ((π₯π·π¦) < π β π₯ππ¦)))) | ||
Theorem | metustbl 24295* | The "section" image of an entourage at a point π always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017.) |
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β βπ β ran (ballβπ·)(π β π β§ π β (π β {π}))) | ||
Theorem | psmetutop 24296 | The topology induced by a uniform structure generated by a metric π· is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
β’ ((π β β β§ π· β (PsMetβπ)) β (unifTopβ(metUnifβπ·)) = (topGenβran (ballβπ·))) | ||
Theorem | xmetutop 24297 | The topology induced by a uniform structure generated by an extended metric π· is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018.) |
β’ ((π β β β§ π· β (βMetβπ)) β (unifTopβ(metUnifβπ·)) = (MetOpenβπ·)) | ||
Theorem | xmsusp 24298 | If the uniform set of a metric space is the uniform structure generated by its metric, then it is a uniform space. (Contributed by Thierry Arnoux, 14-Dec-2017.) |
β’ π = (BaseβπΉ) & β’ π· = ((distβπΉ) βΎ (π Γ π)) & β’ π = (UnifStβπΉ) β β’ ((π β β β§ πΉ β βMetSp β§ π = (metUnifβπ·)) β πΉ β UnifSp) | ||
Theorem | restmetu 24299 | The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017.) |
β’ ((π΄ β β β§ π· β (PsMetβπ) β§ π΄ β π) β ((metUnifβπ·) βΎt (π΄ Γ π΄)) = (metUnifβ(π· βΎ (π΄ Γ π΄)))) | ||
Theorem | metucn 24300* | Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 24272. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ π = (metUnifβπΆ) & β’ π = (metUnifβπ·) & β’ (π β π β β ) & β’ (π β π β β ) & β’ (π β πΆ β (PsMetβπ)) & β’ (π β π· β (PsMetβπ)) β β’ (π β (πΉ β (π Cnuπ) β (πΉ:πβΆπ β§ βπ β β+ βπ β β+ βπ₯ β π βπ¦ β π ((π₯πΆπ¦) < π β ((πΉβπ₯)π·(πΉβπ¦)) < π)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |