P. 155 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15401-15500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	innei 15401	The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property Vii of [BourbakiTop1] p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) -> ( N i^i M ) e. ( ( nei ` J ) ` S ) )
Theorem	opnneiid 15402	Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.)
|- ( J e. Top -> ( N e. ( ( nei ` J ) ` N ) <-> N e. J ) )
Theorem	neissex 15403*	For any neighborhood N of S, there is a neighborhood x of S such that N is a neighborhood of all subsets of x. Generalization to subsets of Property Viv of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. ( ( nei ` J ) ` S ) A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
Theorem	0nei 15404	The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)
|- ( J e. Top -> (/) e. ( ( nei ` J ) ` (/) ) )
9.1.6  Subspace topologies
Theorem	restrcl 15405	Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Jim Kingdon, 23-Mar-2023.)
|- ( ( J ↾t A ) e. Top -> ( J e. _V /\ A e. _V ) )
Theorem	restbasg 15406	A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( B e. TopBases /\ A e. V ) -> ( B ↾t A ) e. TopBases )
Theorem	tgrest 15407	A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Mario Carneiro, 30-Aug-2015.)
|- ( ( B e. V /\ A e. W ) -> ( topGen ` ( B ↾t A ) ) = ( ( topGen ` B ) ↾t A ) )
Theorem	resttop 15408	A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. A is normally a subset of the base set of J. (Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. Top /\ A e. V ) -> ( J ↾t A ) e. Top )
Theorem	resttopon 15409	A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) e. (TopOn ` A ) )
Theorem	restuni 15410	The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> A = U. ( J ↾t A ) )
Theorem	stoig 15411	The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , ( J ↾t A ) >. } e. TopSp )
Theorem	restco 15412	Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J ↾t A ) ↾t B ) = ( J ↾t ( A i^i B ) ) )
Theorem	restabs 15413	Equivalence of being a subspace of a subspace and being a subspace of the original. (Contributed by Jeff Hankins, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ S C_ T /\ T e. W ) -> ( ( J ↾t T ) ↾t S ) = ( J ↾t S ) )
Theorem	restin 15414	When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013.)
|- X = U. J   =>    |- ( ( J e. V /\ A e. W ) -> ( J ↾t A ) = ( J ↾t ( A i^i X ) ) )
Theorem	restuni2 15415	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J ↾t A ) )
Theorem	resttopon2 15416	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A e. V ) -> ( J ↾t A ) e. (TopOn ` ( A i^i X ) ) )
Theorem	rest0 15417	The subspace topology induced by the topology J on the empty set. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( J e. Top -> ( J ↾t (/) ) = { (/) } )
Theorem	restsn 15418	The only subspace topology induced by the topology { (/) }. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( A e. V -> ( { (/) } ↾t A ) = { (/) } )
Theorem	restopnb 15419	If B is an open subset of the subspace base set A, then any subset of B is open iff it is open in A. (Contributed by Mario Carneiro, 2-Mar-2015.)
|- ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( C e. J <-> C e. ( J ↾t A ) ) )
Theorem	ssrest 15420	If K is a finer topology than J, then the subspace topologies induced by A maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( K e. V /\ J C_ K ) -> ( J ↾t A ) C_ ( K ↾t A ) )
Theorem	restopn2 15421	If A is open, then B is open in A iff it is an open subset of A. (Contributed by Mario Carneiro, 2-Mar-2015.)
|- ( ( J e. Top /\ A e. J ) -> ( B e. ( J ↾t A ) <-> ( B e. J /\ B C_ A ) ) )
Theorem	restdis 15422	A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( A e. V /\ B C_ A ) -> ( ~P A ↾t B ) = ~P B )
9.1.7  Limits and continuity in topological spaces
Syntax	ccn 15423	Extend class notation with the class of continuous functions between topologies.
class Cn
Syntax	ccnp 15424	Extend class notation with the class of functions between topologies continuous at a given point.
class CnP
Syntax	clm 15425	Extend class notation with a function on topological spaces whose value is the convergence relation for limit sequences in the space.
class ~~> t
Definition	df-cn 15426*	Define a function on two topologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in [Munkres] p. 102. See iscn 15435 for the predicate form. (Contributed by NM, 17-Oct-2006.)
|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
Definition	df-cnp 15427*	Define a function on two topologies whose value is the set of continuous mappings at a specified point in the first topology. Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.)
|- CnP = ( j e. Top , k e. Top |-> ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } ) )
Definition	df-lm 15428*	Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although f is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function ( x e. RR |-> ( sin ` ( pi x. x ) ) ) converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.)
|- ~~> t = ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
Theorem	lmrel 15429	The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
|- Rel ( ~~> t ` J )
Theorem	lmrcl 15430	Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.)
|- ( F ( ~~> t ` J ) P -> J e. Top )
Theorem	lmfval 15431*	The relation "sequence f converges to point y " in a metric space. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( J e. (TopOn ` X ) -> ( ~~> t ` J ) = { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
Theorem	cnfval 15432*	The set of all continuous functions from topology J to topology K. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( J Cn K ) = { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } )
Theorem	cnpfval 15433*	The function mapping the points in a topology J to the set of all functions from J to topology K continuous at that point. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( J CnP K ) = ( x e. X |-> { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } ) )
Theorem	cnovex 15434	The class of all continuous functions from a topology to another is a set. (Contributed by Jim Kingdon, 14-Dec-2023.)
|- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V )
Theorem	iscn 15435*	The predicate "the class F is a continuous function from topology J to topology K". Definition of continuous function in [Munkres] p. 102. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
Theorem	cnpval 15436*	The set of all functions from topology J to topology K that are continuous at a point P. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( ( J CnP K ) ` P ) = { f e. ( Y ^m X ) | A. y e. K ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) } )
Theorem	iscnp 15437*	The predicate "the class F is a continuous function from topology J to topology K at point P". Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
Theorem	iscn2 15438*	The predicate "the class F is a continuous function from topology J to topology K". Definition of continuous function in [Munkres] p. 102. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
Theorem	cntop1 15439	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> J e. Top )
Theorem	cntop2 15440	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> K e. Top )
Theorem	iscnp3 15441*	The predicate "the class F is a continuous function from topology J to topology K at point P". (Contributed by NM, 15-May-2007.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) ) ) )
Theorem	cnf 15442	A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( F e. ( J Cn K ) -> F : X --> Y )
Theorem	cnf2 15443	A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( J Cn K ) ) -> F : X --> Y )
Theorem	cnprcl2k 15444	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|- ( ( J e. (TopOn ` X ) /\ K e. Top /\ F e. ( ( J CnP K ) ` P ) ) -> P e. X )
Theorem	cnpf2 15445	A continuous function at point P is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
Theorem	tgcn 15446*	The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K = ( topGen ` B ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   =>    |- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )
Theorem	tgcnp 15447*	The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K = ( topGen ` B ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> P e. X )   =>    |- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
Theorem	ssidcn 15448	The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) -> ( ( _I |` X ) e. ( J Cn K ) <-> K C_ J ) )
Theorem	icnpimaex 15449*	Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) (Revised by Jim Kingdon, 28-Mar-2023.)
|- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. K /\ ( F ` P ) e. A ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ A ) )
Theorem	idcn 15450	A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
|- ( J e. (TopOn ` X ) -> ( _I |` X ) e. ( J Cn J ) )
Theorem	lmbr 15451*	Express the binary relation "sequence F converges to point P " in a topological space. Definition 1.4-1 of [Kreyszig] p. 25. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm 15428. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ( ph -> J e. (TopOn ` X ) )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) ) )
Theorem	lmbr2 15452*	Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
Theorem	lmbrf 15453*	Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. This version of lmbr2 15452 presupposes that F is a function. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> X )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) A e. u ) ) ) )
Theorem	lmconst 15454	A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( J e. (TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> ( Z X. { P } ) ( ~~> t ` J ) P )
Theorem	lmcvg 15455*	Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> P e. U )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> U e. J )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. U )
Theorem	iscnp4 15456*	The predicate "the class F is a continuous function from topology J to topology K at point P " in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) ) )
Theorem	cnpnei 15457*	A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top /\ F : X --> Y ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> A. y e. ( ( nei ` K ) ` { ( F ` A ) } ) ( `' F " y ) e. ( ( nei ` J ) ` { A } ) ) )
Theorem	cnima 15458	An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.)
|- ( ( F e. ( J Cn K ) /\ A e. K ) -> ( `' F " A ) e. J )
Theorem	cnco 15459	The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> ( G o. F ) e. ( J Cn L ) )
Theorem	cnptopco 15460	The composition of a function F continuous at P with a function continuous at ( F ` P ) is continuous at P. Proposition 2 of [BourbakiTop1] p. I.9. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
|- ( ( ( J e. Top /\ K e. Top /\ L e. Top ) /\ ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) ) -> ( G o. F ) e. ( ( J CnP L ) ` P ) )
Theorem	cnclima 15461	A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( `' F " A ) e. ( Clsd ` J ) )
Theorem	cnntri 15462	Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- Y = U. K   =>    |- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( `' F " ( ( int ` K ) ` S ) ) C_ ( ( int ` J ) ` ( `' F " S ) ) )
Theorem	cnntr 15463*	Continuity in terms of interior. (Contributed by Jeff Hankins, 2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ~P Y ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) ) )
Theorem	cnss1 15464	If the topology K is finer than J, then there are more continuous functions from K than from J. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   =>    |- ( ( K e. (TopOn ` X ) /\ J C_ K ) -> ( J Cn L ) C_ ( K Cn L ) )
Theorem	cnss2 15465	If the topology K is finer than J, then there are fewer continuous functions into K than into J from some other space. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- Y = U. K   =>    |- ( ( L e. (TopOn ` Y ) /\ L C_ K ) -> ( J Cn K ) C_ ( J Cn L ) )
Theorem	cncnpi 15466	A continuous function is continuous at all points. One direction of Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Cn K ) /\ A e. X ) -> F e. ( ( J CnP K ) ` A ) )
Theorem	cnsscnp 15467	The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   =>    |- ( P e. X -> ( J Cn K ) C_ ( ( J CnP K ) ` P ) )
Theorem	cncnp 15468*	A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) )
Theorem	cncnp2m 15469*	A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Jim Kingdon, 30-Mar-2023.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( J e. Top /\ K e. Top /\ E. y y e. X ) -> ( F e. ( J Cn K ) <-> A. x e. X F e. ( ( J CnP K ) ` x ) ) )
Theorem	cnnei 15470*	Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( J e. Top /\ K e. Top /\ F : X --> Y ) -> ( F e. ( J Cn K ) <-> A. p e. X A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) )
Theorem	cnconst2 15471	A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ B e. Y ) -> ( X X. { B } ) e. ( J Cn K ) )
Theorem	cnconst 15472	A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.)
|- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) /\ ( B e. Y /\ F : X --> { B } ) ) -> F e. ( J Cn K ) )
Theorem	cnrest 15473	Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( F |` A ) e. ( ( J ↾t A ) Cn K ) )
Theorem	cnrest2 15474	Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
|- ( ( K e. (TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K ↾t B ) ) ) )
Theorem	cnrest2r 15475	Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.)
|- ( K e. Top -> ( J Cn ( K ↾t B ) ) C_ ( J Cn K ) )
Theorem	cnptopresti 15476	One direction of cnptoprest 15477 under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 31-Mar-2023.)
|- ( ( ( J e. (TopOn ` X ) /\ K e. Top ) /\ ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) ) -> ( F |` A ) e. ( ( ( J ↾t A ) CnP K ) ` P ) )
Theorem	cnptoprest 15477	Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 5-Apr-2023.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F |` A ) e. ( ( ( J ↾t A ) CnP K ) ` P ) ) )
Theorem	cnptoprest2 15478	Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 6-Apr-2023.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( F : X --> B /\ B C_ Y ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> F e. ( ( J CnP ( K ↾t B ) ) ` P ) ) )
Theorem	cndis 15479	Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( A e. V /\ J e. (TopOn ` X ) ) -> ( ~P A Cn J ) = ( X ^m A ) )
Theorem	cnpdis 15480	If A is an isolated point in X (or equivalently, the singleton { A } is open in X), then every function is continuous at A. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( ( J CnP K ) ` A ) = ( Y ^m X ) )
Theorem	lmfpm 15481	If F converges, then F is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- ( ( J e. (TopOn ` X ) /\ F ( ~~> t ` J ) P ) -> F e. ( X ^pm CC ) )
Theorem	lmfss 15482	Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition). (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- ( ( J e. (TopOn ` X ) /\ F ( ~~> t ` J ) P ) -> F C_ ( CC X. X ) )
Theorem	lmcl 15483	Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- ( ( J e. (TopOn ` X ) /\ F ( ~~> t ` J ) P ) -> P e. X )
Theorem	lmss 15484	Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
|- K = ( J ↾t Y )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> Y e. V )   &    |- ( ph -> J e. Top )   &    |- ( ph -> P e. Y )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> Y )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> F ( ~~> t ` K ) P ) )
Theorem	sslm 15485	A finer topology has fewer convergent sequences (but the sequences that do converge, converge to the same value). (Contributed by Mario Carneiro, 15-Sep-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) /\ J C_ K ) -> ( ~~> t ` K ) C_ ( ~~> t ` J ) )
Theorem	lmres 15486	A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( X ^pm CC ) )   &    |- ( ph -> M e. ZZ )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F |` ( ZZ>= ` M ) ) ( ~~> t ` J ) P ) )
Theorem	lmff 15487*	If F converges, there is some upper integer set on which F is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. dom ( ~~> t ` J ) )   =>    |- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )
Theorem	lmtopcnp 15488	The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) (Revised by Jim Kingdon, 6-Apr-2023.)
|- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> K e. Top )   &    |- ( ph -> G e. ( ( J CnP K ) ` P ) )   =>    |- ( ph -> ( G o. F ) ( ~~> t ` K ) ( G ` P ) )
Theorem	lmcn 15489	The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.)
|- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> G e. ( J Cn K ) )   =>    |- ( ph -> ( G o. F ) ( ~~> t ` K ) ( G ` P ) )
9.1.8  Product topologies
Syntax	ctx 15490	Extend class notation with the binary topological product operation.
class tX
Definition	df-tx 15491*	Define the binary topological product, which is homeomorphic to the general topological product over a two element set, but is more convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
Theorem	txvalex 15492	Existence of the binary topological product. If R and S are known to be topologies, see txtop 15498. (Contributed by Jim Kingdon, 3-Aug-2023.)
|- ( ( R e. V /\ S e. W ) -> ( R tX S ) e. _V )
Theorem	txval 15493*	Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   =>    |- ( ( R e. V /\ S e. W ) -> ( R tX S ) = ( topGen ` B ) )
Theorem	txuni2 15494*	The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   &    |- X = U. R   &    |- Y = U. S   =>    |- ( X X. Y ) = U. B
Theorem	txbasex 15495*	The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   =>    |- ( ( R e. V /\ S e. W ) -> B e. _V )
Theorem	txbas 15496*	The set of Cartesian products of elements from two topological bases is a basis. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   =>    |- ( ( R e. TopBases /\ S e. TopBases ) -> B e. TopBases )
Theorem	eltx 15497*	A set in a product is open iff each point is surrounded by an open rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( ( J e. V /\ K e. W ) -> ( S e. ( J tX K ) <-> A. p e. S E. x e. J E. y e. K ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) ) )
Theorem	txtop 15498	The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
Theorem	txtopi 15499	The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- R e. Top   &    |- S e. Top   =>    |- ( R tX S ) e. Top
Theorem	txtopon 15500	The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro, 2-Sep-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( R tX S ) e. (TopOn ` ( X X. Y ) ) )