Theorem List for Intuitionistic Logic Explorer - 12001-12100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cls0 12001 |
The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof
shortened by Jim Kingdon, 12-Mar-2023.)
|
           |
|
Theorem | ntr0 12002 |
The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
|
           |
|
Theorem | isopn3i 12003 |
An open subset equals its own interior. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
             |
|
Theorem | discld 12004 |
The open sets of a discrete topology are closed and its closed sets are
open. (Contributed by FL, 7-Jun-2007.) (Revised by Mario Carneiro,
7-Apr-2015.)
|
         |
|
Theorem | sn0cld 12005 |
The closed sets of the topology   .
(Contributed by FL,
5-Jan-2009.)
|
         |
|
6.1.5 Neighborhoods
|
|
Syntax | cnei 12006 |
Extend class notation with neighborhood relation for topologies.
|
 |
|
Definition | df-nei 12007* |
Define a function on topologies whose value is a map from a subset to
its neighborhoods. (Contributed by NM, 11-Feb-2007.)
|
        
     |
|
Theorem | neifval 12008* |
Value of the neighborhood function on the subsets of the base set of a
topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario
Carneiro, 11-Nov-2013.)
|
 
       
       |
|
Theorem | neif 12009 |
The neighborhood function is a function from the set of the subsets of
the base set of a topology. (Contributed by NM, 12-Feb-2007.) (Revised
by Mario Carneiro, 11-Nov-2013.)
|
 
       |
|
Theorem | neiss2 12010 |
A set with a neighborhood is a subset of the base set of a topology.
(This theorem depends on a function's value being empty outside of its
domain, but it will make later theorems simpler to state.) (Contributed
by NM, 12-Feb-2007.)
|
              |
|
Theorem | neival 12011* |
Value of the set of neighborhoods of a subset of the base set of a
topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario
Carneiro, 11-Nov-2013.)
|
  
          
      |
|
Theorem | isnei 12012* |
The predicate "the class is a neighborhood of ".
(Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
  
                  |
|
Theorem | neiint 12013 |
An intuitive definition of a neighborhood in terms of interior.
(Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario
Carneiro, 11-Nov-2013.)
|
  
 
       
           |
|
Theorem | isneip 12014* |
The predicate "the class is a neighborhood of point ".
(Contributed by NM, 26-Feb-2007.)
|
               
       |
|
Theorem | neii1 12015 |
A neighborhood is included in the topology's base set. (Contributed by
NM, 12-Feb-2007.)
|
              |
|
Theorem | neisspw 12016 |
The neighborhoods of any set are subsets of the base set. (Contributed
by Stefan O'Rear, 6-Aug-2015.)
|
 
           |
|
Theorem | neii2 12017* |
Property of a neighborhood. (Contributed by NM, 12-Feb-2007.)
|
           

   |
|
Theorem | neiss 12018 |
Any neighborhood of a set is also a neighborhood of any subset
. Similar to Proposition 1 of [BourbakiTop1] p. I.2.
(Contributed by FL, 25-Sep-2006.)
|
                     |
|
Theorem | ssnei 12019 |
A set is included in any of its neighborhoods. Generalization to
subsets of elnei 12020. (Contributed by FL, 16-Nov-2006.)
|
             |
|
Theorem | elnei 12020 |
A point belongs to any of its neighborhoods. Property Viii of
[BourbakiTop1] p. I.3. (Contributed
by FL, 28-Sep-2006.)
|
 
             |
|
Theorem | 0nnei 12021 |
The empty set is not a neighborhood of a nonempty set. (Contributed by
FL, 18-Sep-2007.)
|
             |
|
Theorem | neipsm 12022* |
A neighborhood of a set is a neighborhood of every point in the set.
Proposition 1 of [BourbakiTop1] p.
I.2. (Contributed by FL,
16-Nov-2006.) (Revised by Jim Kingdon, 22-Mar-2023.)
|
  
           
             |
|
Theorem | opnneissb 12023 |
An open set is a neighborhood of any of its subsets. (Contributed by
FL, 2-Oct-2006.)
|
    
           |
|
Theorem | opnssneib 12024 |
Any superset of an open set is a neighborhood of it. (Contributed by
NM, 14-Feb-2007.)
|
    
           |
|
Theorem | ssnei2 12025 |
Any subset of containing a neighborhood
of a set
is a neighborhood of this set. Generalization to subsets of Property
Vi of [BourbakiTop1] p. I.3. (Contributed by FL,
2-Oct-2006.)
|
             
            |
|
Theorem | opnneiss 12026 |
An open set is a neighborhood of any of its subsets. (Contributed by NM,
13-Feb-2007.)
|
  
          |
|
Theorem | opnneip 12027 |
An open set is a neighborhood of any of its members. (Contributed by NM,
8-Mar-2007.)
|
 
             |
|
Theorem | tpnei 12028 |
The underlying set of a topology is a neighborhood of any of its
subsets. Special case of opnneiss 12026. (Contributed by FL,
2-Oct-2006.)
|
 

           |
|
Theorem | neiuni 12029 |
The union of the neighborhoods of a set equals the topology's underlying
set. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro,
9-Apr-2015.)
|
  
            |
