HomeTheorem List (p. 144 of 153)
GIF version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 144 of 153) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | xblpnfps 14301 | 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βπ·)+β) β (π΄ β π β§ (ππ·π΄) β β))) | ||
| Theorem | xblpnf 14302 | 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.) |
| β’ ((π· β (βMetβπ) β§ π β π) β (π΄ β (π(ballβπ·)+β) β (π΄ β π β§ (ππ·π΄) β β))) | ||
| Theorem | blpnf 14303 | The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| β’ ((π· β (Metβπ) β§ π β π) β (π(ballβπ·)+β) = π) | ||
| Theorem | bldisj 14304 | Two balls are disjoint if the center-to-center distance is more than the sum of the radii. (Contributed by Mario Carneiro, 30-Dec-2013.) |
| β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π β β* β§ π β β* β§ (π +π π) β€ (ππ·π))) β ((π(ballβπ·)π ) β© (π(ballβπ·)π)) = β ) | ||
| Theorem | blgt0 14305 | A nonempty ball implies that the radius is positive. (Contributed by NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| β’ (((π· β (βMetβπ) β§ π β π β§ π β β*) β§ π΄ β (π(ballβπ·)π )) β 0 < π ) | ||
| Theorem | bl2in 14306 | Two balls are disjoint if they don't overlap. (Contributed by NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π β β β§ π β€ ((ππ·π) / 2))) β ((π(ballβπ·)π ) β© (π(ballβπ·)π )) = β ) | ||
| Theorem | xblss2ps 14307 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 14310 for extended metrics, we have to assume the balls are a finite distance apart, or else π will not even be in the infinity ball around π. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ (π β π· β (PsMetβπ)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β β*) & β’ (π β π β β*) & β’ (π β (ππ·π) β β) & β’ (π β (ππ·π) β€ (π +π -ππ )) β β’ (π β (π(ballβπ·)π ) β (π(ballβπ·)π)) | ||
| Theorem | xblss2 14308 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 14310 for extended metrics, we have to assume the balls are a finite distance apart, or else π will not even be in the infinity ball around π. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| β’ (π β π· β (βMetβπ)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β β*) & β’ (π β π β β*) & β’ (π β (ππ·π) β β) & β’ (π β (ππ·π) β€ (π +π -ππ )) β β’ (π β (π(ballβπ·)π ) β (π(ballβπ·)π)) | ||
| Theorem | blss2ps 14309 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ (((π· β (PsMetβπ) β§ π β π β§ π β π) β§ (π β β β§ π β β β§ (ππ·π) β€ (π β π ))) β (π(ballβπ·)π ) β (π(ballβπ·)π)) | ||
| Theorem | blss2 14310 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π β β β§ π β β β§ (ππ·π) β€ (π β π ))) β (π(ballβπ·)π ) β (π(ballβπ·)π)) | ||
| Theorem | blhalf 14311 | A ball of radius π / 2 is contained in a ball of radius π centered at any point inside the smaller ball. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jan-2014.) |
| β’ (((π β (βMetβπ) β§ π β π) β§ (π β β β§ π β (π(ballβπ)(π / 2)))) β (π(ballβπ)(π / 2)) β (π(ballβπ)π )) | ||
| Theorem | blfps 14312 | Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ (π· β (PsMetβπ) β (ballβπ·):(π Γ β*)βΆπ« π) | ||
| Theorem | blf 14313 | Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| β’ (π· β (βMetβπ) β (ballβπ·):(π Γ β*)βΆπ« π) | ||
| Theorem | blrnps 14314* | Membership in the range of the ball function. Note that ran (ballβπ·) is the collection of all balls for metric π·. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ (π· β (PsMetβπ) β (π΄ β ran (ballβπ·) β βπ₯ β π βπ β β* π΄ = (π₯(ballβπ·)π))) | ||
| Theorem | blrn 14315* | Membership in the range of the ball function. Note that ran (ballβπ·) is the collection of all balls for metric π·. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ (π· β (βMetβπ) β (π΄ β ran (ballβπ·) β βπ₯ β π βπ β β* π΄ = (π₯(ballβπ·)π))) | ||
| Theorem | xblcntrps 14316 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ ((π· β (PsMetβπ) β§ π β π β§ (π β β* β§ 0 < π )) β π β (π(ballβπ·)π )) | ||
| Theorem | xblcntr 14317 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ (π β β* β§ 0 < π )) β π β (π(ballβπ·)π )) | ||
| Theorem | blcntrps 14318 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ ((π· β (PsMetβπ) β§ π β π β§ π β β+) β π β (π(ballβπ·)π )) | ||
| Theorem | blcntr 14319 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ π β β+) β π β (π(ballβπ·)π )) | ||
| Theorem | xblm 14320* | A ball is inhabited iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (βπ₯ π₯ β (π(ballβπ·)π ) β 0 < π )) | ||
| Theorem | bln0 14321 | A ball is not empty. It is also inhabited, as seen at blcntr 14319. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ π β β+) β (π(ballβπ·)π ) β β ) | ||
| Theorem | blelrnps 14322 | A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ ((π· β (PsMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π ) β ran (ballβπ·)) | ||
| Theorem | blelrn 14323 | A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π ) β ran (ballβπ·)) | ||
| Theorem | blssm 14324 | A ball is a subset of the base set of a metric space. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π ) β π) | ||
| Theorem | unirnblps 14325 | The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ (π· β (PsMetβπ) β βͺ ran (ballβπ·) = π) | ||
| Theorem | unirnbl 14326 | The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ (π· β (βMetβπ) β βͺ ran (ballβπ·) = π) | ||
| Theorem | blininf 14327 | The intersection of two balls with the same center is the smaller of them. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β* β§ π β β*)) β ((π(ballβπ·)π ) β© (π(ballβπ·)π)) = (π(ballβπ·)inf({π , π}, β*, < ))) | ||
| Theorem | ssblps 14328 | The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ (((π· β (PsMetβπ) β§ π β π) β§ (π β β* β§ π β β*) β§ π β€ π) β (π(ballβπ·)π ) β (π(ballβπ·)π)) | ||
| Theorem | ssbl 14329 | The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) |
| β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β* β§ π β β*) β§ π β€ π) β (π(ballβπ·)π ) β (π(ballβπ·)π)) | ||
| Theorem | blssps 14330* | Any point π in a ball π΅ can be centered in another ball that is a subset of π΅. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ ((π· β (PsMetβπ) β§ π΅ β ran (ballβπ·) β§ π β π΅) β βπ₯ β β+ (π(ballβπ·)π₯) β π΅) | ||
| Theorem | blss 14331* | Any point π in a ball π΅ can be centered in another ball that is a subset of π΅. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) |
| β’ ((π· β (βMetβπ) β§ π΅ β ran (ballβπ·) β§ π β π΅) β βπ₯ β β+ (π(ballβπ·)π₯) β π΅) | ||
| Theorem | blssexps 14332* | Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| β’ ((π· β (PsMetβπ) β§ π β π) β (βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) | ||
| Theorem | blssex 14333* | Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ ((π· β (βMetβπ) β§ π β π) β (βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) | ||
| Theorem | ssblex 14334* | A nested ball exists whose radius is less than any desired amount. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β+ β§ π β β+)) β βπ₯ β β+ (π₯ < π β§ (π(ballβπ·)π₯) β (π(ballβπ·)π))) | ||
| Theorem | blin2 14335* | Given any two balls and a point in their intersection, there is a ball contained in the intersection with the given center point. (Contributed by Mario Carneiro, 12-Nov-2013.) |
| β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ)) | ||
| Theorem | blbas 14336 | The balls of a metric space form a basis for a topology. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 15-Jan-2014.) |
| β’ (π· β (βMetβπ) β ran (ballβπ·) β TopBases) | ||
| Theorem | blres 14337 | A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.) |
| β’ πΆ = (π· βΎ (π Γ π)) β β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π β β*) β (π(ballβπΆ)π ) = ((π(ballβπ·)π ) β© π)) | ||
| Theorem | xmeterval 14338 | Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| β’ βΌ = (β‘π· β β) β β’ (π· β (βMetβπ) β (π΄ βΌ π΅ β (π΄ β π β§ π΅ β π β§ (π΄π·π΅) β β))) | ||
| Theorem | xmeter 14339 | The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| β’ βΌ = (β‘π· β β) β β’ (π· β (βMetβπ) β βΌ Er π) | ||
| Theorem | xmetec 14340 | The equivalence classes under the finite separation equivalence relation are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| β’ βΌ = (β‘π· β β) β β’ ((π· β (βMetβπ) β§ π β π) β [π] βΌ = (π(ballβπ·)+β)) | ||
| Theorem | blssec 14341 | A ball centered at π is contained in the set of points finitely separated from π. This is just an application of ssbl 14329 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| β’ βΌ = (β‘π· β β) β β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π) β [π] βΌ ) | ||
| Theorem | blpnfctr 14342 | The infinity ball in an extended metric acts like an ultrametric ball in that every point in the ball is also its center. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β (π(ballβπ·)+β)) β (π(ballβπ·)+β) = (π΄(ballβπ·)+β)) | ||
| Theorem | xmetresbl 14343 | An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec 14340, this shows that any extended metric space can be "factored" into the disjoint union of proper metric spaces, with points in the same region measured by that region's metric, and points in different regions being distance +β from each other. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| β’ π΅ = (π(ballβπ·)π ) β β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π· βΎ (π΅ Γ π΅)) β (Metβπ΅)) | ||
| Theorem | mopnrel 14344 | The class of open sets of a metric space is a relation. (Contributed by Jim Kingdon, 5-May-2023.) |
| β’ Rel MetOpen | ||
| Theorem | mopnval 14345 | An open set is a subset of a metric space which includes a ball around each of its points. Definition 1.3-2 of [Kreyszig] p. 18. The object (MetOpenβπ·) is the family of all open sets in the metric space determined by the metric π·. By mopntop 14347, the open sets of a metric space form a topology π½, whose base set is βͺ π½ by mopnuni 14348. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ = (topGenβran (ballβπ·))) | ||
| Theorem | mopntopon 14346 | The set of open sets of a metric space π is a topology on π. Remark in [Kreyszig] p. 19. This theorem connects the two concepts and makes available the theorems for topologies for use with metric spaces. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) | ||
| Theorem | mopntop 14347 | The set of open sets of a metric space is a topology. (Contributed by NM, 28-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ β Top) | ||
| Theorem | mopnuni 14348 | The union of all open sets in a metric space is its underlying set. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π = βͺ π½) | ||
| Theorem | elmopn 14349* | The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β (π΄ β π½ β (π΄ β π β§ βπ₯ β π΄ βπ¦ β ran (ballβπ·)(π₯ β π¦ β§ π¦ β π΄)))) | ||
| Theorem | mopnfss 14350 | The family of open sets of a metric space is a collection of subsets of the base set. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ β π« π) | ||
| Theorem | mopnm 14351 | The base set of a metric space is open. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π β π½) | ||
| Theorem | elmopn2 14352* | A defining property of an open set of a metric space. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β (π΄ β π½ β (π΄ β π β§ βπ₯ β π΄ βπ¦ β β+ (π₯(ballβπ·)π¦) β π΄))) | ||
| Theorem | mopnss 14353 | An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.) |
| β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΄ β π½) β π΄ β π) | ||
| Theorem | isxms 14354 | Express the predicate "β¨π, π·β© is an extended metric space" with underlying set π and distance function π·. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| β’ π½ = (TopOpenβπΎ) & β’ π = (BaseβπΎ) & β’ π· = ((distβπΎ) βΎ (π Γ π)) β β’ (πΎ β βMetSp β (πΎ β TopSp β§ π½ = (MetOpenβπ·))) | ||
| Theorem | isxms2 14355 | Express the predicate "β¨π, π·β© is an extended metric space" with underlying set π and distance function π·. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| β’ π½ = (TopOpenβπΎ) & β’ π = (BaseβπΎ) & β’ π· = ((distβπΎ) βΎ (π Γ π)) β β’ (πΎ β βMetSp β (π· β (βMetβπ) β§ π½ = (MetOpenβπ·))) | ||
| Theorem | isms 14356 | Express the predicate "β¨π, π·β© is a metric space" with underlying set π and distance function π·. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) |
| β’ π½ = (TopOpenβπΎ) & β’ π = (BaseβπΎ) & β’ π· = ((distβπΎ) βΎ (π Γ π)) β β’ (πΎ β MetSp β (πΎ β βMetSp β§ π· β (Metβπ))) | ||
| Theorem | isms2 14357 | Express the predicate "β¨π, π·β© is a metric space" with underlying set π and distance function π·. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) |
| β’ π½ = (TopOpenβπΎ) & β’ π = (BaseβπΎ) & β’ π· = ((distβπΎ) βΎ (π Γ π)) β β’ (πΎ β MetSp β (π· β (Metβπ) β§ π½ = (MetOpenβπ·))) | ||
| Theorem | xmstopn 14358 | The topology component of an extended metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| β’ π½ = (TopOpenβπΎ) & β’ π = (BaseβπΎ) & β’ π· = ((distβπΎ) βΎ (π Γ π)) β β’ (πΎ β βMetSp β π½ = (MetOpenβπ·)) | ||
| Theorem | mstopn 14359 | The topology component of a metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| β’ π½ = (TopOpenβπΎ) & β’ π = (BaseβπΎ) & β’ π· = ((distβπΎ) βΎ (π Γ π)) β β’ (πΎ β MetSp β π½ = (MetOpenβπ·)) | ||
| Theorem | xmstps 14360 | An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| β’ (π β βMetSp β π β TopSp) | ||
| Theorem | msxms 14361 | A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| β’ (π β MetSp β π β βMetSp) | ||
| Theorem | mstps 14362 | A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| β’ (π β MetSp β π β TopSp) | ||
| Theorem | xmsxmet 14363 | The distance function, suitably truncated, is an extended metric on π. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β βMetSp β π· β (βMetβπ)) | ||
| Theorem | msmet 14364 | The distance function, suitably truncated, is a metric on π. (Contributed by Mario Carneiro, 12-Nov-2013.) |
| β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β MetSp β π· β (Metβπ)) | ||
| Theorem | msf 14365 | The distance function of a metric space is a function into the real numbers. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β MetSp β π·:(π Γ π)βΆβ) | ||
| Theorem | xmsxmet2 14366 | The distance function, suitably truncated, is an extended metric on π. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ (π β βMetSp β (π· βΎ (π Γ π)) β (βMetβπ)) | ||
| Theorem | msmet2 14367 | The distance function, suitably truncated, is a metric on π. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ (π β MetSp β (π· βΎ (π Γ π)) β (Metβπ)) | ||
| Theorem | mscl 14368 | Closure of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β MetSp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β β) | ||
| Theorem | xmscl 14369 | Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β β*) | ||
| Theorem | xmsge0 14370 | The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β 0 β€ (π΄π·π΅)) | ||
| Theorem | xmseq0 14371 | The distance between two points in an extended metric space is zero iff the two points are identical. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) = 0 β π΄ = π΅)) | ||
| Theorem | xmssym 14372 | The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΅π·π΄)) | ||
| Theorem | xmstri2 14373 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅))) | ||
| Theorem | mstri2 14374 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β MetSp β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) + (πΆπ·π΅))) | ||
| Theorem | xmstri 14375 | Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) +π (πΆπ·π΅))) | ||
| Theorem | mstri 14376 | Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β MetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) + (πΆπ·π΅))) | ||
| Theorem | xmstri3 14377 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) +π (π΅π·πΆ))) | ||
| Theorem | mstri3 14378 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β MetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) + (π΅π·πΆ))) | ||
| Theorem | msrtri 14379 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β MetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (absβ((π΄π·πΆ) β (π΅π·πΆ))) β€ (π΄π·π΅)) | ||
| Theorem | xmspropd 14380 | Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β βMetSp β πΏ β βMetSp)) | ||
| Theorem | mspropd 14381 | Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β MetSp β πΏ β MetSp)) | ||
| Theorem | setsmsbasg 14382 | The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) & β’ (π β π β π) & β’ (π β (MetOpenβπ·) β π) β β’ (π β π = (BaseβπΎ)) | ||
| Theorem | setsmsdsg 14383 | The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) & β’ (π β π β π) & β’ (π β (MetOpenβπ·) β π) β β’ (π β (distβπ) = (distβπΎ)) | ||
| Theorem | setsmstsetg 14384 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.) |
| β’ (π β π = (Baseβπ)) & β’ (π β π· = ((distβπ) βΎ (π Γ π))) & β’ (π β πΎ = (π sSet β¨(TopSetβndx), (MetOpenβπ·)β©)) & β’ (π β π β π) & β’ (π β (MetOpenβπ·) β π) β β’ (π β (MetOpenβπ·) = (TopSetβπΎ)) | ||
| Theorem | mopni 14385* | 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 14386* | 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 14387* | 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 14388 | 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 14389 | 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 14390 | 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 14391 | 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 14392 | A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.) |
| β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΅ β ran (ballβπ·)) β π΅ β π½) | ||
| Theorem | blopn 14393 | 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 14394* | 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 14395 | 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 | blsscls2 14396* | A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.) |
| β’ π½ = (MetOpenβπ·) & β’ π = {π§ β π β£ (ππ·π§) β€ π } β β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β* β§ π β β* β§ π < π)) β π β (π(ballβπ·)π)) | ||
| Theorem | metss 14397* | 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 14398* | 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 14399* | 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 14400* | Lemma for metss2 14401. (Contributed by Mario Carneiro, 14-Sep-2015.) |
| β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) β β’ ((π β§ (π₯ β π β§ π β β+)) β (π₯(ballβπ·)(π / π )) β (π₯(ballβπΆ)π)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |