P. 153 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15201-15300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	restuni2 15201	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 15202	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 15203	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 15204	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 15205	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 15206	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 15207	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 15208	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 15209	Extend class notation with the class of continuous functions between topologies.
class Cn
Syntax	ccnp 15210	Extend class notation with the class of functions between topologies continuous at a given point.
class CnP
Syntax	clm 15211	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 15212*	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 15221 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 15213*	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 15214*	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 15215	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 15216	Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.)
|- ( F ( ~~> t ` J ) P -> J e. Top )
Theorem	lmfval 15217*	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 15218*	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 15219*	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 15220	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 15221*	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 15222*	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 15223*	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 15224*	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 15225	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> J e. Top )
Theorem	cntop2 15226	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> K e. Top )
Theorem	iscnp3 15227*	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 15228	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 15229	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 15230	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 15231	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 15232*	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 15233*	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 15234	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 15235*	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 15236	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 15237*	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 15214. (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 15238*	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 15239*	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 15238 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 15240	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 15241*	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 15242*	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 15243*	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 15244	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 15245	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 15246	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 15247	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 15248	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 15249*	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 15250	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 15251	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 15252	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 15253	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 15254*	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 15255*	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 15256*	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 15257	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 15258	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 15259	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 15260	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 15261	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 15262	One direction of cnptoprest 15263 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 15263	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 15264	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 15265	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 15266	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 15267	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 15268	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 15269	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 15270	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 15271	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 15272	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 15273*	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 15274	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 15275	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 15276	Extend class notation with the binary topological product operation.
class tX
Definition	df-tx 15277*	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 15278	Existence of the binary topological product. If R and S are known to be topologies, see txtop 15284. (Contributed by Jim Kingdon, 3-Aug-2023.)
|- ( ( R e. V /\ S e. W ) -> ( R tX S ) e. _V )
Theorem	txval 15279*	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 15280*	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 15281*	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 15282*	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 15283*	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 15284	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 15285	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 15286	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 ) ) )
Theorem	txuni 15287	The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- X = U. R   &    |- Y = U. S   =>    |- ( ( R e. Top /\ S e. Top ) -> ( X X. Y ) = U. ( R tX S ) )
Theorem	txunii 15288	The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- R e. Top   &    |- S e. Top   &    |- X = U. R   &    |- Y = U. S   =>    |- ( X X. Y ) = U. ( R tX S )
Theorem	txopn 15289	The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( ( R e. V /\ S e. W ) /\ ( A e. R /\ B e. S ) ) -> ( A X. B ) e. ( R tX S ) )
Theorem	txss12 15290	Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( A tX C ) C_ ( B tX D ) )
Theorem	txbasval 15291	It is sufficient to consider products of the bases for the topologies in the topological product. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( R e. V /\ S e. W ) -> ( ( topGen ` R ) tX ( topGen ` S ) ) = ( R tX S ) )
Theorem	neitx 15292	The Cartesian product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) )
Theorem	tx1cn 15293	Continuity of the first projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) )
Theorem	tx2cn 15294	Continuity of the second projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) )
Theorem	txcnp 15295*	If two functions are continuous at D, then the ordered pair of them is continuous at D into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> D e. X )   &    |- ( ph -> ( x e. X |-> A ) e. ( ( J CnP K ) ` D ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( ( J CnP L ) ` D ) )   =>    |- ( ph -> ( x e. X |-> <. A , B >. ) e. ( ( J CnP ( K tX L ) ) ` D ) )
Theorem	upxp 15296*	Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- P = ( 1st |` ( B X. C ) )   &    |- Q = ( 2nd |` ( B X. C ) )   =>    |- ( ( A e. D /\ F : A --> B /\ G : A --> C ) -> E! h ( h : A --> ( B X. C ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) )
Theorem	txcnmpt 15297*	A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- W = U. U   &    |- H = ( x e. W |-> <. ( F ` x ) , ( G ` x ) >. )   =>    |- ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> H e. ( U Cn ( R tX S ) ) )
Theorem	uptx 15298*	Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- T = ( R tX S )   &    |- X = U. R   &    |- Y = U. S   &    |- Z = ( X X. Y )   &    |- P = ( 1st |` Z )   &    |- Q = ( 2nd |` Z )   =>    |- ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> E! h e. ( U Cn T ) ( F = ( P o. h ) /\ G = ( Q o. h ) ) )
Theorem	txcn 15299	A map into the product of two topological spaces is continuous iff both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- X = U. R   &    |- Y = U. S   &    |- Z = ( X X. Y )   &    |- W = U. U   &    |- P = ( 1st |` Z )   &    |- Q = ( 2nd |` Z )   =>    |- ( ( R e. Top /\ S e. Top /\ F : W --> Z ) -> ( F e. ( U Cn ( R tX S ) ) <-> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) )
Theorem	txrest 15300	The subspace of a topological product space induced by a subset with a Cartesian product representation is a topological product of the subspaces induced by the subspaces of the terms of the products. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|- ( ( ( R e. V /\ S e. W ) /\ ( A e. X /\ B e. Y ) ) -> ( ( R tX S ) ↾t ( A X. B ) ) = ( ( R ↾t A ) tX ( S ↾t B ) ) )