P. 149 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14801-14900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xmetunirn 14801	Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )
Theorem	xmeteq0 14802	The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) )
Theorem	meteq0 14803	The value of a metric is zero iff its arguments are equal. Property M2 of [Kreyszig] p. 4. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) )
Theorem	xmettri2 14804	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )
Theorem	mettri2 14805	Triangle inequality for the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) )
Theorem	xmet0 14806	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )
Theorem	met0 14807	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )
Theorem	xmetge0 14808	The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
Theorem	metge0 14809	The distance function of a metric space is nonnegative. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
Theorem	xmetlecl 14810	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> ( A D B ) e. RR )
Theorem	xmetsym 14811	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
Theorem	xmetpsmet 14812	An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. ( *Met ` X ) -> D e. (PsMet ` X ) )
Theorem	xmettpos 14813	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( *Met ` X ) -> tpos D = D )
Theorem	metsym 14814	The distance function of a metric space is symmetric. Definition 14-1.1(c) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
Theorem	xmettri 14815	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( C D B ) ) )
Theorem	mettri 14816	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.)
|- ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( C D B ) ) )
Theorem	xmettri3 14817	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( B D C ) ) )
Theorem	mettri3 14818	Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007.)
|- ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( B D C ) ) )
Theorem	xmetrtri 14819	One half of the reverse triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D C ) +e -e ( B D C ) ) <_ ( A D B ) )
Theorem	metrtri 14820	Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 21-Apr-2023.)
|- ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( abs ` ( ( A D C ) - ( B D C ) ) ) <_ ( A D B ) )
Theorem	metn0 14821	A metric space is nonempty iff its base set is nonempty. (Contributed by NM, 4-Oct-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( D e. ( Met ` X ) -> ( D =/= (/) <-> X =/= (/) ) )
Theorem	xmetres2 14822	Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( *Met ` R ) )
Theorem	metreslem 14823	Lemma for metres 14826. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- ( dom D = ( X X. X ) -> ( D |` ( R X. R ) ) = ( D |` ( ( X i^i R ) X. ( X i^i R ) ) ) )
Theorem	metres2 14824	Lemma for metres 14826. (Contributed by FL, 12-Oct-2006.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
|- ( ( D e. ( Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( Met ` R ) )
Theorem	xmetres 14825	A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- ( D e. ( *Met ` X ) -> ( D |` ( R X. R ) ) e. ( *Met ` ( X i^i R ) ) )
Theorem	metres 14826	A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( D e. ( Met ` X ) -> ( D |` ( R X. R ) ) e. ( Met ` ( X i^i R ) ) )
Theorem	0met 14827	The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- (/) e. ( Met ` (/) )
9.2.3  Metric space balls
Theorem	blfvalps 14828*	The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( D e. (PsMet ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) )
Theorem	blfval 14829*	The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Proof shortened by Thierry Arnoux, 11-Feb-2018.)
|- ( D e. ( *Met ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) )
Theorem	blex 14830	A ball is a set. Also see blfn 14284 in case you just know D is a set, not D e. ( *Met ` X ). (Contributed by Jim Kingdon, 4-May-2023.)
|- ( D e. ( *Met ` X ) -> ( ball ` D ) e. _V )
Theorem	blvalps 14831*	The ball around a point P is the set of all points whose distance from P is less than the ball's radius R. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) = { x e. X | ( P D x ) < R } )
Theorem	blval 14832*	The ball around a point P is the set of all points whose distance from P is less than the ball's radius R. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) = { x e. X | ( P D x ) < R } )
Theorem	elblps 14833	Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )
Theorem	elbl 14834	Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )
Theorem	elbl2ps 14835	Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( ( D e. (PsMet ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> ( P D A ) < R ) )
Theorem	elbl2 14836	Membership in a ball. (Contributed by NM, 9-Mar-2007.)
|- ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> ( P D A ) < R ) )
Theorem	elbl3ps 14837	Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.)
|- ( ( ( D e. (PsMet ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A D P ) < R ) )
Theorem	elbl3 14838	Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.)
|- ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A D P ) < R ) )
Theorem	blcomps 14839	Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( ( D e. (PsMet ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> P e. ( A ( ball ` D ) R ) ) )
Theorem	blcom 14840	Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.)
|- ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( P e. X /\ A e. X ) ) -> ( A e. ( P ( ball ` D ) R ) <-> P e. ( A ( ball ` D ) R ) ) )
Theorem	xblpnfps 14841	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.)
|- ( ( D e. (PsMet ` X ) /\ P e. X ) -> ( A e. ( P ( ball ` D ) +oo ) <-> ( A e. X /\ ( P D A ) e. RR ) ) )
Theorem	xblpnf 14842	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.)
|- ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( A e. ( P ( ball ` D ) +oo ) <-> ( A e. X /\ ( P D A ) e. RR ) ) )
Theorem	blpnf 14843	The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( D e. ( Met ` X ) /\ P e. X ) -> ( P ( ball ` D ) +oo ) = X )
Theorem	bldisj 14844	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.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) = (/) )
Theorem	blgt0 14845	A nonempty ball implies that the radius is positive. (Contributed by NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> 0 < R )
Theorem	bl2in 14846	Two balls are disjoint if they don't overlap. (Contributed by NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) R ) ) = (/) )
Theorem	xblss2ps 14847	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 14850 for extended metrics, we have to assume the balls are a finite distance apart, or else P will not even be in the infinity ball around Q. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ph -> D e. (PsMet ` X ) )   &    |- ( ph -> P e. X )   &    |- ( ph -> Q e. X )   &    |- ( ph -> R e. RR* )   &    |- ( ph -> S e. RR* )   &    |- ( ph -> ( P D Q ) e. RR )   &    |- ( ph -> ( P D Q ) <_ ( S +e -e R ) )   =>    |- ( ph -> ( P ( ball ` D ) R ) C_ ( Q ( ball ` D ) S ) )
Theorem	xblss2 14848	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 14850 for extended metrics, we have to assume the balls are a finite distance apart, or else P will not even be in the infinity ball around Q. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> P e. X )   &    |- ( ph -> Q e. X )   &    |- ( ph -> R e. RR* )   &    |- ( ph -> S e. RR* )   &    |- ( ph -> ( P D Q ) e. RR )   &    |- ( ph -> ( P D Q ) <_ ( S +e -e R ) )   =>    |- ( ph -> ( P ( ball ` D ) R ) C_ ( Q ( ball ` D ) S ) )
Theorem	blss2ps 14849	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.)
|- ( ( ( D e. (PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P ( ball ` D ) R ) C_ ( Q ( ball ` D ) S ) )
Theorem	blss2 14850	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.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P ( ball ` D ) R ) C_ ( Q ( ball ` D ) S ) )
Theorem	blhalf 14851	A ball of radius R / 2 is contained in a ball of radius R centered at any point inside the smaller ball. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jan-2014.)
|- ( ( ( M e. ( *Met ` X ) /\ Y e. X ) /\ ( R e. RR /\ Z e. ( Y ( ball ` M ) ( R / 2 ) ) ) ) -> ( Y ( ball ` M ) ( R / 2 ) ) C_ ( Z ( ball ` M ) R ) )
Theorem	blfps 14852	Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( D e. (PsMet ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )
Theorem	blf 14853	Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|- ( D e. ( *Met ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )
Theorem	blrnps 14854*	Membership in the range of the ball function. Note that ran ( ball ` D ) is the collection of all balls for metric D. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( D e. (PsMet ` X ) -> ( A e. ran ( ball ` D ) <-> E. x e. X E. r e. RR* A = ( x ( ball ` D ) r ) ) )
Theorem	blrn 14855*	Membership in the range of the ball function. Note that ran ( ball ` D ) is the collection of all balls for metric D. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( D e. ( *Met ` X ) -> ( A e. ran ( ball ` D ) <-> E. x e. X E. r e. RR* A = ( x ( ball ` D ) r ) ) )
Theorem	xblcntrps 14856	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.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> P e. ( P ( ball ` D ) R ) )
Theorem	xblcntr 14857	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> P e. ( P ( ball ` D ) R ) )
Theorem	blcntrps 14858	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.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> P e. ( P ( ball ` D ) R ) )
Theorem	blcntr 14859	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> P e. ( P ( ball ` D ) R ) )
Theorem	xblm 14860*	A ball is inhabited iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( E. x x e. ( P ( ball ` D ) R ) <-> 0 < R ) )
Theorem	bln0 14861	A ball is not empty. It is also inhabited, as seen at blcntr 14859. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) =/= (/) )
Theorem	blelrnps 14862	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.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. ran ( ball ` D ) )
Theorem	blelrn 14863	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.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. ran ( ball ` D ) )
Theorem	blssm 14864	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.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ X )
Theorem	unirnblps 14865	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.)
|- ( D e. (PsMet ` X ) -> U. ran ( ball ` D ) = X )
Theorem	unirnbl 14866	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.)
|- ( D e. ( *Met ` X ) -> U. ran ( ball ` D ) = X )
Theorem	blininf 14867	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.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( ( P ( ball ` D ) R ) i^i ( P ( ball ` D ) S ) ) = ( P ( ball ` D )inf ( { R , S } , RR* , < ) ) )
Theorem	ssblps 14868	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.)
|- ( ( ( D e. (PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( P ( ball ` D ) R ) C_ ( P ( ball ` D ) S ) )
Theorem	ssbl 14869	The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( P ( ball ` D ) R ) C_ ( P ( ball ` D ) S ) )
Theorem	blssps 14870*	Any point P in a ball B can be centered in another ball that is a subset of B. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ B e. ran ( ball ` D ) /\ P e. B ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B )
Theorem	blss 14871*	Any point P in a ball B can be centered in another ball that is a subset of B. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ B e. ran ( ball ` D ) /\ P e. B ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B )
Theorem	blssexps 14872*	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.)
|- ( ( D e. (PsMet ` X ) /\ P e. X ) -> ( E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
Theorem	blssex 14873*	Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
Theorem	ssblex 14874*	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.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) S ) ) )
Theorem	blin2 14875*	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.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) )
Theorem	blbas 14876	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.)
|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) e. TopBases )
Theorem	blres 14877	A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.)
|- C = ( D |` ( Y X. Y ) )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( P ( ball ` C ) R ) = ( ( P ( ball ` D ) R ) i^i Y ) )
Theorem	xmeterval 14878	Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- .~ = ( `' D " RR )   =>    |- ( D e. ( *Met ` X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( A D B ) e. RR ) ) )
Theorem	xmeter 14879	The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- .~ = ( `' D " RR )   =>    |- ( D e. ( *Met ` X ) -> .~ Er X )
Theorem	xmetec 14880	The equivalence classes under the finite separation equivalence relation are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- .~ = ( `' D " RR )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X ) -> [ P ] .~ = ( P ( ball ` D ) +oo ) )
Theorem	blssec 14881	A ball centered at P is contained in the set of points finitely separated from P. This is just an application of ssbl 14869 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- .~ = ( `' D " RR )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) -> ( P ( ball ` D ) S ) C_ [ P ] .~ )
Theorem	blpnfctr 14882	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.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> ( P ( ball ` D ) +oo ) = ( A ( ball ` D ) +oo ) )
Theorem	xmetresbl 14883	An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec 14880, 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 +oo from each other. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- B = ( P ( ball ` D ) R )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( D |` ( B X. B ) ) e. ( Met ` B ) )
9.2.4  Open sets of a metric space
Theorem	mopnrel 14884	The class of open sets of a metric space is a relation. (Contributed by Jim Kingdon, 5-May-2023.)
|- Rel MetOpen
Theorem	mopnval 14885	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 ` D ) is the family of all open sets in the metric space determined by the metric D. By mopntop 14887, the open sets of a metric space form a topology J, whose base set is U. J by mopnuni 14888. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J = ( topGen ` ran ( ball ` D ) ) )
Theorem	mopntopon 14886	The set of open sets of a metric space X is a topology on X. 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.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J e. (TopOn ` X ) )
Theorem	mopntop 14887	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.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J e. Top )
Theorem	mopnuni 14888	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.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> X = U. J )
Theorem	elmopn 14889*	The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> ( A e. J <-> ( A C_ X /\ A. x e. A E. y e. ran ( ball ` D ) ( x e. y /\ y C_ A ) ) ) )
Theorem	mopnfss 14890	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.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J C_ ~P X )
Theorem	mopnm 14891	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.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> X e. J )
Theorem	elmopn2 14892*	A defining property of an open set of a metric space. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> ( A e. J <-> ( A C_ X /\ A. x e. A E. y e. RR+ ( x ( ball ` D ) y ) C_ A ) ) )
Theorem	mopnss 14893	An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. J ) -> A C_ X )
Theorem	isxms 14894	Express the predicate " <. X , D >. is an extended metric space" with underlying set X and distance function D. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. *MetSp <-> ( K e. TopSp /\ J = ( MetOpen ` D ) ) )
Theorem	isxms2 14895	Express the predicate " <. X , D >. is an extended metric space" with underlying set X and distance function D. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. *MetSp <-> ( D e. ( *Met ` X ) /\ J = ( MetOpen ` D ) ) )
Theorem	isms 14896	Express the predicate " <. X , D >. is a metric space" with underlying set X and distance function D. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. MetSp <-> ( K e. *MetSp /\ D e. ( Met ` X ) ) )
Theorem	isms2 14897	Express the predicate " <. X , D >. is a metric space" with underlying set X and distance function D. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. MetSp <-> ( D e. ( Met ` X ) /\ J = ( MetOpen ` D ) ) )
Theorem	xmstopn 14898	The topology component of an extended metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. *MetSp -> J = ( MetOpen ` D ) )
Theorem	mstopn 14899	The topology component of a metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. MetSp -> J = ( MetOpen ` D ) )
Theorem	xmstps 14900	An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( M e. *MetSp -> M e. TopSp )