|
Theorem | topssnei 12030 |
A finer topology has more neighborhoods. (Contributed by Mario
Carneiro, 9-Apr-2015.)
|
    
                    |
|
Theorem | innei 12031 |
The intersection of two neighborhoods of a set is also a neighborhood of
the set. Generalization to subsets of Property Vii of [BourbakiTop1]
p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006.)
|
                    
          |
|
Theorem | opnneiid 12032 |
Only an open set is a neighborhood of itself. (Contributed by FL,
2-Oct-2006.)
|
 
       
   |
|
Theorem | neissex 12033* |
For any neighborhood
of , there is a
neighborhood of
such that is a neighborhood of all
subsets of .
Generalization to subsets of Property Viv of [BourbakiTop1] p. I.3.
(Contributed by FL, 2-Oct-2006.)
|
           
                       |
|
Theorem | 0nei 12034 |
The empty set is a neighborhood of itself. (Contributed by FL,
10-Dec-2006.)
|
           |
|
6.1.6 Subspace topologies
|
|
Theorem | restrcl 12035 |
Reverse closure for the subspace topology. (Contributed by Mario
Carneiro, 19-Mar-2015.) (Proof shortened by Jim Kingdon,
23-Mar-2023.)
|
  ↾t 
    |
|
Theorem | restbasg 12036 |
A subspace topology basis is a basis. (Contributed by Mario Carneiro,
19-Mar-2015.)
|
   
↾t    |
|
Theorem | tgrest 12037 |
A subspace can be generated by restricted sets from a basis for the
original topology. (Contributed by Mario Carneiro, 19-Mar-2015.)
(Proof shortened by Mario Carneiro, 30-Aug-2015.)
|
       ↾t        ↾t    |
|
Theorem | resttop 12038 |
A subspace topology is a topology. Definition of subspace topology in
[Munkres] p. 89. is normally a subset of the base set of
.
(Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro,
1-May-2015.)
|
   
↾t    |
|
Theorem | resttopon 12039 |
A subspace topology is a topology on the base set. (Contributed by
Mario Carneiro, 13-Aug-2015.)
|
  TopOn   
