Theorem List for Intuitionistic Logic Explorer - 12101-12200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cnconst 12101 |
A constant function is continuous. (Contributed by FL, 15-Jan-2007.)
(Proof shortened by Mario Carneiro, 19-Mar-2015.)
|
   TopOn  TopOn   
       
    |
|
Theorem | cnrest 12102 |
Continuity of a restriction from a subspace. (Contributed by Jeff
Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
|
      
   ↾t     |
|
Theorem | cnrest2 12103 |
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 12104 |
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 12105 |
One direction of cnptoprest 12106 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 12106 |
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 12107 |
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 12108 |
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 12109 |
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 12110 |
If converges, then
is a partial
function. (Contributed by
Mario Carneiro, 23-Dec-2013.)
|
  TopOn              |
|
Theorem | lmfss 12111 |
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 12112 |
Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by
Mario Carneiro, 23-Dec-2013.)
|
  TopOn            |
|
Theorem | lmss 12113 |
Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by
Mario Carneiro, 30-Dec-2013.)
|
 ↾t                                       |
|
Theorem | sslm 12114 |
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 12115 |
A function converges iff its restriction to an upper integers set
converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
 TopOn                                  |
|
Theorem | lmff 12116* |
If converges, there
is some upper integer set on which is
a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
     TopOn                              |
|
Theorem | lmtopcnp 12117 |
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 12118 |
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 Continuous function-builders
|
|
Theorem | cnmptid 12119* |
The identity function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    
     |
|
Theorem | cnmptc 12120* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
 TopOn    TopOn      
     |
|
Theorem | cnmpt11 12121* |
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 12122* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
 TopOn    
        
          |
|
Theorem | cnmpt1res 12123* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 5-Jun-2014.)
|
 ↾t   TopOn            
     |
