P. 152 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15101-15200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hmeocnv 15101	The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( F e. ( J Homeo K ) -> `' F e. ( K Homeo J ) )
Theorem	hmeof1o2 15102	A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( J Homeo K ) ) -> F : X -1-1-onto-> Y )
Theorem	hmeof1o 15103	A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 30-May-2014.)
|- X = U. J   &    |- Y = U. K   =>    |- ( F e. ( J Homeo K ) -> F : X -1-1-onto-> Y )
Theorem	hmeoima 15104	The image of an open set by a homeomorphism is an open set. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ( F e. ( J Homeo K ) /\ A e. J ) -> ( F " A ) e. K )
Theorem	hmeoopn 15105	Homeomorphisms preserve openness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. J <-> ( F " A ) e. K ) )
Theorem	hmeocld 15106	Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( F " A ) e. ( Clsd ` K ) ) )
Theorem	hmeontr 15107	Homeomorphisms preserve interiors. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( int ` K ) ` ( F " A ) ) = ( F " ( ( int ` J ) ` A ) ) )
Theorem	hmeoimaf1o 15108*	The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- G = ( x e. J |-> ( F " x ) )   =>    |- ( F e. ( J Homeo K ) -> G : J -1-1-onto-> K )
Theorem	hmeores 15109	The restriction of a homeomorphism is a homeomorphism. (Contributed by Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( F |` Y ) e. ( ( J ↾t Y ) Homeo ( K ↾t ( F " Y ) ) ) )
Theorem	hmeoco 15110	The composite of two homeomorphisms is a homeomorphism. (Contributed by FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|- ( ( F e. ( J Homeo K ) /\ G e. ( K Homeo L ) ) -> ( G o. F ) e. ( J Homeo L ) )
Theorem	idhmeo 15111	The identity function is a homeomorphism. (Contributed by FL, 14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|- ( J e. (TopOn ` X ) -> ( _I |` X ) e. ( J Homeo J ) )
Theorem	hmeocnvb 15112	The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|- ( Rel F -> ( `' F e. ( J Homeo K ) <-> F e. ( K Homeo J ) ) )
Theorem	txhmeo 15113*	Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- X = U. J   &    |- Y = U. K   &    |- ( ph -> F e. ( J Homeo L ) )   &    |- ( ph -> G e. ( K Homeo M ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) )
Theorem	txswaphmeolem 15114*	Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( y e. Y , x e. X |-> <. x , y >. ) o. ( x e. X , y e. Y |-> <. y , x >. ) ) = ( _I |` ( X X. Y ) )
Theorem	txswaphmeo 15115*	There is a homeomorphism from X X. Y to Y X. X. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( x e. X , y e. Y |-> <. y , x >. ) e. ( ( J tX K ) Homeo ( K tX J ) ) )
9.2  Metric spaces
9.2.1  Pseudometric spaces
Theorem	psmetrel 15116	The class of pseudometrics is a relation. (Contributed by Jim Kingdon, 24-Apr-2023.)
|- Rel PsMet
Theorem	ispsmet 15117*	Express the predicate " D is a pseudometric". (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( X e. V -> ( D e. (PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
Theorem	psmetdmdm 15118	Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. (PsMet ` X ) -> X = dom dom D )
Theorem	psmetf 15119	The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> RR* )
Theorem	psmetcl 15120	Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
Theorem	psmet0 15121	The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X ) -> ( A D A ) = 0 )
Theorem	psmettri2 15122	Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )
Theorem	psmetsym 15123	The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
Theorem	psmettri 15124	Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( C D B ) ) )
Theorem	psmetge0 15125	The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon, 19-Apr-2023.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
Theorem	psmetxrge0 15126	The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
|- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> ( 0 [,] +oo ) )
Theorem	psmetres2 15127	Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. (PsMet ` R ) )
Theorem	psmetlecl 15128	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> ( A D B ) e. RR )
Theorem	distspace 15129	A set X together with a (distance) function D which is a pseudometric is a distance space (according to E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006), i.e. a (base) set X equipped with a distance D, which is a mapping of two elements of the base set to the (extended) reals and which is nonnegative, symmetric and equal to 0 if the two elements are equal. (Contributed by AV, 15-Oct-2021.) (Revised by AV, 5-Jul-2022.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> ( ( D : ( X X. X ) --> RR* /\ ( A D A ) = 0 ) /\ ( 0 <_ ( A D B ) /\ ( A D B ) = ( B D A ) ) ) )
9.2.2  Basic metric space properties
Syntax	cxms 15130	Extend class notation with the class of extended metric spaces.
class *MetSp
Syntax	cms 15131	Extend class notation with the class of metric spaces.
class MetSp
Syntax	ctms 15132	Extend class notation with the function mapping a metric to the metric space it defines.
class toMetSp
Definition	df-xms 15133	Define the (proper) class of extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
Definition	df-ms 15134	Define the (proper) class of metric spaces. (Contributed by NM, 27-Aug-2006.)
|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
Definition	df-tms 15135	Define the function mapping a metric to the metric space which it defines. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
Theorem	metrel 15136	The class of metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.)
|- Rel Met
Theorem	xmetrel 15137	The class of extended metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.)
|- Rel *Met
Theorem	ismet 15138*	Express the predicate " D is a metric". (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( X e. A -> ( D e. ( Met ` X ) <-> ( D : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) ) ) )
Theorem	isxmet 15139*	Express the predicate " D is an extended metric". (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( X e. A -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
Theorem	ismeti 15140*	Properties that determine a metric. (Contributed by NM, 17-Nov-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- X e. _V   &    |- D : ( X X. X ) --> RR   &    |- ( ( x e. X /\ y e. X ) -> ( ( x D y ) = 0 <-> x = y ) )   &    |- ( ( x e. X /\ y e. X /\ z e. X ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )   =>    |- D e. ( Met ` X )
Theorem	isxmetd 15141*	Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ph -> X e. _V )   &    |- ( ph -> D : ( X X. X ) --> RR* )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> x = y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )   =>    |- ( ph -> D e. ( *Met ` X ) )
Theorem	isxmet2d 15142*	It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: D ( x , y ) = if ( x = y , 0 , -oo ) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ph -> X e. _V )   &    |- ( ph -> D : ( X X. X ) --> RR* )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> 0 <_ ( x D y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) <_ 0 <-> x = y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) /\ ( ( z D x ) e. RR /\ ( z D y ) e. RR ) ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )   =>    |- ( ph -> D e. ( *Met ` X ) )
Theorem	metflem 15143*	Lemma for metf 15145 and others. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( D e. ( Met ` X ) -> ( D : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) ) )
Theorem	xmetf 15144	Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
Theorem	metf 15145	Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.)
|- ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR )
Theorem	xmetcl 15146	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
Theorem	metcl 15147	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR )
Theorem	ismet2 15148	An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( Met ` X ) <-> ( D e. ( *Met ` X ) /\ D : ( X X. X ) --> RR ) )
Theorem	metxmet 15149	A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
Theorem	xmetdmdm 15150	Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( D e. ( *Met ` X ) -> X = dom dom D )
Theorem	metdmdm 15151	Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( D e. ( Met ` X ) -> X = dom dom D )
Theorem	xmetunirn 15152	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 15153	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 15154	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 15155	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 15156	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 15157	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 15158	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 15159	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 15160	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 15161	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 15162	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 15163	An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. ( *Met ` X ) -> D e. (PsMet ` X ) )
Theorem	xmettpos 15164	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 15165	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 15166	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 15167	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 15168	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 15169	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 15170	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 15171	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 15172	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 15173	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 15174	Lemma for metres 15177. (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 15175	Lemma for metres 15177. (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 15176	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 15177	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 15178	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 15179*	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 15180*	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 15181	A ball is a set. Also see blfn 14630 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 15182*	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 15183*	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 15184	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 15185	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 15186	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 15187	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 15188	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 15189	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 15190	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 15191	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 15192	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 15193	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 15194	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 15195	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 15196	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 15197	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 15198	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 15201 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 15199	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 15201 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 15200	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 ) )