P. 132 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13101-13200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	msmet 13101	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 13102	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 13103	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 13104	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 13105	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 13106	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 13107	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 13108	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 13109	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 13110	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 13111	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 13112	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 13113	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 13114	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 13115	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 13116	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 13117	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 13118	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 13119	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 13120	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 13121	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 13122*	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 13123*	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 13124*	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 13125	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 13126	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 13127	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 13128	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 13129	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 13130	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 13131*	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 13132	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 13133*	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 13134*	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 13135*	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 13136*	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 13137*	Lemma for metss2 13138. (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 13138*	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 13139*	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 13140*	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 13141*	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 13142*	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 13143*	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 13144*	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 13145*	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 13146	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 13147*	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 13148*	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 13149*	Lemma for xmettx 13150. (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 13150*	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 ) )
8.2.5  Continuity in metric spaces
Theorem	metcnp3 13151*	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 13152*	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 13153*	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 13152 (and Munkres' metcn 13154) for compatibility with df-lm 12830. 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 13154*	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 13155*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 13152. (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 13156*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 13153. (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 13157*	Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 13156 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 13158*	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 13159*	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 13160*	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 ) ) ) )
8.2.6  Topology on the reals
Theorem	qtopbasss 13161*	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 13162	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 13163	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 13164	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|- ( topGen ` ran (,) ) e. Top
Theorem	uniretop 13165	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 13166	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 13167	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 13168	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 13169	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 13170	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 13171	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( abs o. - ) e. ( *Met ` CC )
Theorem	cntoptopon 13172	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 13173	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 13174	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 13175*	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	unicntopcntop 13176	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	cnopncntop 13177	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	reopnap 13178*	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 13179	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 13180	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 13181	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 13182	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 13183	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 13184	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 13185	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 (,)
Theorem	tgioo 13186	The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- D = ( ( abs o. - ) |` ( RR X. RR ) )   &    |- J = ( MetOpen ` D )   =>    |- ( topGen ` ran (,) ) = J
Theorem	tgqioo 13187	The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014.)
|- Q = ( topGen ` ( (,) " ( QQ X. QQ ) ) )   =>    |- ( topGen ` ran (,) ) = Q
Theorem	resubmet 13188	The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.)
|- R = ( topGen ` ran (,) )   &    |- J = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) )   =>    |- ( A C_ RR -> J = ( R ↾t A ) )
Theorem	tgioo2cntop 13189	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( topGen ` ran (,) ) = ( J ↾t RR )
Theorem	rerestcntop 13190	The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   &    |- R = ( topGen ` ran (,) )   =>    |- ( A C_ RR -> ( J ↾t A ) = ( R ↾t A ) )
Theorem	addcncntoplem 13191*	Lemma for addcncntop 13192, subcncntop 13193, and mulcncntop 13194. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   &    |- .+ : ( CC X. CC ) --> CC   &    |- ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - b ) ) < y /\ ( abs ` ( v - c ) ) < z ) -> ( abs ` ( ( u .+ v ) - ( b .+ c ) ) ) < a ) )   =>    |- .+ e. ( ( J tX J ) Cn J )
Theorem	addcncntop 13192	Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- + e. ( ( J tX J ) Cn J )
Theorem	subcncntop 13193	Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- - e. ( ( J tX J ) Cn J )
Theorem	mulcncntop 13194	Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- x. e. ( ( J tX J ) Cn J )
Theorem	divcnap 13195*	Complex number division is a continuous function, when the second argument is apart from zero. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Jim Kingdon, 25-Oct-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   &    |- K = ( J ↾t { x e. CC | x # 0 } )   =>    |- ( y e. CC , z e. { x e. CC | x # 0 } |-> ( y / z ) ) e. ( ( J tX K ) Cn J )
Theorem	fsumcncntop 13196*	A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for B normally contains free variables k and x to index it. (Contributed by NM, 8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )   =>    |- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( J Cn K ) )
8.2.7  Topological definitions using the reals
Syntax	ccncf 13197	Extend class notation to include the operation which returns a class of continuous complex functions.
class -cn->
Definition	df-cncf 13198*	Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.)
|- -cn-> = ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } )
Theorem	cncfval 13199*	The value of the continuous complex function operation is the set of continuous functions from A to B. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
|- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = { f e. ( B ^m A ) | A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) } )
Theorem	elcncf 13200*	Membership in the set of continuous complex functions from A to B. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
|- ( ( A C_ CC /\ B C_ CC ) -> ( F e. ( A -cn-> B ) <-> ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) ) )