P. 210 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20901-21000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ufldom 20901	The ultrafilter lemma property is a cardinal invariant, so since it transfers to subsets it also transfers over set dominance. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ( X e. UFL /\ Y ~<_ X ) -> Y e. UFL )
Theorem	flimval 20902*	The set of limit points of a filter. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ F e. U. ran Fil ) -> ( J fLim F ) = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } )
Theorem	elflim2 20903	The predicate "is a limit point of a filter." (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( A e. ( J fLim F ) <-> ( ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P X ) /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
Theorem	flimtop 20904	Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( A e. ( J fLim F ) -> J e. Top )
Theorem	flimneiss 20905	A filter contains the neighborhood filter as a subfilter. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( A e. ( J fLim F ) -> ( ( nei ` J ) ` { A } ) C_ F )
Theorem	flimnei 20906	A filter contains all of the neighborhoods of its limit points. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 9-Apr-2015.)
|- ( ( A e. ( J fLim F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> N e. F )
Theorem	flimelbas 20907	A limit point of a filter belongs to its base set. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 9-Apr-2015.)
|- X = U. J   =>    |- ( A e. ( J fLim F ) -> A e. X )
Theorem	flimfil 20908	Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( A e. ( J fLim F ) -> F e. ( Fil ` X ) )
Theorem	flimtopon 20909	Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( A e. ( J fLim F ) -> ( J e. (TopOn ` X ) <-> F e. ( Fil ` X ) ) )
Theorem	elflim 20910	The predicate "is a limit point of a filter." (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 23-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
Theorem	flimss2 20911	A limit point of a filter is a limit point of a finer filter. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) /\ G C_ F ) -> ( J fLim G ) C_ ( J fLim F ) )
Theorem	flimss1 20912	A limit point of a filter is a limit point in a coarser topology. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) /\ J C_ K ) -> ( K fLim F ) C_ ( J fLim F ) )
Theorem	neiflim 20913	A point is a limit point of its neighborhood filter. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A e. X ) -> A e. ( J fLim ( ( nei ` J ) ` { A } ) ) )
Theorem	flimopn 20914*	The condition for being a limit point of a filter still holds if one only considers open neighborhoods. (Contributed by Jeff Hankins, 4-Sep-2009.) (Proof shortened by Mario Carneiro, 9-Apr-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. x e. J ( A e. x -> x e. F ) ) ) )
Theorem	fbflim 20915*	A condition for a filter to converge to a point involving one of its bases. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- F = ( X filGen B )   =>    |- ( ( J e. (TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. x e. J ( A e. x -> E. y e. B y C_ x ) ) ) )
Theorem	fbflim2 20916*	A condition for a filter base B to converge to a point A. Use neighborhoods instead of open neighborhoods. Compare fbflim 20915. (Contributed by FL, 4-Jul-2011.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- F = ( X filGen B )   =>    |- ( ( J e. (TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n ) ) )
Theorem	flimclsi 20917	The convergent points of a filter are a subset of the closure of any of the filter sets. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( S e. F -> ( J fLim F ) C_ ( ( cls ` J ) ` S ) )
Theorem	hausflimlem 20918	If A and B are both limits of the same filter, then all neighborhoods of A and B intersect. (Contributed by Mario Carneiro, 21-Sep-2015.)
|- ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> ( U i^i V ) =/= (/) )
Theorem	hausflimi 20919*	One direction of hausflim 20920. A filter in a Hausdorff space has at most one limit. (Contributed by FL, 14-Nov-2010.) (Revised by Mario Carneiro, 21-Sep-2015.)
|- ( J e. Haus -> E* x x e. ( J fLim F ) )
Theorem	hausflim 20920*	A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( J e. Haus <-> ( J e. Top /\ A. f e. ( Fil ` X ) E* x x e. ( J fLim f ) ) )
Theorem	flimcf 20921*	Fineness is properly characterized by the property that every limit point of a filter in the finer topology is a limit point in the coarser topology. (Contributed by Jeff Hankins, 28-Sep-2009.) (Revised by Mario Carneiro, 23-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) )
Theorem	flimrest 20922	The set of limit 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 ) fLim ( F ↾t Y ) ) = ( ( J fLim F ) i^i Y ) )
Theorem	flimclslem 20923	Lemma for flimcls 20924. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- F = ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) )   =>    |- ( ( J e. (TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( F e. ( Fil ` X ) /\ S e. F /\ A e. ( J fLim F ) ) )
Theorem	flimcls 20924*	Closure in terms of filter convergence. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ S C_ X ) -> ( A e. ( ( cls ` J ) ` S ) <-> E. f e. ( Fil ` X ) ( S e. f /\ A e. ( J fLim f ) ) ) )
Theorem	flimsncls 20925	If A is a limit point of the filter F, then all the points which specialize A (in the specialization preorder) are also limit points. Thus, the set of limit points is a union of closed sets (although this is only nontrivial for non-T1 spaces). (Contributed by Mario Carneiro, 20-Sep-2015.)
|- ( A e. ( J fLim F ) -> ( ( cls ` J ) ` { A } ) C_ ( J fLim F ) )
Theorem	hauspwpwf1 20926*	Lemma for hauspwpwdom 20927. Points in the closure of a set in a Hausdorff space are characterized by the open neighborhoods they extend into the generating set. (Contributed by Mario Carneiro, 28-Jul-2015.)
|- X = U. J   &    |- F = ( x e. ( ( cls ` J ) ` A ) |-> { a | E. j e. J ( x e. j /\ a = ( j i^i A ) ) } )   =>    |- ( ( J e. Haus /\ A C_ X ) -> F : ( ( cls ` J ) ` A ) -1-1-> ~P ~P A )
Theorem	hauspwpwdom 20927	If X is a Hausdorff space, then the cardinality of the closure of a set A is bounded by the double powerset of A. In particular, a Hausdorff space with a dense subset A has cardinality at most ~P ~P A, and a separable Hausdorff space has cardinality at most ~P ~P NN. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 28-Jul-2015.)
|- X = U. J   =>    |- ( ( J e. Haus /\ A C_ X ) -> ( ( cls ` J ) ` A ) ~<_ ~P ~P A )
Theorem	flffval 20928*	Given a topology and a filtered set, return the convergence function on the functions from the filtered set to the base set of the topological space. (Contributed by Jeff Hankins, 14-Oct-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( J fLimf L ) = ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) )
Theorem	flfval 20929	Given a function from a filtered set to a topological space, define the set of limit points of the function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
Theorem	flfnei 20930*	The property of being a limit point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. s e. L ( F " s ) C_ n ) ) )
Theorem	flfneii 20931*	A neighborhood of a limit point of a function contains the image of a filter element. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> E. s e. L ( F " s ) C_ N )
Theorem	isflf 20932*	The property of being a limit point of a function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. o e. J ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) )
Theorem	flfelbas 20933	A limit point of a function is in the topological space. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.)
|- ( ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. ( ( J fLimf L ) ` F ) ) -> A e. X )
Theorem	flffbas 20934*	Limit points of a function can be defined using filter bases. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- L = ( Y filGen B )   =>    |- ( ( J e. (TopOn ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. o e. J ( A e. o -> E. s e. B ( F " s ) C_ o ) ) ) )
Theorem	flftg 20935*	Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- J = ( topGen ` B )   =>    |- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) )
Theorem	hausflf 20936*	If a function has its values in a Hausdorff space, then it has at most one limit value. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> E* x x e. ( ( J fLimf L ) ` F ) )
Theorem	hausflf2 20937	If a convergent function has its values in a Hausdorff space, then it has a unique limit. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( ( J fLimf L ) ` F ) =/= (/) ) -> ( ( J fLimf L ) ` F ) ~~ 1o )
Theorem	cnpflfi 20938	Forward direction of cnpflf 20940. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( ( A e. ( J fLim L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F ` A ) e. ( ( K fLimf L ) ` F ) )
Theorem	cnpflf2 20939	F is continuous at point A iff a limit of F when x tends to A is ( F ` A ). Proposition 9 of [BourbakiTop1] p. TG I.50. (Contributed by FL, 29-May-2011.) (Revised by Mario Carneiro, 9-Apr-2015.)
|- L = ( ( nei ` J ) ` { A } )   =>    |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( F : X --> Y /\ ( F ` A ) e. ( ( K fLimf L ) ` F ) ) ) )
Theorem	cnpflf 20940*	Continuity of a function at a point in terms of filter limits. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 7-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 fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) ) ) )
Theorem	cnflf 20941*	A function is continuous iff it respects filter limits. (Contributed by Jeff Hankins, 6-Sep-2009.) (Revised by Stefan O'Rear, 7-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 fLim f ) ( F ` x ) e. ( ( K fLimf f ) ` F ) ) ) )
Theorem	cnflf2 20942*	A function is continuous iff it respects filter limits. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( F " ( J fLim f ) ) C_ ( ( K fLimf f ) ` F ) ) ) )
Theorem	flfcnp 20943	A continuous function preserves filter limits. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- ( ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( A e. ( ( J fLimf L ) ` F ) /\ G e. ( ( J CnP K ) ` A ) ) ) -> ( G ` A ) e. ( ( K fLimf L ) ` ( G o. F ) ) )
Theorem	lmflf 20944	The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- Z = ( ZZ>= ` M )   &    |- L = ( Z filGen ( ZZ>= " Z ) )   =>    |- ( ( J e. (TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( F ( ~~> t ` J ) P <-> P e. ( ( J fLimf L ) ` F ) ) )
Theorem	txflf 20945*	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 20946*	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 20947*	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 20948*	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 20949	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 20950	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 20951	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 20952*	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 20953*	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 20954	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 20955	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 20956	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 20957	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 20958*	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 20959*	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 20960*	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 20961	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 20962	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 20963	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 20964*	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 20965	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 20966*	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 20967*	A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 20966, 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 20968	Forward direction of fclscmp 20969. 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 20969*	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 20970	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 20971*	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 20972	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 20973*	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 20974*	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 20975	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 20976	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 20977	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 20978	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 20979	Lemma for cnpfcf 20980. 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 20980*	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 20981*	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	flfcntr 20982	A continuous function's value is always in the trace of its filter limit. (Contributed by Thierry Arnoux, 30-Aug-2020.)
|- C = U. J   &    |- B = U. K   &    |- ( ph -> J e. Top )   &    |- ( ph -> A C_ C )   &    |- ( ph -> F e. ( ( J ↾t A ) Cn K ) )   &    |- ( ph -> X e. A )   =>    |- ( ph -> ( F ` X ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) ↾t A ) ) ` F ) )
Theorem	alexsublem 20983*	Lemma for alexsub 20984. (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 20984*	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 20990 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 20985*	Biconditional form of the Alexander Subbase Theorem alexsub 20984. (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 20986*	Lemma for alexsubALT 20990. 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 20987*	Lemma for alexsubALT 20990. 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 20988*	Lemma for alexsubALT 20990. 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 20989*	Lemma for alexsubALT 20990. 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 20990*	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 20991*	Lemma for ptcmp 20997. (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 20992*	Lemma for ptcmp 20997. (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 20993*	Lemma for ptcmp 20997. (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 20994*	Lemma for ptcmp 20997. (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 20995*	Lemma for ptcmp 20997. (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 20996	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 20997). (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 20997	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 20998	Extend class notation with the continuous extension operation.
class CnExt
Definition	df-cnext 20999*	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 21000*	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 ) ) ) )