P. 151 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isms2 15001	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 15002	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 15003	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 15004	An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( M e. *MetSp -> M e. TopSp )
Theorem	msxms 15005	A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( M e. MetSp -> M e. *MetSp )
Theorem	mstps 15006	A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( M e. MetSp -> M e. TopSp )
Theorem	xmsxmet 15007	The distance function, suitably truncated, is an extended metric on X. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- X = ( Base ` M )   &    |- D = ( ( dist ` M ) |` ( X X. X ) )   =>    |- ( M e. *MetSp -> D e. ( *Met ` X ) )
Theorem	msmet 15008	The distance function, suitably truncated, is a metric on X. (Contributed by Mario Carneiro, 12-Nov-2013.)
|- X = ( Base ` M )   &    |- D = ( ( dist ` M ) |` ( X X. X ) )   =>    |- ( M e. MetSp -> D e. ( Met ` X ) )
Theorem	msf 15009	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.)
|- X = ( Base ` M )   &    |- D = ( ( dist ` M ) |` ( X X. X ) )   =>    |- ( M e. MetSp -> D : ( X X. X ) --> RR )
Theorem	xmsxmet2 15010	The distance function, suitably truncated, is an extended metric on X. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( M e. *MetSp -> ( D |` ( X X. X ) ) e. ( *Met ` X ) )
Theorem	msmet2 15011	The distance function, suitably truncated, is a metric on X. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( Met ` X ) )
Theorem	mscl 15012	Closure of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ A e. X /\ B e. X ) -> ( A D B ) e. RR )
Theorem	xmscl 15013	Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
Theorem	xmsge0 15014	The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
Theorem	xmseq0 15015	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.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) )
Theorem	xmssym 15016	The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
Theorem	xmstri2 15017	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )
Theorem	mstri2 15018	Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) )
Theorem	xmstri 15019	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.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( C D B ) ) )
Theorem	mstri 15020	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.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( C D B ) ) )
Theorem	xmstri3 15021	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( B D C ) ) )
Theorem	mstri3 15022	Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( B D C ) ) )
Theorem	msrtri 15023	Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( abs ` ( ( A D C ) - ( B D C ) ) ) <_ ( A D B ) )
Theorem	xmspropd 15024	Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )   &    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )   =>    |- ( ph -> ( K e. *MetSp <-> L e. *MetSp ) )
Theorem	mspropd 15025	Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )   &    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )   =>    |- ( ph -> ( K e. MetSp <-> L e. MetSp ) )
Theorem	setsmsbasg 15026	The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( ph -> X = ( Base ` M ) )   &    |- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )   &    |- ( ph -> K = ( M sSet <. (TopSet ` ndx ) , ( MetOpen ` D ) >. ) )   &    |- ( ph -> M e. V )   &    |- ( ph -> ( MetOpen ` D ) e. W )   =>    |- ( ph -> X = ( Base ` K ) )
Theorem	setsmsdsg 15027	The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( ph -> X = ( Base ` M ) )   &    |- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )   &    |- ( ph -> K = ( M sSet <. (TopSet ` ndx ) , ( MetOpen ` D ) >. ) )   &    |- ( ph -> M e. V )   &    |- ( ph -> ( MetOpen ` D ) e. W )   =>    |- ( ph -> ( dist ` M ) = ( dist ` K ) )
Theorem	setsmstsetg 15028	The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.)
|- ( ph -> X = ( Base ` M ) )   &    |- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )   &    |- ( ph -> K = ( M sSet <. (TopSet ` ndx ) , ( MetOpen ` D ) >. ) )   &    |- ( ph -> M e. V )   &    |- ( ph -> ( MetOpen ` D ) e. W )   =>    |- ( ph -> ( MetOpen ` D ) = (TopSet ` K ) )
Theorem	mopni 15029*	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.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) )
Theorem	mopni2 15030*	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.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ A )
Theorem	mopni3 15031*	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.)
|- J = ( MetOpen ` D )   =>    |- ( ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) /\ R e. RR+ ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ A ) )
Theorem	blssopn 15032	The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> ran ( ball ` D ) C_ J )
Theorem	unimopn 15033	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.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A C_ J ) -> U. A e. J )
Theorem	mopnin 15034	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.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )
Theorem	mopn0 15035	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.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> (/) e. J )
Theorem	rnblopn 15036	A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ B e. ran ( ball ` D ) ) -> B e. J )
Theorem	blopn 15037	A ball of a metric space is an open set. (Contributed by NM, 9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. J )
Theorem	neibl 15038*	The neighborhoods around a point P of a metric space are those subsets containing a ball around P. Definition of neighborhood in [Kreyszig] p. 19. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) ) )
Theorem	blnei 15039	A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) e. ( ( nei ` J ) ` { P } ) )
Theorem	blsscls2 15040*	A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- S = { z e. X | ( P D z ) <_ R }   =>    |- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ T e. RR* /\ R < T ) ) -> S C_ ( P ( ball ` D ) T ) )
Theorem	metss 15041*	Two ways of saying that metric D generates a finer topology than metric C. (Contributed by Mario Carneiro, 12-Nov-2013.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( J C_ K <-> A. x e. X A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
Theorem	metequiv 15042*	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.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( J = K <-> A. x e. X ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ A. a e. RR+ E. b e. RR+ ( x ( ball ` C ) b ) C_ ( x ( ball ` D ) a ) ) ) )
Theorem	metequiv2 15043*	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.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( A. x e. X A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> J = K ) )
Theorem	metss2lem 15044*	Lemma for metss2 15045. (Contributed by Mario Carneiro, 14-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- ( ph -> C e. ( Met ` X ) )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )   =>    |- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( x ( ball ` D ) ( S / R ) ) C_ ( x ( ball ` C ) S ) )
Theorem	metss2 15045*	If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y )), then D generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- ( ph -> C e. ( Met ` X ) )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )   =>    |- ( ph -> J C_ K )
Theorem	comet 15046*	The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> F : ( 0 [,] +oo ) --> RR* )   &    |- ( ( ph /\ x e. ( 0 [,] +oo ) ) -> ( ( F ` x ) = 0 <-> x = 0 ) )   &    |- ( ( ph /\ ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) ) -> ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )   &    |- ( ( ph /\ ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) ) -> ( F ` ( x +e y ) ) <_ ( ( F ` x ) +e ( F ` y ) ) )   =>    |- ( ph -> ( F o. D ) e. ( *Met ` X ) )
Theorem	bdmetval 15047*	Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   =>    |- ( ( ( C : ( X X. X ) --> RR* /\ R e. RR* ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) = inf ( { ( A C B ) , R } , RR* , < ) )
Theorem	bdxmet 15048*	The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   =>    |- ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> D e. ( *Met ` X ) )
Theorem	bdmet 15049*	The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   =>    |- ( ( C e. ( *Met ` X ) /\ R e. RR+ ) -> D e. ( Met ` X ) )
Theorem	bdbl 15050*	The standard bounded metric corresponding to C generates the same balls as C for radii less than R. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   =>    |- ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> ( P ( ball ` D ) S ) = ( P ( ball ` C ) S ) )
Theorem	bdmopn 15051*	The standard bounded metric corresponding to C generates the same topology as C. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   &    |- J = ( MetOpen ` C )   =>    |- ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> J = ( MetOpen ` D ) )
Theorem	mopnex 15052*	The topology generated by an extended metric can also be generated by a true metric. Thus, "metrizable topologies" can equivalently be defined in terms of metrics or extended metrics. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> E. d e. ( Met ` X ) J = ( MetOpen ` d ) )
Theorem	metrest 15053	Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.)
|- D = ( C |` ( Y X. Y ) )   &    |- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( J ↾t Y ) = K )
Theorem	xmetxp 15054*	The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   =>    |- ( ph -> P e. ( *Met ` ( X X. Y ) ) )
Theorem	xmetxpbl 15055*	The maximum metric (Chebyshev distance) on the product of two sets, expressed in terms of balls centered on a point C with radius R. (Contributed by Jim Kingdon, 22-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- ( ph -> R e. RR* )   &    |- ( ph -> C e. ( X X. Y ) )   =>    |- ( ph -> ( C ( ball ` P ) R ) = ( ( ( 1st ` C ) ( ball ` M ) R ) X. ( ( 2nd ` C ) ( ball ` N ) R ) ) )
Theorem	xmettxlem 15056*	Lemma for xmettx 15057. (Contributed by Jim Kingdon, 15-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   &    |- L = ( MetOpen ` P )   =>    |- ( ph -> L C_ ( J tX K ) )
Theorem	xmettx 15057*	The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   &    |- L = ( MetOpen ` P )   =>    |- ( ph -> L = ( J tX K ) )
9.2.5  Continuity in metric spaces
Theorem	metcnp3 15058*	Two ways to express that F is continuous at P for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) )
Theorem	metcnp 15059*	Two ways to say a mapping from metric C to metric D is continuous at point P. (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) ) )
Theorem	metcnp2 15060*	Two ways to say a mapping from metric C to metric D is continuous at point P. The distance arguments are swapped compared to metcnp 15059 (and Munkres' metcn 15061) for compatibility with df-lm 14737. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) ) )
Theorem	metcn 15061*	Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" y there is a positive "delta" z such that a distance less than delta in C maps to a distance less than epsilon in D. (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) )
Theorem	metcnpi 15062*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 15059. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < A ) )
Theorem	metcnpi2 15063*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 15060. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) < x -> ( ( F ` y ) D ( F ` P ) ) < A ) )
Theorem	metcnpi3 15064*	Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 15063 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )
Theorem	txmetcnp 15065*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- L = ( MetOpen ` E )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) ) )
Theorem	txmetcn 15066*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- L = ( MetOpen ` E )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )
Theorem	metcnpd 15067*	Two ways to say a mapping from metric C to metric D is continuous at point P. (Contributed by Jim Kingdon, 14-Jun-2023.)
|- ( ph -> J = ( MetOpen ` C ) )   &    |- ( ph -> K = ( MetOpen ` D ) )   &    |- ( ph -> C e. ( *Met ` X ) )   &    |- ( ph -> D e. ( *Met ` Y ) )   &    |- ( ph -> P e. X )   =>    |- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) ) )
9.2.6  Topology on the reals
Theorem	qtopbasss 15068*	The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Jim Kingdon, 22-May-2023.)
|- S C_ RR*   &    |- ( ( x e. S /\ y e. S ) -> sup ( { x , y } , RR* , < ) e. S )   &    |- ( ( x e. S /\ y e. S ) -> inf ( { x , y } , RR* , < ) e. S )   =>    |- ( (,) " ( S X. S ) ) e. TopBases
Theorem	qtopbas 15069	The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.)
|- ( (,) " ( QQ X. QQ ) ) e. TopBases
Theorem	retopbas 15070	A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.)
|- ran (,) e. TopBases
Theorem	retop 15071	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|- ( topGen ` ran (,) ) e. Top
Theorem	uniretop 15072	The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)
|- RR = U. ( topGen ` ran (,) )
Theorem	retopon 15073	The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( topGen ` ran (,) ) e. (TopOn ` RR )
Theorem	retps 15074	The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.)
|- K = { <. ( Base ` ndx ) , RR >. , <. (TopSet ` ndx ) , ( topGen ` ran (,) ) >. }   =>    |- K e. TopSp
Theorem	iooretopg 15075	Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon, 23-May-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) e. ( topGen ` ran (,) ) )
Theorem	cnmetdval 15076	Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- D = ( abs o. - )   =>    |- ( ( A e. CC /\ B e. CC ) -> ( A D B ) = ( abs ` ( A - B ) ) )
Theorem	cnmet 15077	The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006.)
|- ( abs o. - ) e. ( Met ` CC )
Theorem	cnxmet 15078	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( abs o. - ) e. ( *Met ` CC )
Theorem	cntoptopon 15079	The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- J e. (TopOn ` CC )
Theorem	cntoptop 15080	The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- J e. Top
Theorem	cnbl0 15081	Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- D = ( abs o. - )   =>    |- ( R e. RR* -> ( `' abs " ( 0 [,) R ) ) = ( 0 ( ball ` D ) R ) )
Theorem	cnblcld 15082*	Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- D = ( abs o. - )   =>    |- ( R e. RR* -> ( `' abs " ( 0 [,] R ) ) = { x e. CC | ( 0 D x ) <_ R } )
Theorem	cnfldms 15083	The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. MetSp
Theorem	cnfldxms 15084	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. *MetSp
Theorem	cnfldtps 15085	The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ℂfld e. TopSp
Theorem	cnfldtopn 15086	The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J = ( MetOpen ` ( abs o. - ) )
Theorem	cnfldtopon 15087	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. (TopOn ` CC )
Theorem	cnfldtop 15088	The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. Top
Theorem	unicntopcntop 15089	The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
|- CC = U. ( MetOpen ` ( abs o. - ) )
Theorem	unicntop 15090	The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- CC = U. ( TopOpen ` ℂfld )
Theorem	cnopncntop 15091	The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
|- CC e. ( MetOpen ` ( abs o. - ) )
Theorem	cnopn 15092	The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- CC e. ( TopOpen ` ℂfld )
Theorem	reopnap 15093*	The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.)
|- ( A e. RR -> { w e. RR | w # A } e. ( topGen ` ran (,) ) )
Theorem	remetdval 15094	Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )
Theorem	remet 15095	The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- D e. ( Met ` RR )
Theorem	rexmet 15096	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- D e. ( *Met ` RR )
Theorem	bl2ioo 15097	A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A ( ball ` D ) B ) = ( ( A - B ) (,) ( A + B ) ) )
Theorem	ioo2bl 15098	An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) = ( ( ( A + B ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) )
Theorem	ioo2blex 15099	An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) e. ran ( ball ` D ) )
Theorem	blssioo 15100	The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ran ( ball ` D ) C_ ran (,)