Type | Label | Description |
Statement |
|
Theorem | psmettri 14101 |
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
  PsMet  
 
                   |
|
Theorem | psmetge0 14102 |
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 14103 |
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 14104 |
Restriction of a pseudometric. (Contributed by Thierry Arnoux,
11-Feb-2018.)
|
  PsMet   
   PsMet    |
|
Theorem | psmetlecl 14105 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|
  PsMet  
     
 
      |
|
Theorem | distspace 14106 |
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 14107 |
Extend class notation with the class of extended metric spaces.
|
  |
|
Syntax | cms 14108 |
Extend class notation with the class of metric spaces.
|
 |
|
Syntax | ctms 14109 |
Extend class notation with the function mapping a metric to the metric
space it defines.
|
toMetSp |
|
Definition | df-xms 14110 |
Define the (proper) class of extended metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
     
                      |
|
Definition | df-ms 14111 |
Define the (proper) class of metric spaces. (Contributed by NM,
27-Aug-2006.)
|
 
         
                |
|
Definition | df-tms 14112 |
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 14113 |
The class of metrics is a relation. (Contributed by Jim Kingdon,
20-Apr-2023.)
|
 |
|
Theorem | xmetrel 14114 |
The class of extended metrics is a relation. (Contributed by Jim
Kingdon, 20-Apr-2023.)
|
  |
|
Theorem | ismet 14115* |
Express the predicate " is a metric". (Contributed by NM,
25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
                    

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

                       |
|
Theorem | ismeti 14117* |
Properties that determine a metric. (Contributed by NM, 17-Nov-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
       
     
                         |
|
Theorem | isxmetd 14118* |
Properties that determine an extended metric. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
           
            
 
                          |
|
Theorem | isxmet2d 14119* |
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 14120* |
Lemma for metf 14122 and others. (Contributed by NM,
30-Aug-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
             
                          |
|
Theorem | xmetf 14121 |
Mapping of the distance function of an extended metric. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
              |
|
Theorem | metf 14122 |
Mapping of the distance function of a metric space. (Contributed by NM,
30-Aug-2006.)
|
             |
|
Theorem | xmetcl 14123 |
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 14124 |
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 14125 |
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 14126 |
A metric is an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
    
       |
|
Theorem | xmetdmdm 14127 |
Recover the base set from an extended metric. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
        |
|
Theorem | metdmdm 14128 |
Recover the base set from a metric. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
    
  |
|
Theorem | xmetunirn 14129 |
Two ways to express an extended metric on an unspecified base.
(Contributed by Mario Carneiro, 13-Oct-2015.)
|
  
       |
|
Theorem | xmeteq0 14130 |
The value of an extended metric is zero iff its arguments are equal.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
            
   |
|
Theorem | meteq0 14131 |
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 14132 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
         
                   |
|
Theorem | mettri2 14133 |
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 14134 |
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 14135 |
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 14136 |
The distance function of a metric space is nonnegative. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
       
      |
|
Theorem | metge0 14137 |
The distance function of a metric space is nonnegative. (Contributed by
NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
     

      |
|
Theorem | xmetlecl 14138 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
             
 
      |
|
Theorem | xmetsym 14139 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
           
      |
|
Theorem | xmetpsmet 14140 |
An extended metric is a pseudometric. (Contributed by Thierry Arnoux,
7-Feb-2018.)
|
      PsMet    |
|
Theorem | xmettpos 14141 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
      tpos   |
|
Theorem | metsym 14142 |
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 14143 |
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 14144 |
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 14145 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
         
                   |
|
Theorem | mettri3 14146 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 13-Mar-2007.)
|
      
 
        
       |
|
Theorem | xmetrtri 14147 |
One half of the reverse triangle inequality for the distance function of
an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
         
             
      |
|
Theorem | metrtri 14148 |
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 14149 |
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 14150 |
Restriction of an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
                   |
|
Theorem | metreslem 14151 |
Lemma for metres 14154. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
 
               |
|
Theorem | metres2 14152 |
Lemma for metres 14154. (Contributed by FL, 12-Oct-2006.) (Proof
shortened by Mario Carneiro, 14-Aug-2015.)
|
     
           |
|
Theorem | xmetres 14153 |
A restriction of an extended metric is an extended metric. (Contributed
by Mario Carneiro, 24-Aug-2015.)
|
                   |
|
Theorem | metres 14154 |
A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
     
           |
|
Theorem | 0met 14155 |
The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario
Carneiro, 14-Aug-2015.)
|
     |
|
8.2.3 Metric space balls
|
|
Theorem | blfvalps 14156* |
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 14157* |
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 14158 |
A ball is a set. (Contributed by Jim Kingdon, 4-May-2023.)
|
            |
|
Theorem | blvalps 14159* |
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 14160* |
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 14161 |
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 14162 |
Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by
Mario Carneiro, 11-Nov-2013.)
|
                     
    |
|
Theorem | elbl2ps 14163 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
   PsMet     
            
   |
|
Theorem | elbl2 14164 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.)
|
         
 
                |
|
Theorem | elbl3ps 14165 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
   PsMet     
            
   |
