HomeTheorem List (p. 140 of 149)
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. 140 of 149) | < 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 13901 | 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 13902 | 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 13903 | The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| β’ ((π· β (Metβπ) β§ π β π) β (π(ballβπ·)+β) = π) | ||
| Theorem | bldisj 13904 | 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 13905 | 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 13906 | 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 13907 | 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 13910 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 13908 | 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 13910 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 13909 | 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 13910 | 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 13911 | 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 13912 | 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 13913 | Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| β’ (π· β (βMetβπ) β (ballβπ·):(π Γ β*)βΆπ« π) | ||
| Theorem | blrnps 13914* | 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 13915* | 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 13916 | 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 13917 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ (π β β* β§ 0 < π )) β π β (π(ballβπ·)π )) | ||
| Theorem | blcntrps 13918 | 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 13919 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ π β β+) β π β (π(ballβπ·)π )) | ||
| Theorem | xblm 13920* | A ball is inhabited iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (βπ₯ π₯ β (π(ballβπ·)π ) β 0 < π )) | ||
| Theorem | bln0 13921 | A ball is not empty. It is also inhabited, as seen at blcntr 13919. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ ((π· β (βMetβπ) β§ π β π β§ π β β+) β (π(ballβπ·)π ) β β ) | ||
| Theorem | blelrnps 13922 | 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 13923 | 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 13924 | 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 13925 | 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 13926 | 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 13927 | 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 13928 | 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 13929 | 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 13930* | 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 13931* | 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 13932* | 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 13933* | 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 13934* | 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 13935* | 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 13936 | 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 13937 | A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.) |
| β’ πΆ = (π· βΎ (π Γ π)) β β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π β β*) β (π(ballβπΆ)π ) = ((π(ballβπ·)π ) β© π)) | ||
| Theorem | xmeterval 13938 | Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| β’ βΌ = (β‘π· β β) β β’ (π· β (βMetβπ) β (π΄ βΌ π΅ β (π΄ β π β§ π΅ β π β§ (π΄π·π΅) β β))) | ||
| Theorem | xmeter 13939 | The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| β’ βΌ = (β‘π· β β) β β’ (π· β (βMetβπ) β βΌ Er π) | ||
| Theorem | xmetec 13940 | The equivalence classes under the finite separation equivalence relation are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| β’ βΌ = (β‘π· β β) β β’ ((π· β (βMetβπ) β§ π β π) β [π] βΌ = (π(ballβπ·)+β)) | ||
| Theorem | blssec 13941 | A ball centered at π is contained in the set of points finitely separated from π. This is just an application of ssbl 13929 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| β’ βΌ = (β‘π· β β) β β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π) β [π] βΌ ) | ||
| Theorem | blpnfctr 13942 | 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 13943 | An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec 13940, 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 13944 | The class of open sets of a metric space is a relation. (Contributed by Jim Kingdon, 5-May-2023.) |
| β’ Rel MetOpen | ||
| Theorem | mopnval 13945 | 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 13947, the open sets of a metric space form a topology π½, whose base set is βͺ π½ by mopnuni 13948. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ = (topGenβran (ballβπ·))) | ||
| Theorem | mopntopon 13946 | 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 13947 | 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 13948 | 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 13949* | 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 13950 | 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 13951 | 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 13952* | 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 13953 | An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.) |
| β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΄ β π½) β π΄ β π) | ||
| Theorem | isxms 13954 | 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 13955 | 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 13956 | 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 13957 | 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 13958 | 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 13959 | 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 13960 | An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| β’ (π β βMetSp β π β TopSp) | ||
| Theorem | msxms 13961 | A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| β’ (π β MetSp β π β βMetSp) | ||
| Theorem | mstps 13962 | A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| β’ (π β MetSp β π β TopSp) | ||
| Theorem | xmsxmet 13963 | The distance function, suitably truncated, is an extended metric on π. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β βMetSp β π· β (βMetβπ)) | ||
| Theorem | msmet 13964 | The distance function, suitably truncated, is a metric on π. (Contributed by Mario Carneiro, 12-Nov-2013.) |
| β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β MetSp β π· β (Metβπ)) | ||
| Theorem | msf 13965 | 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 13966 | The distance function, suitably truncated, is an extended metric on π. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ (π β βMetSp β (π· βΎ (π Γ π)) β (βMetβπ)) | ||
| Theorem | msmet2 13967 | The distance function, suitably truncated, is a metric on π. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ (π β MetSp β (π· βΎ (π Γ π)) β (Metβπ)) | ||
| Theorem | mscl 13968 | 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 13969 | Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β β*) | ||
| Theorem | xmsge0 13970 | The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β 0 β€ (π΄π·π΅)) | ||
| Theorem | xmseq0 13971 | 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 13972 | The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΅π·π΄)) | ||
| Theorem | xmstri2 13973 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅))) | ||
| Theorem | mstri2 13974 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β MetSp β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) + (πΆπ·π΅))) | ||
| Theorem | xmstri 13975 | 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 13976 | 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 13977 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β βMetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) +π (π΅π·πΆ))) | ||
| Theorem | mstri3 13978 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β MetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) + (π΅π·πΆ))) | ||
| Theorem | msrtri 13979 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| β’ π = (Baseβπ) & β’ π· = (distβπ) β β’ ((π β MetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (absβ((π΄π·πΆ) β (π΅π·πΆ))) β€ (π΄π·π΅)) | ||
| Theorem | xmspropd 13980 | Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β βMetSp β πΏ β βMetSp)) | ||
| Theorem | mspropd 13981 | Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β MetSp β πΏ β MetSp)) | ||
| Theorem | setsmsbasg 13982 | 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 13983 | 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 13984 | 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 13985* | 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 13986* | 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 13987* | 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 13988 | 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 13989 | 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 13990 | 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 13991 | 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 13992 | A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.) |
| β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΅ β ran (ballβπ·)) β π΅ β π½) | ||
| Theorem | blopn 13993 | 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 13994* | 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 13995 | 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 13996* | A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.) |
| β’ π½ = (MetOpenβπ·) & β’ π = {π§ β π β£ (ππ·π§) β€ π } β β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β* β§ π β β* β§ π < π)) β π β (π(ballβπ·)π)) | ||
| Theorem | metss 13997* | 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 13998* | 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 13999* | 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 14000* | Lemma for metss2 14001. (Contributed by Mario Carneiro, 14-Sep-2015.) |
| β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) β β’ ((π β§ (π₯ β π β§ π β β+)) β (π₯(ballβπ·)(π / π )) β (π₯(ballβπΆ)π)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |