Theorem List for Intuitionistic Logic Explorer - 12201-12300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | lmcn 12201 |
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.)
|
                             |
|
6.1.8 Product topologies
|
|
Syntax | ctx 12202 |
Extend class notation with the binary topological product operation.
|
 |
|
Definition | df-tx 12203* |
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 12204 |
Existence of the binary topological product. If and are
known to be topologies, see txtop 12210. (Contributed by Jim Kingdon,
3-Aug-2023.)
|
    
  |
|
Theorem | txval 12205* |
Value of the binary topological product operation. (Contributed by Jeff
Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
|


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


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


        |
|
Theorem | txbas 12208* |
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 12209* |
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 12210 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
    
  |
|
Theorem | txtopi 12211 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 15-Jun-2010.)
|
 
 |
|
Theorem | txtopon 12212 |
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 12213 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
      
     |
|
Theorem | txunii 12214 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 15-Jun-2010.)
|
   
    |
|
Theorem | txopn 12215 |
The product of two open sets is open in the product topology.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
    
 
      |
|
Theorem | txss12 12216 |
Subset property of the topological product. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
       
     |
|
Theorem | txbasval 12217 |
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 12218 |
The Cartesian product of two neighborhoods is a neighborhood in the
product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|
    
                     
         
    |
|
Theorem | tx1cn 12219 |
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 12220 |
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 12221* |
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 12222* |
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 12223* |
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 12224* |
Universal property of the binary topological product. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
       
    
          
     |
|
Theorem | txcn 12225 |
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 12226 |
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 12227 |
The topological product of discrete spaces is discrete. (Contributed by
Mario Carneiro, 14-Aug-2015.)
|
            |
|
Theorem | txdis1cn 12228* |
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 12229* |
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 12230* |
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               
                                                   |
|
6.1.9 Continuous function-builders
|
|
Theorem | cnmptid 12231* |
The identity function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    
     |
|
Theorem | cnmptc 12232* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    TopOn      
     |
|
Theorem | cnmpt11 12233* |
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 12234* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
        
          |
|
Theorem | cnmpt1t 12235* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
           
          |
|
Theorem | cnmpt12f 12236* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
                           |
|
Theorem | cnmpt12 12237* |
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 12238* |
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 12239* |
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 12240* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    TopOn    TopOn      

       |
|
Theorem | cnmpt21 12241* |
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 12242* |
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 12243* |
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 12244* |
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 12245* |
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 12246* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 5-Jun-2014.)
|
 ↾t   TopOn            
     |
|
Theorem | cnmpt2res 12247* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
 ↾t   TopOn     
↾t   TopOn           
   

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

        
       |
|
Theorem | imasnopn 12249 |
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.)
|
       
 
        |
