P. 125 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12401-12500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mstri 12401	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 12402	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 12403	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 12404	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 12405	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 12406	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 12407	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 12408	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 12409	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 12410*	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 12411*	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 12412*	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 12413	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 12414	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 12415	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 12416	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 12417	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 12418	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 12419*	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 12420	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 12421*	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 12422*	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 12423*	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 12424*	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 12425*	Lemma for metss2 12426. (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 12426*	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 12427*	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 12428*	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 12429*	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 12430*	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 12431*	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 12432*	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 12433*	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 12434	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 )
6.2.5  Continuity in metric spaces
Theorem	metcnp3 12435*	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 12436*	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 12437*	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 12436 (and Munkres' metcn 12438) for compatibility with df-lm 12141. 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 12438*	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 12439*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 12436. (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 12440*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 12437. (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 12441*	Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 12440 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	metcnpd 12442*	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 ) ) ) )
6.2.6  Topology on the reals
Theorem	qtopbasss 12443*	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 12444	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 12445	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 12446	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|- ( topGen ` ran (,) ) e. Top
Theorem	uniretop 12447	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 12448	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 12449	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 12450	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 12451	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 12452	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 12453	The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( abs o. - ) e. ( *Met ` CC )
Theorem	cntoptopon 12454	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 12455	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 12456	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 12457*	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	remetdval 12458	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 12459	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 12460	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 12461	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 12462	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 12463	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 12464	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 12465	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 12466	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 12467	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 12468	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 12469	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 ) )
6.2.7  Topological definitions using the reals
Syntax	ccncf 12470	Extend class notation to include the operation which returns a class of continuous complex functions.
class -cn->
Definition	df-cncf 12471*	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 12472*	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 12473*	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 ) ) ) )
Theorem	elcncf2 12474*	Version of elcncf 12473 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.)
|- ( ( 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 ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) )
Theorem	cncfrss 12475	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> A C_ CC )
Theorem	cncfrss2 12476	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> B C_ CC )
Theorem	cncff 12477	A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- ( F e. ( A -cn-> B ) -> F : A --> B )
Theorem	cncfi 12478*	Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- ( ( F e. ( A -cn-> B ) /\ C e. A /\ R e. RR+ ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < R ) )
Theorem	elcncf1di 12479*	Membership in the set of continuous complex functions from A to B. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ( ph -> F : A --> B )   &    |- ( ph -> ( ( x e. A /\ y e. RR+ ) -> Z e. RR+ ) )   &    |- ( ph -> ( ( ( x e. A /\ w e. A ) /\ y e. RR+ ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) )   =>    |- ( ph -> ( ( A C_ CC /\ B C_ CC ) -> F e. ( A -cn-> B ) ) )
Theorem	elcncf1ii 12480*	Membership in the set of continuous complex functions from A to B. (Contributed by Paul Chapman, 26-Nov-2007.)
|- F : A --> B   &    |- ( ( x e. A /\ y e. RR+ ) -> Z e. RR+ )   &    |- ( ( ( x e. A /\ w e. A ) /\ y e. RR+ ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )   =>    |- ( ( A C_ CC /\ B C_ CC ) -> F e. ( A -cn-> B ) )
Theorem	rescncf 12481	A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- ( C C_ A -> ( F e. ( A -cn-> B ) -> ( F |` C ) e. ( C -cn-> B ) ) )
Theorem	cncffvrn 12482	Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( C C_ CC /\ F e. ( A -cn-> B ) ) -> ( F e. ( A -cn-> C ) <-> F : A --> C ) )
Theorem	cncfss 12483	The set of continuous functions is expanded when the range is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.)
|- ( ( B C_ C /\ C C_ CC ) -> ( A -cn-> B ) C_ ( A -cn-> C ) )
Theorem	climcncf 12484	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. ( A -cn-> B ) )   &    |- ( ph -> G : Z --> A )   &    |- ( ph -> G ~~> D )   &    |- ( ph -> D e. A )   =>    |- ( ph -> ( F o. G ) ~~> ( F ` D ) )
Theorem	abscncf 12485	Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- abs e. ( CC -cn-> RR )
Theorem	recncf 12486	Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- Re e. ( CC -cn-> RR )
Theorem	imcncf 12487	Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- Im e. ( CC -cn-> RR )
Theorem	cjcncf 12488	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- * e. ( CC -cn-> CC )
Theorem	mulc1cncf 12489*	Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- F = ( x e. CC |-> ( A x. x ) )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	divccncfap 12490*	Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.)
|- F = ( x e. CC |-> ( x / A ) )   =>    |- ( ( A e. CC /\ A # 0 ) -> F e. ( CC -cn-> CC ) )
Theorem	cncfco 12491	The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- ( ph -> F e. ( A -cn-> B ) )   &    |- ( ph -> G e. ( B -cn-> C ) )   =>    |- ( ph -> ( G o. F ) e. ( A -cn-> C ) )
Theorem	cncfmet 12492	Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.)
|- C = ( ( abs o. - ) |` ( A X. A ) )   &    |- D = ( ( abs o. - ) |` ( B X. B ) )   &    |- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( J Cn K ) )
Theorem	cncfcncntop 12493	Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- J = ( MetOpen ` ( abs o. - ) )   &    |- K = ( J ↾t A )   &    |- L = ( J ↾t B )   =>    |- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( K Cn L ) )
Theorem	cncfcn1cntop 12494	Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.)
|- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( CC -cn-> CC ) = ( J Cn J )
Theorem	cncfmptc 12495*	A constant function is a continuous function on CC. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Sep-2015.)
|- ( ( A e. T /\ S C_ CC /\ T C_ CC ) -> ( x e. S |-> A ) e. ( S -cn-> T ) )
Theorem	cncfmptid 12496*	The identity function is a continuous function on CC. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 17-May-2016.)
|- ( ( S C_ T /\ T C_ CC ) -> ( x e. S |-> x ) e. ( S -cn-> T ) )
Theorem	cncfmpt1f 12497*	Composition of continuous functions. -cn-> analogue of cnmpt11f 12234. (Contributed by Mario Carneiro, 3-Sep-2014.)
|- ( ph -> F e. ( CC -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> ( F ` A ) ) e. ( X -cn-> CC ) )
Theorem	addccncf 12498*	Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- F = ( x e. CC |-> ( x + A ) )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	cdivcncfap 12499*	Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.)
|- F = ( x e. { y e. CC | y # 0 } |-> ( A / x ) )   =>    |- ( A e. CC -> F e. ( { y e. CC | y # 0 } -cn-> CC ) )
Theorem	negcncf 12500*	The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- F = ( x e. A |-> -u x )   =>    |- ( A C_ CC -> F e. ( A -cn-> CC ) )