Type | Label | Description |
Statement |
|
Theorem | cnpval 13701* |
The set of all functions from topology to topology that are
continuous at a point . (Contributed by NM, 17-Oct-2006.)
(Revised by Mario Carneiro, 11-Nov-2013.)
|
  TopOn 
TopOn        
  
     
     
     |
|
Theorem | iscnp 13702* |
The predicate "the class is a continuous function from topology
to topology
at point ". Based on Theorem
7.2(g) of
[Munkres] p. 107. (Contributed by NM,
17-Oct-2006.) (Revised by Mario
Carneiro, 21-Aug-2015.)
|
  TopOn 
TopOn                    
     
      |
|
Theorem | iscn2 13703* |
The predicate "the class is a continuous function from topology
to topology
". Definition of
continuous function in
[Munkres] p. 102. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
      
                |
|
Theorem | cntop1 13704 |
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
  
  |
|
Theorem | cntop2 13705 |
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
  
  |
|
Theorem | iscnp3 13706* |
The predicate "the class is a continuous function from topology
to topology
at point ". (Contributed by
NM,
15-May-2007.)
|
  TopOn 
TopOn                    
             |
|
Theorem | cnf 13707 |
A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.)
(Revised by Mario Carneiro, 21-Aug-2015.)
|
           |
|
Theorem | cnf2 13708 |
A continuous function is a mapping. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
  TopOn 
TopOn           |
|
Theorem | cnprcl2k 13709 |
Reverse closure for a function continuous at a point. (Contributed by
Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|
  TopOn 
      
  |
|
Theorem | cnpf2 13710 |
A continuous function at point is a mapping. (Contributed by
Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|
  TopOn 
TopOn               |
|
Theorem | tgcn 13711* |
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.)
|
 TopOn          TopOn    
                 |
|
Theorem | tgcnp 13712* |
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.)
|
 TopOn          TopOn      
     
          
     
      |
|
Theorem | ssidcn 13713 |
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.)
|
  TopOn 
TopOn  

  
   |
|
Theorem | icnpimaex 13714* |
Property of a function continuous at a point. (Contributed by FL,
31-Dec-2006.) (Revised by Jim Kingdon, 28-Mar-2023.)
|
   TopOn  TopOn   
     
   
 
     
   |
|
Theorem | idcn 13715 |
A restricted identity function is a continuous function. (Contributed
by FL, 27-Dec-2006.) (Proof shortened by Mario Carneiro,
21-Mar-2015.)
|
 TopOn       |
|
Theorem | lmbr 13716* |
Express the binary relation "sequence converges to point
" in a
topological space. Definition 1.4-1 of [Kreyszig] p. 25.
The condition
  allows us to use objects
more general
than sequences when convenient; see the comment in df-lm 13693.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
 TopOn             
   
 
          |
|
Theorem | lmbr2 13717* |
Express the binary relation "sequence converges to point
" in a
metric space using an arbitrary upper set of integers.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
 TopOn                   
   
      
          |
|
Theorem | lmbrf 13718* |
Express the binary relation "sequence converges to point
" in a
metric space using an arbitrary upper set of integers.
This version of lmbr2 13717 presupposes that is a function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
 TopOn                       
                       |
|
Theorem | lmconst 13719 |
A constant sequence converges to its value. (Contributed by NM,
8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
      TopOn 
              |
|
Theorem | lmcvg 13720* |
Convergence property of a converging sequence. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
                     
           |
|
Theorem | iscnp4 13721* |
The predicate "the class is a continuous function from topology
to topology
at point " in terms of
neighborhoods.
(Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro,
10-Sep-2015.)
|
  TopOn 
TopOn                                              
    |
|
Theorem | cnpnei 13722* |
A condition for continuity at a point in terms of neighborhoods.
(Contributed by Jeff Hankins, 7-Sep-2009.)
|
    
             
                                 |
|
Theorem | cnima 13723 |
An open subset of the codomain of a continuous function has an open
preimage. (Contributed by FL, 15-Dec-2006.)
|
  
         |
|
Theorem | cnco 13724 |
The composition of two continuous functions is a continuous function.
(Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro,
21-Aug-2015.)
|
  
     
    |
|
Theorem | cnptopco 13725 |
The composition of a function continuous at with a function
continuous at     is continuous at . Proposition 2 of
[BourbakiTop1] p. I.9.
(Contributed by FL, 16-Nov-2006.) (Proof
shortened by Mario Carneiro, 27-Dec-2014.)
|
  
       
            

        |
|
Theorem | cnclima 13726 |
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.)
|
  
          
      |