↾t  TopOn    |
|
Theorem | restuni 12040 |
The underlying set of a subspace topology. (Contributed by FL,
5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
|
  
   ↾t    |
|
Theorem | stoig 12041 |
The topological space built with a subspace topology. (Contributed by
FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
|
  
       
   TopSet   
↾t      |
|
Theorem | restco 12042 |
Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.)
(Revised by Mario Carneiro, 1-May-2015.)
|
     ↾t  ↾t   ↾t      |
|
Theorem | restabs 12043 |
Equivalence of being a subspace of a subspace and being a subspace of the
original. (Contributed by Jeff Hankins, 11-Jul-2009.) (Proof shortened
by Mario Carneiro, 1-May-2015.)
|
     ↾t  ↾t   ↾t    |
|
Theorem | restin 12044 |
When the subspace region is not a subset of the base of the topology,
the resulting set is the same as the subspace restricted to the base.
(Contributed by Mario Carneiro, 15-Dec-2013.)
|
    
↾t   ↾t      |
|
Theorem | restuni2 12045 |
The underlying set of a subspace topology. (Contributed by Mario
Carneiro, 21-Mar-2015.)
|
     
  ↾t    |
|
Theorem | resttopon2 12046 |
The underlying set of a subspace topology. (Contributed by Mario
Carneiro, 13-Aug-2015.)
|
  TopOn 
 
↾t  TopOn      |
|
Theorem | rest0 12047 |
The subspace topology induced by the topology on the empty set.
(Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro,
1-May-2015.)
|
 
↾t      |
|
Theorem | restsn 12048 |
The only subspace topology induced by the topology   .
(Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro,
15-Dec-2013.)
|
    ↾t
     |
|
Theorem | restopnb 12049 |
If is an open subset
of the subspace base set , then any
subset of is
open iff it is open in . (Contributed by Mario
Carneiro, 2-Mar-2015.)
|
  

   
 ↾t     |
|
Theorem | ssrest 12050 |
If is a finer
topology than , then
the subspace topologies
induced by
maintain this relationship. (Contributed by Mario
Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.)
|
    ↾t   ↾t    |
|
Theorem | restopn2 12051 |
If is open, then is open in iff it is an open subset
of
. (Contributed
by Mario Carneiro, 2-Mar-2015.)
|
     ↾t 
     |
|
Theorem | restdis 12052 |
A subspace of a discrete topology is discrete. (Contributed by Mario
Carneiro, 19-Mar-2015.)
|
     ↾t 
   |
|
6.1.7 Limits and continuity in topological
spaces
|
|
Syntax | ccn 12053 |
Extend class notation with the class of continuous functions between
topologies.
|
 |
|
Syntax | ccnp 12054 |
Extend class notation with the class of functions between topologies
continuous at a given point.
|
 |
|
Syntax | clm 12055 |
Extend class notation with a function on topological spaces whose value is
the convergence relation for limit sequences in the space.
|
  |
|
Definition | df-cn 12056* |
Define a function on two topologies whose value is the set of continuous
mappings from the first topology to the second. Based on definition of
continuous function in [Munkres] p. 102.
See iscn 12064 for the predicate
form. (Contributed by NM, 17-Oct-2006.)
|
    
  
        |
|
Definition | df-cnp 12057* |
Define a function on two topologies whose value is the set of continuous
mappings at a specified point in the first topology. Based on Theorem
7.2(g) of [Munkres] p. 107.
(Contributed by NM, 17-Oct-2006.)
|
         
    
     
      |
|
Definition | df-lm 12058* |
Define a function on topologies whose value is the convergence relation
for sequences into the given topological space. Although is
typically a sequence (a function from an upperset of integers) with
values in the topological space, it need not be. Note, however, that
the limit property concerns only values at integers, so that the
real-valued function        
converges to zero (in the standard topology on the reals) with this
definition. (Contributed by NM, 7-Sep-2006.)
|

          

             |
|
Theorem | lmrcl 12059 |
Reverse closure for the convergence relation. (Contributed by Mario
Carneiro, 7-Sep-2015.)
|
          |
|
Theorem | lmfval 12060* |
The relation "sequence converges to point " in a metric
space. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro,
21-Aug-2015.)
|
 TopOn               
  
          |
|
Theorem | lmreltop 12061 |
The topological space convergence relation is a relation. (Contributed
by Jim Kingdon, 25-Mar-2023.)
|
        |
|
Theorem | cnfval 12062* |
The set of all continuous functions from topology to topology
. (Contributed
by NM, 17-Oct-2006.) (Revised by Mario Carneiro,
21-Aug-2015.)
|
  TopOn 
TopOn  
              |