|
Theorem | elbl3 14166 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
         
 
                |
|
Theorem | blcomps 14167 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
   PsMet     
        
           |
|
Theorem | blcom 14168 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.)
|
         
 
        
           |
|
Theorem | xblpnfps 14169 |
The infinity ball in an extended metric is the set of all points that
are a finite distance from the center. (Contributed by Mario Carneiro,
23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
  PsMet 
             
    |
|
Theorem | xblpnf 14170 |
The infinity ball in an extended metric is the set of all points that
are a finite distance from the center. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
                    
    |
|
Theorem | blpnf 14171 |
The infinity ball in a standard metric is just the whole space.
(Contributed by Mario Carneiro, 23-Aug-2015.)
|
                |
|
Theorem | bldisj 14172 |
Two balls are disjoint if the center-to-center distance is more than the
sum of the radii. (Contributed by Mario Carneiro, 30-Dec-2013.)
|
        

    
     
                    |
|
Theorem | blgt0 14173 |
A nonempty ball implies that the radius is positive. (Contributed by
NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
                 
  |
|
Theorem | bl2in 14174 |
Two balls are disjoint if they don't overlap. (Contributed by NM,
11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
                
                    |
|
Theorem | xblss2ps 14175 |
One ball is contained in another if the center-to-center distance is
less than the difference of the radii. In this version of blss2 14178 for
extended metrics, we have to assume the balls are a finite distance
apart, or else will not even be in the infinity ball around
.
(Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
 PsMet                     
                          |
|
Theorem | xblss2 14176 |
One ball is contained in another if the center-to-center distance is
less than the difference of the radii. In this version of blss2 14178 for
extended metrics, we have to assume the balls are a finite distance
apart, or else will not even be in the infinity ball around
.
(Contributed by Mario Carneiro, 23-Aug-2015.)
|
                         
                          |
|
Theorem | blss2ps 14177 |
One ball is contained in another if the center-to-center distance is
less than the difference of the radii. (Contributed by Mario Carneiro,
15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
   PsMet                              |
|
Theorem | blss2 14178 |
One ball is contained in another if the center-to-center distance is
less than the difference of the radii. (Contributed by Mario Carneiro,
15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
        
     
                     |
|
Theorem | blhalf 14179 |
A ball of radius is contained in a ball of radius centered
at any point inside the smaller ball. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jan-2014.)
|
         
                                |
|
Theorem | blfps 14180 |
Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario
Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
 PsMet               |
|
Theorem | blf 14181 |
Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario
Carneiro, 23-Aug-2015.)
|
                   |
|
Theorem | blrnps 14182* |
Membership in the range of the ball function. Note that
    is the
collection of all balls for metric .
(Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro,
12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
 PsMet  
     
           |
|
Theorem | blrn 14183* |
Membership in the range of the ball function. Note that
    is the
collection of all balls for metric .
(Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
            
           |
|
Theorem | xblcntrps 14184 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux,
11-Mar-2018.)
|
  PsMet 

 
          |
|
Theorem | xblcntr 14185 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
         
          |
|
Theorem | blcntrps 14186 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux,
11-Mar-2018.)
|
  PsMet 

          |
|
Theorem | blcntr 14187 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
                  |
|
Theorem | xblm 14188* |
A ball is inhabited iff the radius is positive. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
                     |
|
Theorem | bln0 14189 |
A ball is not empty. It is also inhabited, as seen at blcntr 14187.
(Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
                  |
|
Theorem | blelrnps 14190 |
A ball belongs to the set of balls of a metric space. (Contributed by
NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
  PsMet 
               |
|
Theorem | blelrn 14191 |
A ball belongs to the set of balls of a metric space. (Contributed by
NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
               
      |
|
Theorem | blssm 14192 |
A ball is a subset of the base set of a metric space. (Contributed by
NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
                  |
|
Theorem | unirnblps 14193 |
The union of the set of balls of a metric space is its base set.
(Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro,
12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
 PsMet         |
|
Theorem | unirnbl 14194 |
The union of the set of balls of a metric space is its base set.
(Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
             |
|
Theorem | blininf 14195 |
The intersection of two balls with the same center is the smaller of
them. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
         
                          inf  
      |
|
Theorem | ssblps 14196 |
The size of a ball increases monotonically with its radius.
(Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro,
24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
   PsMet    
                   |
|
Theorem | ssbl 14197 |
The size of a ball increases monotonically with its radius.
(Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro,
24-Aug-2015.)
|
         
                    |
|
Theorem | blssps 14198* |
Any point in a ball
can be centered in
another ball that is
a subset of .
(Contributed by NM, 31-Aug-2006.) (Revised by
Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux,
11-Mar-2018.)
|
  PsMet 
             
  |
|
Theorem | blss 14199* |
Any point in a ball
can be centered in
another ball that is
a subset of .
(Contributed by NM, 31-Aug-2006.) (Revised by
Mario Carneiro, 24-Aug-2015.)
|
                       |
|
Theorem | blssexps 14200* |
Two ways to express the existence of a ball subset. (Contributed by NM,
5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
  PsMet 
                      |