P. 209 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20801-20900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	txflf 20801*	Two sequences converge in a filter iff the sequence of their ordered pairs converges. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. ( Fil ` Z ) )   &    |- ( ph -> F : Z --> X )   &    |- ( ph -> G : Z --> Y )   &    |- H = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. )   =>    |- ( ph -> ( <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` H ) <-> ( R e. ( ( J fLimf L ) ` F ) /\ S e. ( ( K fLimf L ) ` G ) ) ) )
Theorem	flfcnp2 20802*	The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. ( Fil ` Z ) )   &    |- ( ( ph /\ x e. Z ) -> A e. X )   &    |- ( ( ph /\ x e. Z ) -> B e. Y )   &    |- ( ph -> R e. ( ( J fLimf L ) ` ( x e. Z |-> A ) ) )   &    |- ( ph -> S e. ( ( K fLimf L ) ` ( x e. Z |-> B ) ) )   &    |- ( ph -> O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) )   =>    |- ( ph -> ( R O S ) e. ( ( N fLimf L ) ` ( x e. Z |-> ( A O B ) ) ) )
Theorem	fclsval 20803*	The set of all cluster points of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> ( J fClus F ) = if ( X = Y , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) )
Theorem	isfcls 20804*	A cluster point of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- X = U. J   =>    |- ( A e. ( J fClus F ) <-> ( J e. Top /\ F e. ( Fil ` X ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )
Theorem	fclsfil 20805	Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- X = U. J   =>    |- ( A e. ( J fClus F ) -> F e. ( Fil ` X ) )
Theorem	fclstop 20806	Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( A e. ( J fClus F ) -> J e. Top )
Theorem	fclstopon 20807	Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( A e. ( J fClus F ) -> ( J e. (TopOn ` X ) <-> F e. ( Fil ` X ) ) )
Theorem	isfcls2 20808*	A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) )
Theorem	fclsopn 20809*	Write the cluster point condition in terms of open sets. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
Theorem	fclsopni 20810	An open neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( A e. ( J fClus F ) /\ ( U e. J /\ A e. U /\ S e. F ) ) -> ( U i^i S ) =/= (/) )
Theorem	fclselbas 20811	A cluster point is in the base set. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- X = U. J   =>    |- ( A e. ( J fClus F ) -> A e. X )
Theorem	fclsneii 20812	A neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> ( N i^i S ) =/= (/) )
Theorem	fclssscls 20813	The set of cluster points is a subset of the closure of any filter element. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( S e. F -> ( J fClus F ) C_ ( ( cls ` J ) ` S ) )
Theorem	fclsnei 20814*	Cluster points in terms of neighborhoods. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) ) )
Theorem	supnfcls 20815*	The filter of supersets of X \ U does not cluster at any point of the open set U. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ U e. J /\ A e. U ) -> -. A e. ( J fClus { x e. ~P X | ( X \ U ) C_ x } ) )
Theorem	fclsbas 20816*	Cluster points in terms of filter bases. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- F = ( X filGen B )   =>    |- ( ( J e. (TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. B ( o i^i s ) =/= (/) ) ) ) )
Theorem	fclsss1 20817	A finer topology has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) -> ( K fClus F ) C_ ( J fClus F ) )
Theorem	fclsss2 20818	A finer filter has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) /\ F C_ G ) -> ( J fClus G ) C_ ( J fClus F ) )
Theorem	fclsrest 20819	The set of cluster points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( ( J ↾t Y ) fClus ( F ↾t Y ) ) = ( ( J fClus F ) i^i Y ) )
Theorem	fclscf 20820*	Characterization of fineness of topologies in terms of cluster points. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fClus f ) C_ ( J fClus f ) ) )
Theorem	flimfcls 20821	A limit point is a cluster point. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( J fLim F ) C_ ( J fClus F )
Theorem	fclsfnflim 20822*	A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- ( F e. ( Fil ` X ) -> ( A e. ( J fClus F ) <-> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) )
Theorem	flimfnfcls 20823*	A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 20822, this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- X = U. J   =>    |- ( F e. ( Fil ` X ) -> ( A e. ( J fLim F ) <-> A. g e. ( Fil ` X ) ( F C_ g -> A e. ( J fClus g ) ) ) )
Theorem	fclscmpi 20824	Forward direction of fclscmp 20825. Every filter clusters in a compact space. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( J fClus F ) =/= (/) )
Theorem	fclscmp 20825*	A space is compact iff every filter clusters. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( J e. (TopOn ` X ) -> ( J e. Comp <-> A. f e. ( Fil ` X ) ( J fClus f ) =/= (/) ) )
Theorem	uffclsflim 20826	The cluster points of an ultrafilter are its limit points. (Contributed by Jeff Hankins, 11-Dec-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- ( F e. ( UFil ` X ) -> ( J fClus F ) = ( J fLim F ) )
Theorem	ufilcmp 20827*	A space is compact iff every ultrafilter converges. (Contributed by Jeff Hankins, 11-Dec-2009.) (Proof shortened by Mario Carneiro, 12-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- ( ( X e. UFL /\ J e. (TopOn ` X ) ) -> ( J e. Comp <-> A. f e. ( UFil ` X ) ( J fLim f ) =/= (/) ) )
Theorem	fcfval 20828	The set of cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( J fClus ( ( X FilMap F ) ` L ) ) )
Theorem	isfcf 20829*	The property of being a cluster point of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) ) )
Theorem	fcfnei 20830*	The property of being a cluster point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) ) ) )
Theorem	fcfelbas 20831	A cluster point of a function is in the base set of the topology. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fClusf L ) ` F ) ) -> A e. X )
Theorem	fcfneii 20832	A neighborhood of a cluster point of a function contains a function value from every tail. (Contributed by Jeff Hankins, 27-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fClusf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. L ) ) -> ( N i^i ( F " S ) ) =/= (/) )
Theorem	flfssfcf 20833	A limit point of a function is a cluster point of the function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) C_ ( ( J fClusf L ) ` F ) )
Theorem	uffcfflf 20834	If the domain filter is an ultrafilter, the cluster points of the function are the limit points. (Contributed by Jeff Hankins, 12-Dec-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( ( J fLimf L ) ` F ) )
Theorem	cnpfcfi 20835	Lemma for cnpfcf 20836. If a function is continuous at a point, it respects clustering there. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F ` A ) e. ( ( K fClusf L ) ` F ) )
Theorem	cnpfcf 20836*	A function F is continuous at point A iff F respects cluster points there. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) ) ) )
Theorem	cnfcf 20837*	Continuity of a function in terms of cluster points of a function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) A. x e. ( J fClus f ) ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )
Theorem	alexsublem 20838*	Lemma for alexsub 20839. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ph -> X e. UFL )   &    |- ( ph -> X = U. B )   &    |- ( ph -> J = ( topGen ` ( fi ` B ) ) )   &    |- ( ( ph /\ ( x C_ B /\ X = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y )   &    |- ( ph -> F e. ( UFil ` X ) )   &    |- ( ph -> ( J fLim F ) = (/) )   =>    |- -. ph
Theorem	alexsub 20839*	The Alexander Subbase Theorem: If B is a subbase for the topology J, and any cover taken from B has a finite subcover, then the generated topology is compact. This proof uses the ultrafilter lemma; see alexsubALT 20845 for a proof using Zorn's lemma. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- ( ph -> X e. UFL )   &    |- ( ph -> X = U. B )   &    |- ( ph -> J = ( topGen ` ( fi ` B ) ) )   &    |- ( ( ph /\ ( x C_ B /\ X = U. x ) ) -> E. y e. ( ~P x i^i Fin ) X = U. y )   =>    |- ( ph -> J e. Comp )
Theorem	alexsubb 20840*	Biconditional form of the Alexander Subbase Theorem alexsub 20839. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- ( ( X e. UFL /\ X = U. B ) -> ( ( topGen ` ( fi ` B ) ) e. Comp <-> A. x e. ~P B ( X = U. x -> E. y e. ( ~P x i^i Fin ) X = U. y ) ) )
Theorem	alexsubALTlem1 20841*	Lemma for alexsubALT 20845. A compact space has a subbase such that every cover taken from it has a finite subcover. (Contributed by Jeff Hankins, 27-Jan-2010.)
|- X = U. J   =>    |- ( J e. Comp -> E. x ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
Theorem	alexsubALTlem2 20842*	Lemma for alexsubALT 20845. Every subset of a base which has no finite subcover is a subset of a maximal such collection. (Contributed by Jeff Hankins, 27-Jan-2010.)
|- X = U. J   =>    |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> E. u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v )
Theorem	alexsubALTlem3 20843*	Lemma for alexsubALT 20845. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)
|- X = U. J   =>    |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n )
Theorem	alexsubALTlem4 20844*	Lemma for alexsubALT 20845. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)
|- X = U. J   =>    |- ( J = ( topGen ` ( fi ` x ) ) -> ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) )
Theorem	alexsubALT 20845*	The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 11-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = U. J   =>    |- ( J e. Comp <-> E. x ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
Theorem	ptcmplem1 20846*	Lemma for ptcmp 20852. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )   &    |- X = X_ n e. A U. ( F ` n )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> Comp )   &    |- ( ph -> X e. (UFL i^i dom card ) )   =>    |- ( ph -> ( X = U. ( ran S u. { X } ) /\ ( Xt_ ` F ) = ( topGen ` ( fi ` ( ran S u. { X } ) ) ) ) )
Theorem	ptcmplem2 20847*	Lemma for ptcmp 20852. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )   &    |- X = X_ n e. A U. ( F ` n )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> Comp )   &    |- ( ph -> X e. (UFL i^i dom card ) )   &    |- ( ph -> U C_ ran S )   &    |- ( ph -> X = U. U )   &    |- ( ph -> -. E. z e. ( ~P U i^i Fin ) X = U. z )   =>    |- ( ph -> U_ k e. { n e. A | -. U. ( F ` n ) ~~ 1o } U. ( F ` k ) e. dom card )
Theorem	ptcmplem3 20848*	Lemma for ptcmp 20852. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )   &    |- X = X_ n e. A U. ( F ` n )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> Comp )   &    |- ( ph -> X e. (UFL i^i dom card ) )   &    |- ( ph -> U C_ ran S )   &    |- ( ph -> X = U. U )   &    |- ( ph -> -. E. z e. ( ~P U i^i Fin ) X = U. z )   &    |- K = { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U }   =>    |- ( ph -> E. f ( f Fn A /\ A. k e. A ( f ` k ) e. ( U. ( F ` k ) \ U. K ) ) )
Theorem	ptcmplem4 20849*	Lemma for ptcmp 20852. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )   &    |- X = X_ n e. A U. ( F ` n )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> Comp )   &    |- ( ph -> X e. (UFL i^i dom card ) )   &    |- ( ph -> U C_ ran S )   &    |- ( ph -> X = U. U )   &    |- ( ph -> -. E. z e. ( ~P U i^i Fin ) X = U. z )   &    |- K = { u e. ( F ` k ) | ( `' ( w e. X |-> ( w ` k ) ) " u ) e. U }   =>    |- -. ph
Theorem	ptcmplem5 20850*	Lemma for ptcmp 20852. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )   &    |- X = X_ n e. A U. ( F ` n )   &    |- ( ph -> A e. V )   &    |- ( ph -> F : A --> Comp )   &    |- ( ph -> X e. (UFL i^i dom card ) )   =>    |- ( ph -> ( Xt_ ` F ) e. Comp )
Theorem	ptcmpg 20851	Tychonoff's theorem: The product of compact spaces is compact. The choice principles needed are encoded in the last hypothesis: the base set of the product must be well-orderable and satisfy the ultrafilter lemma. Both these assumptions are satisfied if ~P ~P X is well-orderable, so if we assume the Axiom of Choice we can eliminate them (see ptcmp 20852). (Contributed by Mario Carneiro, 27-Aug-2015.)
|- J = ( Xt_ ` F )   &    |- X = U. J   =>    |- ( ( A e. V /\ F : A --> Comp /\ X e. (UFL i^i dom card ) ) -> J e. Comp )
Theorem	ptcmp 20852	Tychonoff's theorem: The product of compact spaces is compact. The proof uses the Axiom of Choice. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ( A e. V /\ F : A --> Comp ) -> ( Xt_ ` F ) e. Comp )
12.2.5  Extension by continuity
Syntax	ccnext 20853	Extend class notation with the continuous extension operation.
class CnExt
Definition	df-cnext 20854*	Define the continuous extension of a given function. (Contributed by Thierry Arnoux, 1-Dec-2017.)
|- CnExt = ( j e. Top , k e. Top |-> ( f e. ( U. k ^pm U. j ) |-> U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) ↾t dom f ) ) ` f ) ) ) )
Theorem	cnextval 20855*	The function applying continuous extension to a given function f. (Contributed by Thierry Arnoux, 1-Dec-2017.)
|- ( ( J e. Top /\ K e. Top ) -> ( JCnExt K ) = ( f e. ( U. K ^pm U. J ) |-> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t dom f ) ) ` f ) ) ) )
Theorem	cnextfval 20856*	The continuous extension of a given function F. (Contributed by Thierry Arnoux, 1-Dec-2017.)
|- X = U. J   &    |- B = U. K   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> ( ( JCnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ) )
Theorem	cnextrel 20857	In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.)
|- C = U. J   &    |- B = U. K   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( JCnExt K ) ` F ) )
Theorem	cnextfun 20858	If the target space is Hausdorff, a continuous extension is a function (Contributed by Thierry Arnoux, 20-Dec-2017.)
|- C = U. J   &    |- B = U. K   =>    |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( JCnExt K ) ` F ) )
Theorem	cnextfvval 20859*	The value of the continuous extension of a given function F at a point X. (Contributed by Thierry Arnoux, 21-Dec-2017.)
|- C = U. J   &    |- B = U. K   &    |- ( ph -> J e. Top )   &    |- ( ph -> K e. Haus )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> A C_ C )   &    |- ( ph -> ( ( cls ` J ) ` A ) = C )   &    |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) )   =>    |- ( ( ph /\ X e. C ) -> ( ( ( JCnExt K ) ` F ) ` X ) = U. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) ↾t A ) ) ` F ) )
Theorem	cnextf 20860*	Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017.)
|- C = U. J   &    |- B = U. K   &    |- ( ph -> J e. Top )   &    |- ( ph -> K e. Haus )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> A C_ C )   &    |- ( ph -> ( ( cls ` J ) ` A ) = C )   &    |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) )   =>    |- ( ph -> ( ( JCnExt K ) ` F ) : C --> B )
Theorem	cnextcn 20861*	Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology J on C, a subset A dense in C, this states a condition for F from A to a regular space K to be extensible by continuity (Contributed by Thierry Arnoux, 1-Jan-2018.)
|- C = U. J   &    |- B = U. K   &    |- ( ph -> J e. Top )   &    |- ( ph -> K e. Haus )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> A C_ C )   &    |- ( ph -> ( ( cls ` J ) ` A ) = C )   &    |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) )   &    |- ( ph -> K e. Reg )   =>    |- ( ph -> ( ( JCnExt K ) ` F ) e. ( J Cn K ) )
Theorem	cnextfres 20862*	F and its extension by continuity agree on the domain of F. (Contributed by Thierry Arnoux, 17-Jan-2018.)
|- C = U. J   &    |- B = U. K   &    |- ( ph -> J e. Top )   &    |- ( ph -> K e. Haus )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> A C_ C )   &    |- ( ph -> ( ( cls ` J ) ` A ) = C )   &    |- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) =/= (/) )   &    |- ( ph -> K e. Reg )   &    |- ( ph -> F e. ( ( J ↾t A ) Cn K ) )   =>    |- ( ph -> ( ( ( JCnExt K ) ` F ) |` A ) = F )
12.2.6  Topological groups
Syntax	ctmd 20863	Extend class notation with the class of all topological monoids.
class TopMnd
Syntax	ctgp 20864	Extend class notation with the class of all topological groups.
class TopGrp
Definition	df-tmd 20865*	Define the class of all topological monoids. A topological monoid is a monoid whose operation is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- TopMnd = { f e. ( Mnd i^i TopSp ) | [. ( TopOpen ` f ) / j ]. ( +f ` f ) e. ( ( j tX j ) Cn j ) }
Definition	df-tgp 20866*	Define the class of all topological groups. A topological group is a group whose operation and inverse function are continuous. (Contributed by FL, 18-Apr-2010.)
|- TopGrp = { f e. ( Grp i^i TopMnd ) | [. ( TopOpen ` f ) / j ]. ( invg ` f ) e. ( j Cn j ) }
Theorem	istmd 20867	The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.)
|- F = ( +f ` G )   &    |- J = ( TopOpen ` G )   =>    |- ( G e. TopMnd <-> ( G e. Mnd /\ G e. TopSp /\ F e. ( ( J tX J ) Cn J ) ) )
Theorem	tmdmnd 20868	A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- ( G e. TopMnd -> G e. Mnd )
Theorem	tmdtps 20869	A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- ( G e. TopMnd -> G e. TopSp )
Theorem	istgp 20870	The predicate "is a topological group". Definition of [BourbakiTop1] p. III.1 (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- J = ( TopOpen ` G )   &    |- I = ( invg ` G )   =>    |- ( G e. TopGrp <-> ( G e. Grp /\ G e. TopMnd /\ I e. ( J Cn J ) ) )
Theorem	tgpgrp 20871	A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- ( G e. TopGrp -> G e. Grp )
Theorem	tgptmd 20872	A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- ( G e. TopGrp -> G e. TopMnd )
Theorem	tgptps 20873	A topological group is a topological space. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- ( G e. TopGrp -> G e. TopSp )
Theorem	tmdtopon 20874	The topology of a topological monoid. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- J = ( TopOpen ` G )   &    |- X = ( Base ` G )   =>    |- ( G e. TopMnd -> J e. (TopOn ` X ) )
Theorem	tgptopon 20875	The topology of a topological group. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- J = ( TopOpen ` G )   &    |- X = ( Base ` G )   =>    |- ( G e. TopGrp -> J e. (TopOn ` X ) )
Theorem	tmdcn 20876	In a topological monoid, the operation F representing the functionalization of the operator slot +g is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- J = ( TopOpen ` G )   &    |- F = ( +f ` G )   =>    |- ( G e. TopMnd -> F e. ( ( J tX J ) Cn J ) )
Theorem	tgpcn 20877	In a topological group, the operation F representing the functionalization of the operator slot +g is continuous. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- J = ( TopOpen ` G )   &    |- F = ( +f ` G )   =>    |- ( G e. TopGrp -> F e. ( ( J tX J ) Cn J ) )
Theorem	tgpinv 20878	In a topological group, the inverse function is continuous. (Contributed by FL, 21-Jun-2010.) (Revised by FL, 27-Jun-2014.)
|- J = ( TopOpen ` G )   &    |- I = ( invg ` G )   =>    |- ( G e. TopGrp -> I e. ( J Cn J ) )
Theorem	grpinvhmeo 20879	The inverse function in a topological group is a homeomorphism from the group to itself. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- J = ( TopOpen ` G )   &    |- I = ( invg ` G )   =>    |- ( G e. TopGrp -> I e. ( J Homeo J ) )
Theorem	cnmpt1plusg 20880*	Continuity of the group sum; analogue of cnmpt12f 20461 which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- J = ( TopOpen ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. TopMnd )   &    |- ( ph -> K e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( K Cn J ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( K Cn J ) )   =>    |- ( ph -> ( x e. X |-> ( A .+ B ) ) e. ( K Cn J ) )
Theorem	cnmpt2plusg 20881*	Continuity of the group sum; analogue of cnmpt22f 20470 which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- J = ( TopOpen ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. TopMnd )   &    |- ( ph -> K e. (TopOn ` X ) )   &    |- ( ph -> L e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )   &    |- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> ( A .+ B ) ) e. ( ( K tX L ) Cn J ) )
Theorem	tmdcn2 20882*	Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- B = ( Base ` G )   &    |- J = ( TopOpen ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> E. u e. J E. v e. J ( X e. u /\ Y e. v /\ A. x e. u A. y e. v ( x .+ y ) e. U ) )
Theorem	tgpsubcn 20883	In a topological group, the "subtraction" (or "division") is continuous. Axiom GT' of [BourbakiTop1] p. III.1 (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 19-Mar-2015.)
|- J = ( TopOpen ` G )   &    |- .- = ( -g ` G )   =>    |- ( G e. TopGrp -> .- e. ( ( J tX J ) Cn J ) )
Theorem	istgp2 20884	A group with a topology is a topological group iff the subtraction operation is continuous. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` G )   &    |- .- = ( -g ` G )   =>    |- ( G e. TopGrp <-> ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) )
Theorem	tmdmulg 20885*	In a topological monoid, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- J = ( TopOpen ` G )   &    |- .x. = (.g ` G )   &    |- B = ( Base ` G )   =>    |- ( ( G e. TopMnd /\ N e. NN0 ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )
Theorem	tgpmulg 20886*	In a topological group, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- J = ( TopOpen ` G )   &    |- .x. = (.g ` G )   &    |- B = ( Base ` G )   =>    |- ( ( G e. TopGrp /\ N e. ZZ ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )
Theorem	tgpmulg2 20887	In a topological monoid, the group multiple function is jointly continuous (although this is not saying much as one of the factors is discrete). Use zdis 21615 to write the left topology as a subset of the complex numbers. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- J = ( TopOpen ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. TopGrp -> .x. e. ( ( ~P ZZ tX J ) Cn J ) )
Theorem	tmdgsum 20888*	In a topological monoid, the group sum operation is a continuous function from the function space to the base topology. This theorem is not true when A is infinite, because in this case for any basic open set of the domain one of the factors will be the whole space, so by varying the value of the functions to sum at this index, one can achieve any desired sum. (Contributed by Mario Carneiro, 19-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.)
|- J = ( TopOpen ` G )   &    |- B = ( Base ` G )   =>    |- ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( x e. ( B ^m A ) |-> ( G gsumg x ) ) e. ( ( J ^ko ~P A ) Cn J ) )
Theorem	tmdgsum2 20889*	For any neighborhood U of n X, there is a neighborhood u of X such that any sum of n elements in u sums to an element of U. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- J = ( TopOpen ` G )   &    |- B = ( Base ` G )   &    |- .x. = (.g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> G e. TopMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> U e. J )   &    |- ( ph -> X e. B )   &    |- ( ph -> ( ( # ` A ) .x. X ) e. U )   =>    |- ( ph -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsumg f ) e. U ) )
Theorem	oppgtmd 20890	The opposite of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- O = (oppg ` G )   =>    |- ( G e. TopMnd -> O e. TopMnd )
Theorem	oppgtgp 20891	The opposite of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.)
|- O = (oppg ` G )   =>    |- ( G e. TopGrp -> O e. TopGrp )
Theorem	distgp 20892	Any group equipped with the discrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- J = ( TopOpen ` G )   =>    |- ( ( G e. Grp /\ J = ~P B ) -> G e. TopGrp )
Theorem	indistgp 20893	Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- J = ( TopOpen ` G )   =>    |- ( ( G e. Grp /\ J = { (/) , B } ) -> G e. TopGrp )
Theorem	symgtgp 20894	The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- G = ( SymGrp ` A )   =>    |- ( A e. V -> G e. TopGrp )
Theorem	tmdlactcn 20895*	The left group action of element A in a topological monoid G is a continuous function. (Contributed by FL, 18-Mar-2008.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- F = ( x e. X |-> ( A .+ x ) )   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- J = ( TopOpen ` G )   =>    |- ( ( G e. TopMnd /\ A e. X ) -> F e. ( J Cn J ) )
Theorem	tgplacthmeo 20896*	The left group action of element A in a topological group G is a homeomorphism from the group to itself. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- F = ( x e. X |-> ( A .+ x ) )   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- J = ( TopOpen ` G )   =>    |- ( ( G e. TopGrp /\ A e. X ) -> F e. ( J Homeo J ) )
Theorem	submtmd 20897	A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- H = ( G ↾s S )   =>    |- ( ( G e. TopMnd /\ S e. (SubMnd ` G ) ) -> H e. TopMnd )
Theorem	subgtgp 20898	A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.)
|- H = ( G ↾s S )   =>    |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) ) -> H e. TopGrp )
Theorem	subgntr 20899	A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg 20901, the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- J = ( TopOpen ` G )   =>    |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ A e. ( ( int ` J ) ` S ) ) -> S e. J )
Theorem	opnsubg 20900	An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015.)
|- J = ( TopOpen ` G )   =>    |- ( ( G e. TopGrp /\ S e. (SubGrp ` G ) /\ S e. J ) -> S e. ( Clsd ` J ) )