|
Theorem | cnntri 13727 |
Property of the preimage of an interior. (Contributed by Mario
Carneiro, 25-Aug-2015.)
|
                                  |
|
Theorem | cnntr 13728* |
Continuity in terms of interior. (Contributed by Jeff Hankins,
2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
  TopOn 
TopOn  
  
                                     |
|
Theorem | cnss1 13729 |
If the topology is
finer than , then
there are more
continuous functions from than from .
(Contributed by Mario
Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|
   TopOn     
   |
|
Theorem | cnss2 13730 |
If the topology is
finer than , then
there are fewer
continuous functions into than into
from some other space.
(Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario
Carneiro, 21-Aug-2015.)
|
   TopOn     
   |
|
Theorem | cncnpi 13731 |
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.)
|
    
         |
|
Theorem | cnsscnp 13732 |
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.)
|
 
          |
|
Theorem | cncnp 13733* |
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.)
|
  TopOn 
TopOn  
  
                |
|
Theorem | cncnp2m 13734* |
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.)
|
       
 
         |
|
Theorem | cnnei 13735* |
Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux,
3-Jan-2018.)
|
                             
              
   |
|
Theorem | cnconst2 13736 |
A constant function is continuous. (Contributed by Mario Carneiro,
19-Mar-2015.)
|
  TopOn 
TopOn           |
|
Theorem | cnconst 13737 |
A constant function is continuous. (Contributed by FL, 15-Jan-2007.)
(Proof shortened by Mario Carneiro, 19-Mar-2015.)
|
   TopOn  TopOn   
       
    |
|
Theorem | cnrest 13738 |
Continuity of a restriction from a subspace. (Contributed by Jeff
Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
|
      
   ↾t     |
|
Theorem | cnrest2 13739 |
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.)
|
  TopOn 
 
 
  ↾t      |
|
Theorem | cnrest2r 13740 |
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.)
|
 
 ↾t   
   |
|
Theorem | cnptopresti 13741 |
One direction of cnptoprest 13742 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.)
|
   TopOn           
     ↾t        |
|
Theorem | cnptoprest 13742 |
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.)
|
    
                            ↾t         |
|
Theorem | cnptoprest2 13743 |
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.)
|
    
              
   ↾t         |
|
Theorem | cndis 13744 |
Every function is continuous when the domain is discrete. (Contributed
by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro,
21-Aug-2015.)
|
  TopOn     
    |
|
Theorem | cnpdis 13745 |
If is an isolated
point in (or
equivalently, the singleton
  is open in ), then every function is continuous at
. (Contributed
by Mario Carneiro, 9-Sep-2015.)
|
   TopOn  TopOn    
      
    |
|
Theorem | lmfpm 13746 |
If converges, then
is a partial
function. (Contributed by
Mario Carneiro, 23-Dec-2013.)
|
  TopOn              |
|
Theorem | lmfss 13747 |
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.)
|
  TopOn         
    |
|
Theorem | lmcl 13748 |
Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by
Mario Carneiro, 23-Dec-2013.)
|
  TopOn            |
|
Theorem | lmss 13749 |
Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by
Mario Carneiro, 30-Dec-2013.)
|
 ↾t                                       |
|
Theorem | sslm 13750 |
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.)
|
  TopOn 
TopOn       
       |
|
Theorem | lmres 13751 |
A function converges iff its restriction to an upper integers set
converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
 TopOn                                  |
|
Theorem | lmff 13752* |
If converges, there
is some upper integer set on which is
a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
     TopOn                              |
|
Theorem | lmtopcnp 13753 |
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.)
|
                   
               |
|
Theorem | lmcn 13754 |
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.)
|
                             |
|
8.1.8 Product topologies
|
|
Syntax | ctx 13755 |
Extend class notation with the binary topological product operation.
|
 |
|
Definition | df-tx 13756* |
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.)
|
     

      |
|
Theorem | txvalex 13757 |
Existence of the binary topological product. If and are
known to be topologies, see txtop 13763. (Contributed by Jim Kingdon,
3-Aug-2023.)
|
    
  |
|
Theorem | txval 13758* |
Value of the binary topological product operation. (Contributed by Jeff
Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
|


       
      |
|
Theorem | txuni2 13759* |
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 31-Aug-2015.)
|


  
   
  |
|
Theorem | txbasex 13760* |
The basis for the product topology is a set. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|


        |
|
Theorem | txbas 13761* |
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.)
|


     
  |
|
Theorem | eltx 13762* |
A set in a product is open iff each point is surrounded by an open
rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|
    
 



  

    |
|
Theorem | txtop 13763 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
    
  |
|
Theorem | txtopi 13764 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 15-Jun-2010.)
|
 
 |
|
Theorem | txtopon 13765 |
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro,
2-Sep-2015.)
|
  TopOn 
TopOn  
  TopOn      |
|
Theorem | txuni 13766 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
      
     |
|
Theorem | txunii 13767 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 15-Jun-2010.)
|
   
    |
|
Theorem | txopn 13768 |
The product of two open sets is open in the product topology.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
    
 
      |
|
Theorem | txss12 13769 |
Subset property of the topological product. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
       
     |
|
Theorem | txbasval 13770 |
It is sufficient to consider products of the bases for the topologies in
the topological product. (Contributed by Mario Carneiro,
25-Aug-2014.)
|
       
         |
|
Theorem | neitx 13771 |
The Cartesian product of two neighborhoods is a neighborhood in the
product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|
    
                     
         
    |
|
Theorem | tx1cn 13772 |
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.)
|
  TopOn 
TopOn  
   
      |
|
Theorem | tx2cn 13773 |
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.)
|
  TopOn 
TopOn  
   
      |
|
Theorem | txcnp 13774* |
If two functions are continuous at , then the ordered pair of them
is continuous at into the product topology. (Contributed by Mario
Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    TopOn    TopOn               
          
              |
|
Theorem | upxp 13775* |
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.)
|
                                   |
|
Theorem | txcnmpt 13776* |
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.)
|
       
         

 

     |
|
Theorem | uptx 13777* |
Universal property of the binary topological product. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
       
    
          
     |
|
Theorem | txcn 13778 |
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.)
|
   
  
                    
      |
|
Theorem | txrest 13779 |
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.)
|
    
 
   ↾t      ↾t 
 ↾t     |
|
Theorem | txdis 13780 |
The topological product of discrete spaces is discrete. (Contributed by
Mario Carneiro, 14-Aug-2015.)
|
            |
|
Theorem | txdis1cn 13781* |
A function is jointly continuous on a discrete left topology iff it is
continuous as a function of its right argument, for each fixed left
value. (Contributed by Mario Carneiro, 19-Sep-2015.)
|
   TopOn                     
       |
|
Theorem | txlm 13782* |
Two sequences converge iff the sequence of their ordered pairs
converges. Proposition 14-2.6 of [Gleason] p. 230. (Contributed by
NM, 16-Jul-2007.) (Revised by Mario Carneiro, 5-May-2014.)
|
       TopOn    TopOn              
             
                      
         |
|
Theorem | lmcn2 13783* |
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, 15-May-2014.)
|
       TopOn    TopOn               
                                                   |
|
8.1.9 Continuous function-builders
|
|
Theorem | cnmptid 13784* |
The identity function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    
     |
|
Theorem | cnmptc 13785* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    TopOn      
     |
|
Theorem | cnmpt11 13786* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
     TopOn         
  
     |
|
Theorem | cnmpt11f 13787* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
        
          |
|
Theorem | cnmpt1t 13788* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
           
          |
|
Theorem | cnmpt12f 13789* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
                           |
|
Theorem | cnmpt12 13790* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 12-Jun-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
           TopOn    TopOn     
       
   
     |
|
Theorem | cnmpt1st 13791* |
The projection onto the first coordinate is continuous. (Contributed by
Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    TopOn    

       |
|
Theorem | cnmpt2nd 13792* |
The projection onto the second coordinate is continuous. (Contributed
by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    TopOn    

       |
|
Theorem | cnmpt2c 13793* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    TopOn    TopOn      

       |
|
Theorem | cnmpt21 13794* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    TopOn    

       TopOn         
  

       |
|
Theorem | cnmpt21f 13795* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    TopOn    

          
         
   |
|
Theorem | cnmpt2t 13796* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    TopOn    

            
   

            |
|
Theorem | cnmpt22 13797* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    TopOn    

            
   TopOn    TopOn     
       
   

       |
|
Theorem | cnmpt22f 13798* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    TopOn    

            
          
           |
|
Theorem | cnmpt1res 13799* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 5-Jun-2014.)
|
 ↾t   TopOn            
     |
|
Theorem | cnmpt2res 13800* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
 ↾t   TopOn     
↾t   TopOn           
   

       |