|
6.2 Metric spaces
|
|
6.2.1 Pseudometric spaces
|
|
Theorem | psmetrel 12124 |
The class of pseudometrics is a relation. (Contributed by Jim Kingdon,
24-Apr-2023.)
|
PsMet |
|
Theorem | ispsmet 12125* |
Express the predicate " is a pseudometric." (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
  PsMet        
                              |
|
Theorem | psmetdmdm 12126 |
Recover the base set from a pseudometric. (Contributed by Thierry
Arnoux, 7-Feb-2018.)
|
 PsMet 
  |
|
Theorem | psmetf 12127 |
The distance function of a pseudometric as a function. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
 PsMet          |
|
Theorem | psmetcl 12128 |
Closure of the distance function of a pseudometric space. (Contributed
by Thierry Arnoux, 7-Feb-2018.)
|
  PsMet 
    
  |
|
Theorem | psmet0 12129 |
The distance function of a pseudometric space is zero if its arguments
are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|
  PsMet 
    
  |
|
Theorem | psmettri2 12130 |
Triangle inequality for the distance function of a pseudometric.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
  PsMet  
 
                   |
|
Theorem | psmetsym 12131 |
The distance function of a pseudometric is symmetrical. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
  PsMet 
    
      |
|
Theorem | psmettri 12132 |
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
  PsMet  
 
                   |
|
Theorem | psmetge0 12133 |
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 12134 |
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 12135 |
Restriction of a pseudometric. (Contributed by Thierry Arnoux,
11-Feb-2018.)
|
  PsMet   
   PsMet    |
|
Theorem | psmetlecl 12136 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|
  PsMet  
     
 
      |
|
Theorem | distspace 12137 |
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 12138 |
Extend class notation with the class of extended metric spaces.
|
  |
|
Syntax | cms 12139 |
Extend class notation with the class of metric spaces.
|
 |
|
Syntax | ctms 12140 |
Extend class notation with the function mapping a metric to the metric
space it defines.
|
toMetSp |
|
Definition | df-xms 12141 |
Define the (proper) class of extended metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
     
                      |
|
Definition | df-ms 12142 |
Define the (proper) class of metric spaces. (Contributed by NM,
27-Aug-2006.)
|
 
         
                |
|
Definition | df-tms 12143 |
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 12144 |
The class of metrics is a relation. (Contributed by Jim Kingdon,
20-Apr-2023.)
|
 |
|
Theorem | xmetrel 12145 |
The class of extended metrics is a relation. (Contributed by Jim
Kingdon, 20-Apr-2023.)
|
  |
|
Theorem | ismet 12146* |
Express the predicate " is a metric." (Contributed by NM,
25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
                    

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

                       |
|
Theorem | ismeti 12148* |
Properties that determine a metric. (Contributed by NM, 17-Nov-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
       
     
                         |
|
Theorem | isxmetd 12149* |
Properties that determine an extended metric. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
           
            
 
                          |
|
Theorem | isxmet2d 12150* |
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 12151* |
Lemma for metf 12153 and others. (Contributed by NM,
30-Aug-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
             
                          |
|
Theorem | xmetf 12152 |
Mapping of the distance function of an extended metric. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
              |
|
Theorem | metf 12153 |
Mapping of the distance function of a metric space. (Contributed by NM,
30-Aug-2006.)
|
             |
|
Theorem | xmetcl 12154 |
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 12155 |
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 12156 |
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 12157 |
A metric is an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
    
       |
|
Theorem | xmetdmdm 12158 |
Recover the base set from an extended metric. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
        |
|
Theorem | metdmdm 12159 |
Recover the base set from a metric. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
    
  |
|
Theorem | xmetunirn 12160 |
Two ways to express an extended metric on an unspecified base.
(Contributed by Mario Carneiro, 13-Oct-2015.)
|
  
       |
|
Theorem | xmeteq0 12161 |
The value of an extended metric is zero iff its arguments are equal.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
            
   |
|
Theorem | meteq0 12162 |
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 12163 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
         
                   |
|
Theorem | mettri2 12164 |
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 12165 |
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 12166 |
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 12167 |
The distance function of a metric space is nonnegative. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
       
      |
|
Theorem | metge0 12168 |
The distance function of a metric space is nonnegative. (Contributed by
NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
     

      |
|
Theorem | xmetlecl 12169 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
             
 
      |
|
Theorem | xmetsym 12170 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
           
      |
|
Theorem | xmetpsmet 12171 |
An extended metric is a pseudometric. (Contributed by Thierry Arnoux,
7-Feb-2018.)
|
      PsMet    |
|
Theorem | xmettpos 12172 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
      tpos   |
|
Theorem | metsym 12173 |
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 12174 |
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 12175 |
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 12176 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
         
                   |
|
Theorem | mettri3 12177 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 13-Mar-2007.)
|
      
 
        
       |
|
Theorem | xmetrtri 12178 |
One half of the reverse triangle inequality for the distance function of
an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
         
             
      |
|
Theorem | metrtri 12179 |
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 12180 |
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 12181 |
Restriction of an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
                   |
|
Theorem | metreslem 12182 |
Lemma for metres 12185. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
 
               |
|
Theorem | metres2 12183 |
Lemma for metres 12185. (Contributed by FL, 12-Oct-2006.) (Proof
shortened by Mario Carneiro, 14-Aug-2015.)
|
     
           |
|
Theorem | xmetres 12184 |
A restriction of an extended metric is an extended metric. (Contributed
by Mario Carneiro, 24-Aug-2015.)
|
                   |
|
Theorem | metres 12185 |
A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
     
           |
|
Theorem | 0met 12186 |
The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario
Carneiro, 14-Aug-2015.)
|
     |
|
6.2.3 Metric space balls
|
|
Theorem | blfvalps 12187* |
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 12188* |
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 12189 |
A ball is a set. (Contributed by Jim Kingdon, 4-May-2023.)
|
            |
|
Theorem | blvalps 12190* |
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 12191* |
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 12192 |
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 12193 |
Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by
Mario Carneiro, 11-Nov-2013.)
|
                     
    |
|
Theorem | elbl2ps 12194 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
   PsMet     
            
   |
|
Theorem | elbl2 12195 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.)
|
         
 
                |
|
Theorem | elbl3ps 12196 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
   PsMet     
            
   |
|
Theorem | elbl3 12197 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
         
 
                |
|
Theorem | blcomps 12198 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
   PsMet     
        
           |
|
Theorem | blcom 12199 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.)
|
         
 
        
           |
|
Theorem | xblpnfps 12200 |
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 
             
    |