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

        
       |
|
Theorem | imasnopn 13802 |
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 13803 |
Extend class notation with the class of all homeomorphisms.
|
 |
|
Definition | df-hmeo 13804* |
Function returning all the homeomorphisms from topology to
topology .
(Contributed by FL, 14-Feb-2007.)
|
   
 

    |
|
Theorem | hmeofn 13805 |
The set of homeomorphisms is a function on topologies. (Contributed by
Mario Carneiro, 23-Aug-2015.)
|
   |
|
Theorem | hmeofvalg 13806* |
The set of all the homeomorphisms between two topologies. (Contributed
by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
         
      |
|
Theorem | ishmeo 13807 |
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 13808 |
A homeomorphism is continuous. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
    
    |
|
Theorem | hmeocnvcn 13809 |
The converse of a homeomorphism is continuous. (Contributed by Mario
Carneiro, 22-Aug-2015.)
|
     
    |
|
Theorem | hmeocnv 13810 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
     
      |
|
Theorem | hmeof1o2 13811 |
A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
  TopOn 
TopOn             |
|
Theorem | hmeof1o 13812 |
A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.)
(Revised by Mario Carneiro, 30-May-2014.)
|
             |
|
Theorem | hmeoima 13813 |
The image of an open set by a homeomorphism is an open set. (Contributed
by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
     
    
  |
|
Theorem | hmeoopn 13814 |
Homeomorphisms preserve openness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
        
       |
|
Theorem | hmeocld 13815 |
Homeomorphisms preserve closedness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
        
       
       |
|
Theorem | hmeontr 13816 |
Homeomorphisms preserve interiors. (Contributed by Mario Carneiro,
25-Aug-2015.)
|
                                  |
|
Theorem | hmeoimaf1o 13817* |
The function mapping open sets to their images under a homeomorphism is
a bijection of topologies. (Contributed by Mario Carneiro,
10-Sep-2015.)
|
      
          |
|
Theorem | hmeores 13818 |
The restriction of a homeomorphism is a homeomorphism. (Contributed by
Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
        
   ↾t     ↾t         |
|
Theorem | hmeoco 13819 |
The composite of two homeomorphisms is a homeomorphism. (Contributed by
FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
     
     

      |
|
Theorem | idhmeo 13820 |
The identity function is a homeomorphism. (Contributed by FL,
14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
 TopOn         |
|
Theorem | hmeocnvb 13821 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
  
   
       |
|
Theorem | txhmeo 13822* |
Lift a pair of homeomorphisms on the factors to a homeomorphism of
product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)
|
               

                      |
|
Theorem | txswaphmeolem 13823* |
Show inverse for the "swap components" operation on a Cartesian
product.
(Contributed by Mario Carneiro, 21-Mar-2015.)
|
             
    |
|
Theorem | txswaphmeo 13824* |
There is a homeomorphism from to . (Contributed
by Mario Carneiro, 21-Mar-2015.)
|
  TopOn 
TopOn  
       
        |
|
8.2 Metric spaces
|
|
8.2.1 Pseudometric spaces
|
|
Theorem | psmetrel 13825 |
The class of pseudometrics is a relation. (Contributed by Jim Kingdon,
24-Apr-2023.)
|
PsMet |
|
Theorem | ispsmet 13826* |
Express the predicate " is a pseudometric". (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
  PsMet        
                              |
|
Theorem | psmetdmdm 13827 |
Recover the base set from a pseudometric. (Contributed by Thierry
Arnoux, 7-Feb-2018.)
|
 PsMet 
  |
|
Theorem | psmetf 13828 |
The distance function of a pseudometric as a function. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
 PsMet          |
|
Theorem | psmetcl 13829 |
Closure of the distance function of a pseudometric space. (Contributed
by Thierry Arnoux, 7-Feb-2018.)
|
  PsMet 
    
  |
|
Theorem | psmet0 13830 |
The distance function of a pseudometric space is zero if its arguments
are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|
  PsMet 
    
  |
|
Theorem | psmettri2 13831 |
Triangle inequality for the distance function of a pseudometric.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
  PsMet  
 
                   |
|
Theorem | psmetsym 13832 |
The distance function of a pseudometric is symmetrical. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
  PsMet 
    
      |
|
Theorem | psmettri 13833 |
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
  PsMet  
 
                   |
|
Theorem | psmetge0 13834 |
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 13835 |
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 13836 |
Restriction of a pseudometric. (Contributed by Thierry Arnoux,
11-Feb-2018.)
|
  PsMet   
   PsMet    |
|
Theorem | psmetlecl 13837 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|
  PsMet  
     
 
      |
|
Theorem | distspace 13838 |
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 
        
             
        |
|
8.2.2 Basic metric space
properties
|
|
Syntax | cxms 13839 |
Extend class notation with the class of extended metric spaces.
|
  |
|
Syntax | cms 13840 |
Extend class notation with the class of metric spaces.
|
 |
|
Syntax | ctms 13841 |
Extend class notation with the function mapping a metric to the metric
space it defines.
|
toMetSp |
|
Definition | df-xms 13842 |
Define the (proper) class of extended metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
     
                      |
|
Definition | df-ms 13843 |
Define the (proper) class of metric spaces. (Contributed by NM,
27-Aug-2006.)
|
 
         
                |
|
Definition | df-tms 13844 |
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 13845 |
The class of metrics is a relation. (Contributed by Jim Kingdon,
20-Apr-2023.)
|
 |
|
Theorem | xmetrel 13846 |
The class of extended metrics is a relation. (Contributed by Jim
Kingdon, 20-Apr-2023.)
|
  |
|
Theorem | ismet 13847* |
Express the predicate " is a metric". (Contributed by NM,
25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
                    

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

                       |
|
Theorem | ismeti 13849* |
Properties that determine a metric. (Contributed by NM, 17-Nov-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
       
     
                         |
|
Theorem | isxmetd 13850* |
Properties that determine an extended metric. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
           
            
 
                          |
|
Theorem | isxmet2d 13851* |
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 13852* |
Lemma for metf 13854 and others. (Contributed by NM,
30-Aug-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
             
                          |
|
Theorem | xmetf 13853 |
Mapping of the distance function of an extended metric. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
              |
|
Theorem | metf 13854 |
Mapping of the distance function of a metric space. (Contributed by NM,
30-Aug-2006.)
|
             |
|
Theorem | xmetcl 13855 |
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 13856 |
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 13857 |
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 13858 |
A metric is an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
    
       |
|
Theorem | xmetdmdm 13859 |
Recover the base set from an extended metric. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
        |
|
Theorem | metdmdm 13860 |
Recover the base set from a metric. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
    
  |
|
Theorem | xmetunirn 13861 |
Two ways to express an extended metric on an unspecified base.
(Contributed by Mario Carneiro, 13-Oct-2015.)
|
  
       |
|
Theorem | xmeteq0 13862 |
The value of an extended metric is zero iff its arguments are equal.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
            
   |
|
Theorem | meteq0 13863 |
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 13864 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
         
                   |
|
Theorem | mettri2 13865 |
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 13866 |
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 13867 |
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 13868 |
The distance function of a metric space is nonnegative. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
       
      |
|
Theorem | metge0 13869 |
The distance function of a metric space is nonnegative. (Contributed by
NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
     

      |
|
Theorem | xmetlecl 13870 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
             
 
      |
|
Theorem | xmetsym 13871 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
           
      |
|
Theorem | xmetpsmet 13872 |
An extended metric is a pseudometric. (Contributed by Thierry Arnoux,
7-Feb-2018.)
|
      PsMet    |
|
Theorem | xmettpos 13873 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
      tpos   |
|
Theorem | metsym 13874 |
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 13875 |
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.)
|
         
                   |
|
Theorem | mettri 13876 |
Triangle inequality for the distance function of a metric space.
Definition 14-1.1(d) of [Gleason] p.
223. (Contributed by NM,
27-Aug-2006.)
|
      
 
        
       |
|
Theorem | xmettri3 13877 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
         
                   |
|
Theorem | mettri3 13878 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 13-Mar-2007.)
|
      
 
        
       |
|
Theorem | xmetrtri 13879 |
One half of the reverse triangle inequality for the distance function of
an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
         
             
      |
|
Theorem | metrtri 13880 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon,
21-Apr-2023.)
|
      
 
       
     
      |
|
Theorem | metn0 13881 |
A metric space is nonempty iff its base set is nonempty. (Contributed
by NM, 4-Oct-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
     
   |
|
Theorem | xmetres2 13882 |
Restriction of an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
                   |
|
Theorem | metreslem 13883 |
Lemma for metres 13886. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
 
               |
|
Theorem | metres2 13884 |
Lemma for metres 13886. (Contributed by FL, 12-Oct-2006.) (Proof
shortened by Mario Carneiro, 14-Aug-2015.)
|
     
           |
|
Theorem | xmetres 13885 |
A restriction of an extended metric is an extended metric. (Contributed
by Mario Carneiro, 24-Aug-2015.)
|
                   |
|
Theorem | metres 13886 |
A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
     
           |
|
Theorem | 0met 13887 |
The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario
Carneiro, 14-Aug-2015.)
|
     |
|
8.2.3 Metric space balls
|
|
Theorem | blfvalps 13888* |
The value of the ball function. (Contributed by NM, 30-Aug-2006.)
(Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux,
11-Feb-2018.)
|
 PsMet       
         |
|
Theorem | blfval 13889* |
The value of the ball function. (Contributed by NM, 30-Aug-2006.)
(Revised by Mario Carneiro, 11-Nov-2013.) (Proof shortened by Thierry
Arnoux, 11-Feb-2018.)
|
           
         |
|
Theorem | blex 13890 |
A ball is a set. (Contributed by Jim Kingdon, 4-May-2023.)
|
            |
|
Theorem | blvalps 13891* |
The ball around a point is the set of all points whose distance
from is less
than the ball's radius . (Contributed by NM,
31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
  PsMet 
         
       |
|
Theorem | blval 13892* |
The ball around a point is the set of all points whose distance
from is less
than the ball's radius . (Contributed by NM,
31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|
                        |
|
Theorem | elblps 13893 |
Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by
Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux,
11-Mar-2018.)
|
  PsMet 
 
            
    |
|
Theorem | elbl 13894 |
Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by
Mario Carneiro, 11-Nov-2013.)
|
                     
    |
|
Theorem | elbl2ps 13895 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
   PsMet     
            
   |
|
Theorem | elbl2 13896 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.)
|
         
 
                |
|
Theorem | elbl3ps 13897 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
   PsMet     
            
   |
|
Theorem | elbl3 13898 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
         
 
                |
|
Theorem | blcomps 13899 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
   PsMet     
        
           |
|
Theorem | blcom 13900 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.)
|
         
 
        
           |