|
Theorem | cnpfval 12063* |
The function mapping the points in a topology to the set of all
functions from
to topology
continuous at that point.
(Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro,
21-Aug-2015.)
|
  TopOn 
TopOn  
           
 
   
      |
|
Theorem | iscn 12064* |
The predicate "the class is a continuous function from topology
to topology
". Definition of
continuous function in
[Munkres] p. 102. (Contributed by NM,
17-Oct-2006.) (Revised by Mario
Carneiro, 21-Aug-2015.)
|
  TopOn 
TopOn  
  
               |
|
Theorem | cnpval 12065* |
The set of all functions from topology to topology that are
continuous at a point . (Contributed by NM, 17-Oct-2006.)
(Revised by Mario Carneiro, 11-Nov-2013.)
|
  TopOn 
TopOn        
  
     
     
     |
|
Theorem | iscnp 12066* |
The predicate "the class is a continuous function from topology
to topology
at point ". Based on Theorem
7.2(g) of
[Munkres] p. 107. (Contributed by NM,
17-Oct-2006.) (Revised by Mario
Carneiro, 21-Aug-2015.)
|
  TopOn 
TopOn                    
     
      |
|
Theorem | iscn2 12067* |
The predicate "the class is a continuous function from topology
to topology
". Definition of
continuous function in
[Munkres] p. 102. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
      
                |
|
Theorem | cntop1 12068 |
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
  
  |
|
Theorem | cntop2 12069 |
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
  
  |
|
Theorem | iscnp3 12070* |
The predicate "the class is a continuous function from topology
to topology
at point ". (Contributed by
NM,
15-May-2007.)
|
  TopOn 
TopOn                    
             |
|
Theorem | cnf 12071 |
A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.)
(Revised by Mario Carneiro, 21-Aug-2015.)
|
           |
|
Theorem | cnf2 12072 |
A continuous function is a mapping. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
  TopOn 
TopOn           |
|
Theorem | cnprcl2k 12073 |
Reverse closure for a function continuous at a point. (Contributed by
Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|
  TopOn 
      
  |
|
Theorem | cnpf2 12074 |
A continuous function at point is a mapping. (Contributed by
Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|
  TopOn 
TopOn               |
|
Theorem | tgcn 12075* |
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 12076* |
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 12077 |
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 12078* |
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 12079 |
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 12080* |
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 12058.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
 TopOn             
   
 
          |
|
Theorem | lmbr2 12081* |
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 12082* |
Express the binary relation "sequence converges to point
" in a
metric space using an arbitrary upper set of integers.
This version of lmbr2 12081 presupposes that is a function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
 TopOn                       
                       |
|
Theorem | lmconst 12083 |
A constant sequence converges to its value. (Contributed by NM,
8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
      TopOn 
              |
|
Theorem | lmcvg 12084* |
Convergence property of a converging sequence. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
                     
           |
|
Theorem | iscnp4 12085* |
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 12086* |
A condition for continuity at a point in terms of neighborhoods.
(Contributed by Jeff Hankins, 7-Sep-2009.)
|
    
             
                                 |
|
Theorem | cnima 12087 |
An open subset of the codomain of a continuous function has an open
preimage. (Contributed by FL, 15-Dec-2006.)
|
  
         |
|
Theorem | cnco 12088 |
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 12089 |
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 12090 |
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 12091 |
Property of the preimage of an interior. (Contributed by Mario
Carneiro, 25-Aug-2015.)
|
                                  |
|
Theorem | cnntr 12092* |
Continuity in terms of interior. (Contributed by Jeff Hankins,
2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
  TopOn 
TopOn  
  
                                     |
|
Theorem | cnss1 12093 |
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 12094 |
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 12095 |
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 12096 |
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 12097* |
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 12098* |
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 12099* |
Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux,
3-Jan-2018.)
|
                             
              
   |
|
Theorem | cnconst2 12100 |
A constant function is continuous. (Contributed by Mario Carneiro,
19-Mar-2015.)
|
  TopOn 
TopOn           |