|
6.2 Metric spaces
|
|
6.2.1 Pseudometric spaces
|
|
Theorem | psmetrel 12250 |
The class of pseudometrics is a relation. (Contributed by Jim Kingdon,
24-Apr-2023.)
|
PsMet |
|
Theorem | ispsmet 12251* |
Express the predicate " is a pseudometric." (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
  PsMet        
                              |
|
Theorem | psmetdmdm 12252 |
Recover the base set from a pseudometric. (Contributed by Thierry
Arnoux, 7-Feb-2018.)
|
 PsMet 
  |
|
Theorem | psmetf 12253 |
The distance function of a pseudometric as a function. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
 PsMet          |
|
Theorem | psmetcl 12254 |
Closure of the distance function of a pseudometric space. (Contributed
by Thierry Arnoux, 7-Feb-2018.)
|
  PsMet 
    
  |
|
Theorem | psmet0 12255 |
The distance function of a pseudometric space is zero if its arguments
are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|
  PsMet 
    
  |
|
Theorem | psmettri2 12256 |
Triangle inequality for the distance function of a pseudometric.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
  PsMet  
 
                   |
|
Theorem | psmetsym 12257 |
The distance function of a pseudometric is symmetrical. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
  PsMet 
    
      |
|
Theorem | psmettri 12258 |
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
  PsMet  
 
                   |
|
Theorem | psmetge0 12259 |
The distance function of a pseudometric space is nonnegative.
(Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon,
19-Apr-2023.)
|
  PsMet 

      |
|
Theorem | psmetxrge0 12260 |
The distance function of a pseudometric space is a function into the
nonnegative extended real numbers. (Contributed by Thierry Arnoux,
24-Feb-2018.)
|
 PsMet             |
|
Theorem | psmetres2 12261 |
Restriction of a pseudometric. (Contributed by Thierry Arnoux,
11-Feb-2018.)
|
  PsMet   
   PsMet    |
|
Theorem | psmetlecl 12262 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|
  PsMet  
     
 
      |
|
Theorem | distspace 12263 |
A set together with a
(distance) function
which is a
pseudometric is a distance space (according to E. Deza, M.M. Deza:
"Dictionary of Distances", Elsevier, 2006), i.e. a (base) set
equipped with a distance , which is a mapping of two elements of
the base set to the (extended) reals and which is nonnegative, symmetric
and equal to 0 if the two elements are equal. (Contributed by AV,
15-Oct-2021.) (Revised by AV, 5-Jul-2022.)
|
  PsMet 
        
             
        |
|
6.2.2 Basic metric space
properties
|
|
Syntax | cxms 12264 |
Extend class notation with the class of extended metric spaces.
|
  |
|
Syntax | cms 12265 |
Extend class notation with the class of metric spaces.
|
 |
|
Syntax | ctms 12266 |
Extend class notation with the function mapping a metric to the metric
space it defines.
|
toMetSp |
|
Definition | df-xms 12267 |
Define the (proper) class of extended metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
     
                      |
|
Definition | df-ms 12268 |
Define the (proper) class of metric spaces. (Contributed by NM,
27-Aug-2006.)
|
 
         
                |
|
Definition | df-tms 12269 |
Define the function mapping a metric to the metric space which it defines.
(Contributed by Mario Carneiro, 2-Sep-2015.)
|
toMetSp                      sSet
 TopSet  
        |
|
Theorem | metrel 12270 |
The class of metrics is a relation. (Contributed by Jim Kingdon,
20-Apr-2023.)
|
 |
|
Theorem | xmetrel 12271 |
The class of extended metrics is a relation. (Contributed by Jim
Kingdon, 20-Apr-2023.)
|
  |
|
Theorem | ismet 12272* |
Express the predicate " is a metric." (Contributed by NM,
25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
                    

                    |
|
Theorem | isxmet 12273* |
Express the predicate " is an extended metric." (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
              
      

                       |
|
Theorem | ismeti 12274* |
Properties that determine a metric. (Contributed by NM, 17-Nov-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
       
     
                         |
|
Theorem | isxmetd 12275* |
Properties that determine an extended metric. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
           
            
 
                          |
|
Theorem | isxmet2d 12276* |
It is safe to only require the triangle inequality when the values are
real (so that we can use the standard addition over the reals), but in
this case the nonnegativity constraint cannot be deduced and must be
provided separately. (Counterexample:
        
satisfies all hypotheses
except nonnegativity.) (Contributed by Mario Carneiro,
20-Aug-2015.)
|
           
  
       
 
         
     
                             |
|
Theorem | metflem 12277* |
Lemma for metf 12279 and others. (Contributed by NM,
30-Aug-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
             
                          |
|
Theorem | xmetf 12278 |
Mapping of the distance function of an extended metric. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
              |
|
Theorem | metf 12279 |
Mapping of the distance function of a metric space. (Contributed by NM,
30-Aug-2006.)
|
             |
|
Theorem | xmetcl 12280 |
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30-Aug-2006.)
|
           
  |
|
Theorem | metcl 12281 |
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30-Aug-2006.)
|
     
    
  |
|
Theorem | ismet2 12282 |
An extended metric is a metric exactly when it takes real values for all
values of the arguments. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
                    |
|
Theorem | metxmet 12283 |
A metric is an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
    
       |
|
Theorem | xmetdmdm 12284 |
Recover the base set from an extended metric. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
        |
|
Theorem | metdmdm 12285 |
Recover the base set from a metric. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
    
  |
|
Theorem | xmetunirn 12286 |
Two ways to express an extended metric on an unspecified base.
(Contributed by Mario Carneiro, 13-Oct-2015.)
|
  
       |
|
Theorem | xmeteq0 12287 |
The value of an extended metric is zero iff its arguments are equal.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
            
   |
|
Theorem | meteq0 12288 |
The value of a metric is zero iff its arguments are equal. Property M2
of [Kreyszig] p. 4. (Contributed by
NM, 30-Aug-2006.)
|
     
     
   |
|
Theorem | xmettri2 12289 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
         
                   |
|
Theorem | mettri2 12290 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro,
20-Aug-2015.)
|
      
 
        
       |
|
Theorem | xmet0 12291 |
The distance function of a metric space is zero if its arguments are
equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
           
  |
|
Theorem | met0 12292 |
The distance function of a metric space is zero if its arguments are
equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by NM,
30-Aug-2006.)
|
          
  |
|
Theorem | xmetge0 12293 |
The distance function of a metric space is nonnegative. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
       
      |
|
Theorem | metge0 12294 |
The distance function of a metric space is nonnegative. (Contributed by
NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
     

      |
|
Theorem | xmetlecl 12295 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
             
 
      |
|
Theorem | xmetsym 12296 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
           
      |
|
Theorem | xmetpsmet 12297 |
An extended metric is a pseudometric. (Contributed by Thierry Arnoux,
7-Feb-2018.)
|
      PsMet    |
|
Theorem | xmettpos 12298 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
      tpos   |
|
Theorem | metsym 12299 |
The distance function of a metric space is symmetric. Definition
14-1.1(c) of [Gleason] p. 223.
(Contributed by NM, 27-Aug-2006.)
(Revised by Mario Carneiro, 20-Aug-2015.)
|
     
    
      |
|
Theorem | xmettri 12300 |
Triangle inequality for the distance function of a metric space.
Definition 14-1.1(d) of [Gleason] p.
223. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
         
                   |