P. 228 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22701-22800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cncffvrn 22701	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 22702	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 22703	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 22704	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 22705	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 22706	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 22707	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|- * e. ( CC -cn-> CC )
Theorem	mulc1cncf 22708*	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	divccncf 22709*	Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
|- F = ( x e. CC |-> ( x / A ) )   =>    |- ( ( A e. CC /\ A =/= 0 ) -> F e. ( CC -cn-> CC ) )
Theorem	cncfco 22710	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 22711	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	cncfcn 22712	Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.)
|- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t A )   &    |- L = ( J ↾t B )   =>    |- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( K Cn L ) )
Theorem	cncfcn1 22713	Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( CC -cn-> CC ) = ( J Cn J )
Theorem	cncfmptc 22714*	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 22715*	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 22716*	Composition of continuous functions. -cn-> analogue of cnmpt11f 21467. (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	cncfmpt2f 22717*	Composition of continuous functions. -cn-> analogue of cnmpt12f 21469. (Contributed by Mario Carneiro, 3-Sep-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- ( ph -> F e. ( ( J tX J ) Cn J ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) )
Theorem	cncfmpt2ss 22718*	Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.)
|- J = ( TopOpen ` ℂfld )   &    |- F e. ( ( J tX J ) Cn J )   &    |- ( ph -> ( x e. X |-> A ) e. ( X -cn-> S ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> S ) )   &    |- S C_ CC   &    |- ( ( A e. S /\ B e. S ) -> ( A F B ) e. S )   =>    |- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> S ) )
Theorem	addccncf 22719*	Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- F = ( x e. CC |-> ( x + A ) )   =>    |- ( A e. CC -> F e. ( CC -cn-> CC ) )
Theorem	cdivcncf 22720*	Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- F = ( x e. ( CC \ { 0 } ) |-> ( A / x ) )   =>    |- ( A e. CC -> F e. ( ( CC \ { 0 } ) -cn-> CC ) )
Theorem	negcncf 22721*	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 ) )
Theorem	negfcncf 22722*	The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
|- G = ( x e. A |-> -u ( F ` x ) )   =>    |- ( F e. ( A -cn-> CC ) -> G e. ( A -cn-> CC ) )
Theorem	abscncfALT 22723	Absolute value is continuous. Alternate proof of abscncf 22704. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
|- abs e. ( CC -cn-> RR )
Theorem	cncfcnvcn 22724	Rewrite cmphaushmeo 21603 for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015.)
|- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t X )   =>    |- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( Y -cn-> X ) ) )
Theorem	expcncf 22725*	The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 22675. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )
Theorem	cnmptre 22726*	Lemma for iirevcn 22729 and related functions. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- R = ( TopOpen ` ℂfld )   &    |- J = ( ( topGen ` ran (,) ) ↾t A )   &    |- K = ( ( topGen ` ran (,) ) ↾t B )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B C_ RR )   &    |- ( ( ph /\ x e. A ) -> F e. B )   &    |- ( ph -> ( x e. CC |-> F ) e. ( R Cn R ) )   =>    |- ( ph -> ( x e. A |-> F ) e. ( J Cn K ) )
Theorem	cnmpt2pc 22727*	Piecewise definition of a continuous function on a real interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- R = ( topGen ` ran (,) )   &    |- M = ( R ↾t ( A [,] B ) )   &    |- N = ( R ↾t ( B [,] C ) )   &    |- O = ( R ↾t ( A [,] C ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B e. ( A [,] C ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ( ph /\ ( x = B /\ y e. X ) ) -> D = E )   &    |- ( ph -> ( x e. ( A [,] B ) , y e. X |-> D ) e. ( ( M tX J ) Cn K ) )   &    |- ( ph -> ( x e. ( B [,] C ) , y e. X |-> E ) e. ( ( N tX J ) Cn K ) )   =>    |- ( ph -> ( x e. ( A [,] C ) , y e. X |-> if ( x <_ B , D , E ) ) e. ( ( O tX J ) Cn K ) )
Theorem	iirev 22728	Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( X e. ( 0 [,] 1 ) -> ( 1 - X ) e. ( 0 [,] 1 ) )
Theorem	iirevcn 22729	The reversion function is a continuous map of the unit interval. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- ( x e. ( 0 [,] 1 ) |-> ( 1 - x ) ) e. ( II Cn II )
Theorem	iihalf1 22730	Map the first half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( X e. ( 0 [,] ( 1 / 2 ) ) -> ( 2 x. X ) e. ( 0 [,] 1 ) )
Theorem	iihalf1cn 22731	The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- J = ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )   =>    |- ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( J Cn II )
Theorem	iihalf2 22732	Map the second half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( X e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. X ) - 1 ) e. ( 0 [,] 1 ) )
Theorem	iihalf2cn 22733	The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- J = ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) )   =>    |- ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. x ) - 1 ) ) e. ( J Cn II )
Theorem	elii1 22734	Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.)
|- ( X e. ( 0 [,] ( 1 / 2 ) ) <-> ( X e. ( 0 [,] 1 ) /\ X <_ ( 1 / 2 ) ) )
Theorem	elii2 22735	Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.)
|- ( ( X e. ( 0 [,] 1 ) /\ -. X <_ ( 1 / 2 ) ) -> X e. ( ( 1 / 2 ) [,] 1 ) )
Theorem	iimulcl 22736	The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) ) -> ( A x. B ) e. ( 0 [,] 1 ) )
Theorem	iimulcn 22737*	Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014.)
|- ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn II )
Theorem	icoopnst 22738	A half-open interval starting at A is open in the closed interval from A to B. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- J = ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A (,] B ) -> ( A [,) C ) e. J ) )
Theorem	iocopnst 22739	A half-open interval ending at B is open in the closed interval from A to B. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- J = ( MetOpen ` ( ( abs o. - ) |` ( ( A [,] B ) X. ( A [,] B ) ) ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,) B ) -> ( C (,] B ) e. J ) )
Theorem	icchmeo 22740*	The natural bijection from [ 0 , 1 ] to an arbitrary nontrivial closed interval [ A , B ] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- J = ( TopOpen ` ℂfld )   &    |- F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )   =>    |- ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Homeo ( J ↾t ( A [,] B ) ) ) )
Theorem	icopnfcnv 22741*	Define a bijection from [ 0 , 1 ) to [ 0 , +oo ). (Contributed by Mario Carneiro, 9-Sep-2015.)
|- F = ( x e. ( 0 [,) 1 ) |-> ( x / ( 1 - x ) ) )   =>    |- ( F : ( 0 [,) 1 ) -1-1-onto-> ( 0 [,) +oo ) /\ `' F = ( y e. ( 0 [,) +oo ) |-> ( y / ( 1 + y ) ) ) )
Theorem	icopnfhmeo 22742*	The defined bijection from [ 0 , 1 ) to [ 0 , +oo ) is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- F = ( x e. ( 0 [,) 1 ) |-> ( x / ( 1 - x ) ) )   &    |- J = ( TopOpen ` ℂfld )   =>    |- ( F Isom < , < ( ( 0 [,) 1 ) , ( 0 [,) +oo ) ) /\ F e. ( ( J ↾t ( 0 [,) 1 ) ) Homeo ( J ↾t ( 0 [,) +oo ) ) ) )
Theorem	iccpnfcnv 22743*	Define a bijection from [ 0 , 1 ] to [ 0 , +oo ]. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )   =>    |- ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ `' F = ( y e. ( 0 [,] +oo ) |-> if ( y = +oo , 1 , ( y / ( 1 + y ) ) ) ) )
Theorem	iccpnfhmeo 22744	The defined bijection from [ 0 , 1 ] to [ 0 , +oo ] is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )   &    |- K = ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) )   =>    |- ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ F e. ( II Homeo K ) )
Theorem	xrhmeo 22745*	The bijection from [ -u 1 , 1 ] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )   &    |- G = ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = (ordTop ` <_ )   =>    |- ( G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) /\ G e. ( ( J ↾t ( -u 1 [,] 1 ) ) Homeo (ordTop ` <_ ) ) )
Theorem	xrhmph 22746	The extended reals are homeomorphic to the interval [ 0 , 1 ]. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- II ~= (ordTop ` <_ )
Theorem	xrcmp 22747	The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo 22609), this means that RR* is a compactification of RR. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- (ordTop ` <_ ) e. Comp
Theorem	xrconn 22748	The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- (ordTop ` <_ ) e. Conn
Theorem	icccvx 22749	A linear combination of two reals lies in the interval between them. Equivalently, a closed interval is a convex set. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. C ) + ( T x. D ) ) e. ( A [,] B ) ) )
Theorem	oprpiece1res1 22750*	Restriction to the first part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.)
|- A e. RR   &    |- B e. RR   &    |- A <_ B   &    |- R e. _V   &    |- S e. _V   &    |- K e. ( A [,] B )   &    |- F = ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) )   &    |- G = ( x e. ( A [,] K ) , y e. C |-> R )   =>    |- ( F |` ( ( A [,] K ) X. C ) ) = G
Theorem	oprpiece1res2 22751*	Restriction to the second part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.)
|- A e. RR   &    |- B e. RR   &    |- A <_ B   &    |- R e. _V   &    |- S e. _V   &    |- K e. ( A [,] B )   &    |- F = ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) )   &    |- ( x = K -> R = P )   &    |- ( x = K -> S = Q )   &    |- ( y e. C -> P = Q )   &    |- G = ( x e. ( K [,] B ) , y e. C |-> S )   =>    |- ( F |` ( ( K [,] B ) X. C ) ) = G
Theorem	cnrehmeo 22752*	The canonical bijection from ( RR X. RR ) to CC described in cnref1o 11827 is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if ( RR X. RR ) is metrized with the l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro, 25-Aug-2014.)
|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )   &    |- J = ( topGen ` ran (,) )   &    |- K = ( TopOpen ` ℂfld )   =>    |- F e. ( ( J tX J ) Homeo K )
Theorem	cnheiborlem 22753*	Lemma for cnheibor 22754. (Contributed by Mario Carneiro, 14-Sep-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- T = ( J ↾t X )   &    |- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )   &    |- Y = ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) )   =>    |- ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> T e. Comp )
Theorem	cnheibor 22754*	Heine-Borel theorem for complex numbers. A subset of CC is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- T = ( J ↾t X )   =>    |- ( X C_ CC -> ( T e. Comp <-> ( X e. ( Clsd ` J ) /\ E. r e. RR A. x e. X ( abs ` x ) <_ r ) ) )
Theorem	cnllycmp 22755	The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- J e. 𝑛Locally Comp
Theorem	rellycmp 22756	The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
|- ( topGen ` ran (,) ) e. 𝑛Locally Comp
Theorem	bndth 22757*	The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -u F.) (Contributed by Mario Carneiro, 12-Aug-2014.)
|- X = U. J   &    |- K = ( topGen ` ran (,) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> F e. ( J Cn K ) )   =>    |- ( ph -> E. x e. RR A. y e. X ( F ` y ) <_ x )
Theorem	evth 22758*	The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- X = U. J   &    |- K = ( topGen ` ran (,) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> X =/= (/) )   =>    |- ( ph -> E. x e. X A. y e. X ( F ` y ) <_ ( F ` x ) )
Theorem	evth2 22759*	The Extreme Value Theorem, minimum version. A continuous function from a nonempty compact topological space to the reals attains its minimum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- X = U. J   &    |- K = ( topGen ` ran (,) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> X =/= (/) )   =>    |- ( ph -> E. x e. X A. y e. X ( F ` x ) <_ ( F ` y ) )
Theorem	lebnumlem1 22760*	Lemma for lebnum 22763. The function F measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> U C_ J )   &    |- ( ph -> X = U. U )   &    |- ( ph -> U e. Fin )   &    |- ( ph -> -. X e. U )   &    |- F = ( y e. X |-> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )   =>    |- ( ph -> F : X --> RR+ )
Theorem	lebnumlem2 22761*	Lemma for lebnum 22763. As a finite sum of point-to-set distance functions, which are continuous by metdscn 22659, the function F is also continuous. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> U C_ J )   &    |- ( ph -> X = U. U )   &    |- ( ph -> U e. Fin )   &    |- ( ph -> -. X e. U )   &    |- F = ( y e. X |-> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )   &    |- K = ( topGen ` ran (,) )   =>    |- ( ph -> F e. ( J Cn K ) )
Theorem	lebnumlem3 22762*	Lemma for lebnum 22763. By the previous lemmas, F is continuous and positive on a compact set, so it has a positive minimum r. Then setting d = r / # ( U ), since for each u e. U we have ball ( x , d ) C_ u iff d <_ d ( x , X \ u ), if -. ball ( x , d ) C_ u for all u then summing over u yields sum_ u e. U d ( x , X \ u ) = F ( x ) < sum_ u e. U d = r, in contradiction to the assumption that r is the minimum of F. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) (Revised by AV, 30-Sep-2020.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> U C_ J )   &    |- ( ph -> X = U. U )   &    |- ( ph -> U e. Fin )   &    |- ( ph -> -. X e. U )   &    |- F = ( y e. X |-> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )   &    |- K = ( topGen ` ran (,) )   =>    |- ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
Theorem	lebnum 22763*	The Lebesgue number lemma, or Lebesgue covering lemma. If X is a compact metric space and U is an open cover of X, then there exists a positive real number d such that every ball of size d (and every subset of a ball of size d, including every subset of diameter less than d) is a subset of some member of the cover. (Contributed by Mario Carneiro, 14-Feb-2015.) (Proof shortened by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> U C_ J )   &    |- ( ph -> X = U. U )   =>    |- ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
Theorem	xlebnum 22764*	Generalize lebnum 22763 to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> U C_ J )   &    |- ( ph -> X = U. U )   =>    |- ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
Theorem	lebnumii 22765*	Specialize the Lebesgue number lemma lebnum 22763 to the unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.)
|- ( ( U C_ II /\ ( 0 [,] 1 ) = U. U ) -> E. n e. NN A. k e. ( 1 ... n ) E. u e. U ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ u )
12.4.12  Path homotopy
Syntax	chtpy 22766	Extend class notation with the class of homotopies between two continuous functions.
class Htpy
Syntax	cphtpy 22767	Extend class notation with the class of path homotopies between two continuous functions.
class PHtpy
Syntax	cphtpc 22768	Extend class notation with the path homotopy relation.
class ~=ph
Definition	df-htpy 22769*	Define the function which takes topological spaces X , Y and two continuous functions F , G : X --> Y and returns the class of homotopies from F to G. (Contributed by Mario Carneiro, 22-Feb-2015.)
|- Htpy = ( x e. Top , y e. Top |-> ( f e. ( x Cn y ) , g e. ( x Cn y ) |-> { h e. ( ( x tX II ) Cn y ) | A. s e. U. x ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) )
Definition	df-phtpy 22770*	Define the class of path homotopies between two paths F , G : II --> X; these are homotopies (in the sense of df-htpy 22769) which also preserve both endpoints of the paths throughout the homotopy. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- PHtpy = ( x e. Top |-> ( f e. ( II Cn x ) , g e. ( II Cn x ) |-> { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )
Theorem	ishtpy 22771*	Membership in the class of homotopies between two continuous functions. (Contributed by Mario Carneiro, 22-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   =>    |- ( ph -> ( H e. ( F ( J Htpy K ) G ) <-> ( H e. ( ( J tX II ) Cn K ) /\ A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) ) ) )
Theorem	htpycn 22772	A homotopy is a continuous function. (Contributed by Mario Carneiro, 22-Feb-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   =>    |- ( ph -> ( F ( J Htpy K ) G ) C_ ( ( J tX II ) Cn K ) )
Theorem	htpyi 22773	A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   &    |- ( ph -> H e. ( F ( J Htpy K ) G ) )   =>    |- ( ( ph /\ A e. X ) -> ( ( A H 0 ) = ( F ` A ) /\ ( A H 1 ) = ( G ` A ) ) )
Theorem	ishtpyd 22774*	Deduction for membership in the class of homotopies. (Contributed by Mario Carneiro, 22-Feb-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   &    |- ( ph -> H e. ( ( J tX II ) Cn K ) )   &    |- ( ( ph /\ s e. X ) -> ( s H 0 ) = ( F ` s ) )   &    |- ( ( ph /\ s e. X ) -> ( s H 1 ) = ( G ` s ) )   =>    |- ( ph -> H e. ( F ( J Htpy K ) G ) )
Theorem	htpycom 22775*	Given a homotopy from F to G, produce a homotopy from G to F. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   &    |- M = ( x e. X , y e. ( 0 [,] 1 ) |-> ( x H ( 1 - y ) ) )   &    |- ( ph -> H e. ( F ( J Htpy K ) G ) )   =>    |- ( ph -> M e. ( G ( J Htpy K ) F ) )
Theorem	htpyid 22776*	A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- G = ( x e. X , y e. ( 0 [,] 1 ) |-> ( F ` x ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   =>    |- ( ph -> G e. ( F ( J Htpy K ) F ) )
Theorem	htpyco1 22777*	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- N = ( x e. X , y e. ( 0 [,] 1 ) |-> ( ( P ` x ) H y ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> P e. ( J Cn K ) )   &    |- ( ph -> F e. ( K Cn L ) )   &    |- ( ph -> G e. ( K Cn L ) )   &    |- ( ph -> H e. ( F ( K Htpy L ) G ) )   =>    |- ( ph -> N e. ( ( F o. P ) ( J Htpy L ) ( G o. P ) ) )
Theorem	htpyco2 22778	Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   &    |- ( ph -> P e. ( K Cn L ) )   &    |- ( ph -> H e. ( F ( J Htpy K ) G ) )   =>    |- ( ph -> ( P o. H ) e. ( ( P o. F ) ( J Htpy L ) ( P o. G ) ) )
Theorem	htpycc 22779*	Concatenate two homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- N = ( x e. X , y e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , ( x L ( 2 x. y ) ) , ( x M ( ( 2 x. y ) - 1 ) ) ) )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> G e. ( J Cn K ) )   &    |- ( ph -> H e. ( J Cn K ) )   &    |- ( ph -> L e. ( F ( J Htpy K ) G ) )   &    |- ( ph -> M e. ( G ( J Htpy K ) H ) )   =>    |- ( ph -> N e. ( F ( J Htpy K ) H ) )
Theorem	isphtpy 22780*	Membership in the class of path homotopies between two continuous functions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ph -> ( H e. ( F ( PHtpy ` J ) G ) <-> ( H e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) ) )
Theorem	phtpyhtpy 22781	A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( F ( II Htpy J ) G ) )
Theorem	phtpycn 22782	A path homotopy is a continuous function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   =>    |- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( ( II tX II ) Cn J ) )
Theorem	phtpyi 22783	Membership in the class of path homotopies between two continuous functions. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )   =>    |- ( ( ph /\ A e. ( 0 [,] 1 ) ) -> ( ( 0 H A ) = ( F ` 0 ) /\ ( 1 H A ) = ( F ` 1 ) ) )
Theorem	phtpy01 22784	Two path-homotopic paths have the same start and end point. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )   =>    |- ( ph -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )
Theorem	isphtpyd 22785*	Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( F ( II Htpy J ) G ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` 0 ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` 1 ) )   =>    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )
Theorem	isphtpy2d 22786*	Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( ( II tX II ) Cn J ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 0 ) = ( F ` s ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 1 ) = ( G ` s ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` 0 ) )   &    |- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` 1 ) )   =>    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )
Theorem	phtpycom 22787*	Given a homotopy from F to G, produce a homotopy from G to F. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x H ( 1 - y ) ) )   &    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )   =>    |- ( ph -> K e. ( G ( PHtpy ` J ) F ) )
Theorem	phtpyid 22788*	A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- G = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` x ) )   &    |- ( ph -> F e. ( II Cn J ) )   =>    |- ( ph -> G e. ( F ( PHtpy ` J ) F ) )
Theorem	phtpyco2 22789	Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> P e. ( J Cn K ) )   &    |- ( ph -> H e. ( F ( PHtpy ` J ) G ) )   =>    |- ( ph -> ( P o. H ) e. ( ( P o. F ) ( PHtpy ` K ) ( P o. G ) ) )
Theorem	phtpycc 22790*	Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 7-Jun-2014.)
|- M = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , ( x K ( 2 x. y ) ) , ( x L ( ( 2 x. y ) - 1 ) ) ) )   &    |- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn J ) )   &    |- ( ph -> H e. ( II Cn J ) )   &    |- ( ph -> K e. ( F ( PHtpy ` J ) G ) )   &    |- ( ph -> L e. ( G ( PHtpy ` J ) H ) )   =>    |- ( ph -> M e. ( F ( PHtpy ` J ) H ) )
Definition	df-phtpc 22791*	Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.)
|- ~=ph = ( x e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) } )
Theorem	phtpcrel 22792	The path homotopy relation is a relation. (Contributed by Mario Carneiro, 7-Jun-2014.) (Revised by Mario Carneiro, 7-Aug-2014.)
|- Rel ( ~=ph ` J )
Theorem	isphtpc 22793	The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- ( F ( ~=ph ` J ) G <-> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )
Theorem	phtpcer 22794	Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 6-Jul-2015.) (Proof shortened by AV, 1-May-2021.)
|- ( ~=ph ` J ) Er ( II Cn J )
Theorem	phtpcerOLD 22795	Obsolete proof of phtpcer 22794 as of 1-May-2021. Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 6-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ~=ph ` J ) Er ( II Cn J )
Theorem	phtpc01 22796	Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( F ( ~=ph ` J ) G -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )
Theorem	reparphti 22797*	Lemma for reparpht 22798. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn II ) )   &    |- ( ph -> ( G ` 0 ) = 0 )   &    |- ( ph -> ( G ` 1 ) = 1 )   &    |- H = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` ( ( ( 1 - y ) x. ( G ` x ) ) + ( y x. x ) ) ) )   =>    |- ( ph -> H e. ( ( F o. G ) ( PHtpy ` J ) F ) )
Theorem	reparpht 22798	Reparametrization lemma. The reparametrization of a path by any continuous map G : II --> II with G ( 0 ) = 0 and G ( 1 ) = 1 is path-homotopic to the original path. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F e. ( II Cn J ) )   &    |- ( ph -> G e. ( II Cn II ) )   &    |- ( ph -> ( G ` 0 ) = 0 )   &    |- ( ph -> ( G ` 1 ) = 1 )   =>    |- ( ph -> ( F o. G ) ( ~=ph ` J ) F )
Theorem	phtpcco2 22799	Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.)
|- ( ph -> F ( ~=ph ` J ) G )   &    |- ( ph -> P e. ( J Cn K ) )   =>    |- ( ph -> ( P o. F ) ( ~=ph ` K ) ( P o. G ) )
12.4.13  The fundamental group
Syntax	cpco 22800	Extend class notation with the concatenation operation for paths in a topological space.
class *p