![]() |
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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mspropd 24201 | Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β MetSp β πΏ β MetSp)) | ||
Theorem | setsmsbas 24202 | 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 24203 | Obsolete proof of setsmsbas 24202 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 24204 | 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 24205 | Obsolete proof of setsmsds 24204 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 24206 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) & β’ (π β π β π) β β’ (π β (MetOpenβπ·) = (TopSetβπΎ)) | ||
Theorem | setsmstopn 24207 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) & β’ (π β π β π) β β’ (π β (MetOpenβπ·) = (TopOpenβπΎ)) | ||
Theorem | setsxms 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 | setsms 24209 | 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 24210 | 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 24211 | Lemma for tmsbas 24213, tmsds 24214, and tmstopn 24215. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = {β¨(Baseβndx), πβ©, β¨(distβndx), π·β©} & β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β (π = (BaseβπΎ) β§ π· = (distβπΎ) β§ (MetOpenβπ·) = (TopOpenβπΎ))) | ||
Theorem | tmslemOLD 24212 | Obsolete version of tmslem 24211 as of 28-Oct-2024. Lemma for tmsbas 24213, tmsds 24214, and tmstopn 24215. (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 24213 | The base set of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β π = (BaseβπΎ)) | ||
Theorem | tmsds 24214 | The metric of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β π· = (distβπΎ)) | ||
Theorem | tmstopn 24215 | The topology of a constructed metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) & β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ = (TopOpenβπΎ)) | ||
Theorem | tmsxms 24216 | The constructed metric space is an extended metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) β β’ (π· β (βMetβπ) β πΎ β βMetSp) | ||
Theorem | tmsms 24217 | The constructed metric space is a metric space given a metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ πΎ = (toMetSpβπ·) β β’ (π· β (Metβπ) β πΎ β MetSp) | ||
Theorem | imasf1obl 24218 | 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 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 | imasf1oms 24220 | 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 24221* |
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 24235) - 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 24222* | 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 24223* | 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 24224* | 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 24225 | 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 24226 | 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 24227 | 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 24228 | 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 24229 | A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΅ β ran (ballβπ·)) β π΅ β π½) | ||
Theorem | blopn 24230 | 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 24231* | 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 24232 | 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 24233* | 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 24234* | A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ π = {π§ β π β£ (ππ·π§) β€ π } β β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β* β§ π β β* β§ π < π)) β π β (π(ballβπ·)π)) | ||
Theorem | blcld 24235* | 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 24236* | 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 24237 | 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 24238* | 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 24239* | 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 24240* | 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 24241* | Lemma for metss2 24242. (Contributed by Mario Carneiro, 14-Sep-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) β β’ ((π β§ (π₯ β π β§ π β β+)) β (π₯(ballβπ·)(π / π )) β (π₯(ballβπΆ)π)) | ||
Theorem | metss2 24242* | 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 24243* | 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 24244* | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π , (π₯πΆπ¦), π )) β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = if((π΄πΆπ΅) β€ π , (π΄πΆπ΅), π )) | ||
Theorem | stdbdxmet 24245* | 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 24246* | 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 24247* | 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 24248* | 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 24249* | 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 24250 | 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 24251 | The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ β 1stΟ) | ||
Theorem | met2ndci 24252 | 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 24253* | 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 24254 | 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 24255 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((πΎ β βMetSp β§ π΄ β π) β (πΎ βΎs π΄) β βMetSp) | ||
Theorem | ressms 24256 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((πΎ β MetSp β§ π΄ β π) β (πΎ βΎs π΄) β MetSp) | ||
Theorem | prdsmslem1 24257 | Lemma for prdsms 24261. 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 24258 | Lemma for prdsms 24261. 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 24259* | Lemma for prdsxms 24260. 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 24260 | 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 24261 | 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 24262 | 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 24263 | A power of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π βs πΌ) β β’ ((π β MetSp β§ πΌ β Fin) β π β MetSp) | ||
Theorem | xpsxms 24264 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β βMetSp β§ π β βMetSp) β π β βMetSp) | ||
Theorem | xpsms 24265 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β MetSp β§ π β MetSp) β π β MetSp) | ||
Theorem | tmsxps 24266 | 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 24267 | 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 24268 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (β¨π΄, π΅β©πβ¨πΆ, π·β©) = sup({(π΄ππΆ), (π΅ππ·)}, β*, < )) | ||
Theorem | tmsxpsval2 24269 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (β¨π΄, π΅β©πβ¨πΆ, π·β©) = if((π΄ππΆ) β€ (π΅ππ·), (π΅ππ·), (π΄ππΆ))) | ||
Theorem | metcnp3 24270* | 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 24271* | 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 24272* | Two ways to say a mapping from metric πΆ to metric π· is continuous at point π. The distance arguments are swapped compared to metcnp 24271 (and Munkres' metcn 24273) for compatibility with df-lm 22954. 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 24273* | 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 24274* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 24271. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β βπ₯ β β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π΄)) | ||
Theorem | metcnpi2 24275* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 24272. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β βπ₯ β β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π΄)) | ||
Theorem | metcnpi3 24276* | Epsilon-delta property of a metric space function continuous at π. A variation of metcnpi2 24275 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β βπ₯ β β+ βπ¦ β π ((π¦πΆπ) β€ π₯ β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) | ||
Theorem | txmetcnp 24277* | 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 24278* | 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 24279* | 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 24280* | 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 24281* | 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 24282* | 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 24283* | 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 24284* | 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 24285* | 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 24286* | 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 24287* | 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 24288* | 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 24289* | 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 25014. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π β β β§ π· β (PsMetβπ)) β (πΆ β (CauFiluβ((π Γ π)filGenπΉ)) β (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | metuust 24290 | 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 24291* | 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 25014. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (PsMetβπ)) β (πΆ β (CauFiluβ(metUnifβπ·)) β (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | blval2 24292 | 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 24293 | 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 24294* | 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 24295* | 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 24296* | 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 24297 | 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 24298 | 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 24299 | 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 24300 | The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017.) |
β’ ((π΄ β β β§ π· β (PsMetβπ) β§ π΄ β π) β ((metUnifβπ·) βΎt (π΄ Γ π΄)) = (metUnifβ(π· βΎ (π΄ Γ π΄)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |