Theorem List for Intuitionistic Logic Explorer - 13601-13700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | tgcn 13601* |
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 13602* |
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 13603 |
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 13604* |
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 13605 |
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 13606* |
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 13583.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
 TopOn             
   
 
          |
|
Theorem | lmbr2 13607* |
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 13608* |
Express the binary relation "sequence converges to point
" in a
metric space using an arbitrary upper set of integers.
This version of lmbr2 13607 presupposes that is a function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
 TopOn                       
                       |
|
Theorem | lmconst 13609 |
A constant sequence converges to its value. (Contributed by NM,
8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
      TopOn 
              |
|
Theorem | lmcvg 13610* |
Convergence property of a converging sequence. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
                     
           |
|
Theorem | iscnp4 13611* |
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 13612* |
A condition for continuity at a point in terms of neighborhoods.
(Contributed by Jeff Hankins, 7-Sep-2009.)
|
    
             
                                 |
|
Theorem | cnima 13613 |
An open subset of the codomain of a continuous function has an open
preimage. (Contributed by FL, 15-Dec-2006.)
|
  
         |
|
Theorem | cnco 13614 |
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 13615 |
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 13616 |
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 13617 |
Property of the preimage of an interior. (Contributed by Mario
Carneiro, 25-Aug-2015.)
|
                                  |
|
Theorem | cnntr 13618* |
Continuity in terms of interior. (Contributed by Jeff Hankins,
2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
  TopOn 
TopOn  
  
                                     |
|
Theorem | cnss1 13619 |
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 13620 |
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 13621 |
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 13622 |
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 13623* |
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 13624* |
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 13625* |
Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux,
3-Jan-2018.)
|
                             
              
   |
|
Theorem | cnconst2 13626 |
A constant function is continuous. (Contributed by Mario Carneiro,
19-Mar-2015.)
|
  TopOn 
TopOn           |
|
Theorem | cnconst 13627 |
A constant function is continuous. (Contributed by FL, 15-Jan-2007.)
(Proof shortened by Mario Carneiro, 19-Mar-2015.)
|
   TopOn  TopOn   
       
    |
|
Theorem | cnrest 13628 |
Continuity of a restriction from a subspace. (Contributed by Jeff
Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
|
      
   ↾t     |
|
Theorem | cnrest2 13629 |
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 13630 |
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 13631 |
One direction of cnptoprest 13632 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 13632 |
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 13633 |
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 13634 |
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 13635 |
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 13636 |
If converges, then
is a partial
function. (Contributed by
Mario Carneiro, 23-Dec-2013.)
|
  TopOn              |
|
Theorem | lmfss 13637 |
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 13638 |
Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by
Mario Carneiro, 23-Dec-2013.)
|
  TopOn            |
|
Theorem | lmss 13639 |
Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by
Mario Carneiro, 30-Dec-2013.)
|
 ↾t                                       |
|
Theorem | sslm 13640 |
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 13641 |
A function converges iff its restriction to an upper integers set
converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
 TopOn                                  |
|
Theorem | lmff 13642* |
If converges, there
is some upper integer set on which is
a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
     TopOn                              |
|
Theorem | lmtopcnp 13643 |
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 13644 |
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 13645 |
Extend class notation with the binary topological product operation.
|
 |
|
Definition | df-tx 13646* |
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 13647 |
Existence of the binary topological product. If and are
known to be topologies, see txtop 13653. (Contributed by Jim Kingdon,
3-Aug-2023.)
|
    
  |
|
Theorem | txval 13648* |
Value of the binary topological product operation. (Contributed by Jeff
Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
|


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


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


        |
|
Theorem | txbas 13651* |
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 13652* |
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 13653 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
    
  |
|
Theorem | txtopi 13654 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 15-Jun-2010.)
|
 
 |
|
Theorem | txtopon 13655 |
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 13656 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
      
     |
|
Theorem | txunii 13657 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 15-Jun-2010.)
|
   
    |
|
Theorem | txopn 13658 |
The product of two open sets is open in the product topology.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
    
 
      |
|
Theorem | txss12 13659 |
Subset property of the topological product. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
       
     |
|
Theorem | txbasval 13660 |
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 13661 |
The Cartesian product of two neighborhoods is a neighborhood in the
product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|
    
                     
         
    |
|
Theorem | tx1cn 13662 |
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 13663 |
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 13664* |
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 13665* |
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 13666* |
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 13667* |
Universal property of the binary topological product. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
       
    
          
     |
|
Theorem | txcn 13668 |
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 13669 |
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 13670 |
The topological product of discrete spaces is discrete. (Contributed by
Mario Carneiro, 14-Aug-2015.)
|
            |
|
Theorem | txdis1cn 13671* |
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 13672* |
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 13673* |
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 13674* |
The identity function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    
     |
|
Theorem | cnmptc 13675* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    TopOn      
     |
|
Theorem | cnmpt11 13676* |
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 13677* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
        
          |
|
Theorem | cnmpt1t 13678* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
           
          |
|
Theorem | cnmpt12f 13679* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
                           |
|
Theorem | cnmpt12 13680* |
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 13681* |
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 13682* |
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 13683* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    TopOn    TopOn      

       |
|
Theorem | cnmpt21 13684* |
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 13685* |
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 13686* |
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 13687* |
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 13688* |
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 13689* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 5-Jun-2014.)
|
 ↾t   TopOn            
     |
|
Theorem | cnmpt2res 13690* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
 ↾t   TopOn     
↾t   TopOn           
   

       |
|
Theorem | cnmptcom 13691* |
The argument converse of a continuous function is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
 TopOn    TopOn    

        
       |
|
Theorem | imasnopn 13692 |
If a relation graph is open, then an image set of a singleton is also
open. Corollary of Proposition 4 of [BourbakiTop1] p. I.26.
(Contributed by Thierry Arnoux, 14-Jan-2018.)
|
       
 
        |
|
8.1.10 Homeomorphisms
|
|
Syntax | chmeo 13693 |
Extend class notation with the class of all homeomorphisms.
|
 |
|
Definition | df-hmeo 13694* |
Function returning all the homeomorphisms from topology to
topology .
(Contributed by FL, 14-Feb-2007.)
|
   
 

    |
|
Theorem | hmeofn 13695 |
The set of homeomorphisms is a function on topologies. (Contributed by
Mario Carneiro, 23-Aug-2015.)
|
   |
|
Theorem | hmeofvalg 13696* |
The set of all the homeomorphisms between two topologies. (Contributed
by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
         
      |
|
Theorem | ishmeo 13697 |
The predicate F is a homeomorphism between topology and topology
. Proposition
of [BourbakiTop1] p. I.2. (Contributed
by FL,
14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
      
 
     |
|
Theorem | hmeocn 13698 |
A homeomorphism is continuous. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
    
    |
|
Theorem | hmeocnvcn 13699 |
The converse of a homeomorphism is continuous. (Contributed by Mario
Carneiro, 22-Aug-2015.)
|
     
    |
|
Theorem | hmeocnv 13700 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
     
      |