Type  Label  Description 
Statement 

Theorem  clsss 12301 
Subset relationship for closure. (Contributed by NM, 10Feb2007.)



Theorem  ntrss 12302 
Subset relationship for interior. (Contributed by NM, 3Oct2007.)
(Revised by Jim Kingdon, 11Mar2023.)



Theorem  sscls 12303 
A subset of a topology's underlying set is included in its closure.
(Contributed by NM, 22Feb2007.)



Theorem  ntrss2 12304 
A subset includes its interior. (Contributed by NM, 3Oct2007.)
(Revised by Mario Carneiro, 11Nov2013.)



Theorem  ssntr 12305 
An open subset of a set is a subset of the set's interior. (Contributed
by Jeff Hankins, 31Aug2009.) (Revised by Mario Carneiro,
11Nov2013.)



Theorem  ntrss3 12306 
The interior of a subset of a topological space is included in the
space. (Contributed by NM, 1Oct2007.)



Theorem  ntrin 12307 
A pairwise intersection of interiors is the interior of the
intersection. This does not always hold for arbitrary intersections.
(Contributed by Jeff Hankins, 31Aug2009.)



Theorem  isopn3 12308 
A subset is open iff it equals its own interior. (Contributed by NM,
9Oct2006.) (Revised by Mario Carneiro, 11Nov2013.)



Theorem  ntridm 12309 
The interior operation is idempotent. (Contributed by NM,
2Oct2007.)



Theorem  clstop 12310 
The closure of a topology's underlying set is the entire set.
(Contributed by NM, 5Oct2007.) (Proof shortened by Jim Kingdon,
11Mar2023.)



Theorem  ntrtop 12311 
The interior of a topology's underlying set is the entire set.
(Contributed by NM, 12Sep2006.)



Theorem  clsss2 12312 
If a subset is included in a closed set, so is the subset's closure.
(Contributed by NM, 22Feb2007.)



Theorem  clsss3 12313 
The closure of a subset of a topological space is included in the space.
(Contributed by NM, 26Feb2007.)



Theorem  ntrcls0 12314 
A subset whose closure has an empty interior also has an empty interior.
(Contributed by NM, 4Oct2007.)



Theorem  ntreq0 12315* 
Two ways to say that a subset has an empty interior. (Contributed by
NM, 3Oct2007.) (Revised by Jim Kingdon, 11Mar2023.)



Theorem  cls0 12316 
The closure of the empty set. (Contributed by NM, 2Oct2007.) (Proof
shortened by Jim Kingdon, 12Mar2023.)



Theorem  ntr0 12317 
The interior of the empty set. (Contributed by NM, 2Oct2007.)



Theorem  isopn3i 12318 
An open subset equals its own interior. (Contributed by Mario Carneiro,
30Dec2016.)



Theorem  discld 12319 
The open sets of a discrete topology are closed and its closed sets are
open. (Contributed by FL, 7Jun2007.) (Revised by Mario Carneiro,
7Apr2015.)



Theorem  sn0cld 12320 
The closed sets of the topology .
(Contributed by FL,
5Jan2009.)



7.1.5 Neighborhoods


Syntax  cnei 12321 
Extend class notation with neighborhood relation for topologies.



Definition  dfnei 12322* 
Define a function on topologies whose value is a map from a subset to
its neighborhoods. (Contributed by NM, 11Feb2007.)



Theorem  neifval 12323* 
Value of the neighborhood function on the subsets of the base set of a
topology. (Contributed by NM, 11Feb2007.) (Revised by Mario
Carneiro, 11Nov2013.)



Theorem  neif 12324 
The neighborhood function is a function from the set of the subsets of
the base set of a topology. (Contributed by NM, 12Feb2007.) (Revised
by Mario Carneiro, 11Nov2013.)



Theorem  neiss2 12325 
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, 12Feb2007.)



Theorem  neival 12326* 
Value of the set of neighborhoods of a subset of the base set of a
topology. (Contributed by NM, 11Feb2007.) (Revised by Mario
Carneiro, 11Nov2013.)



Theorem  isnei 12327* 
The predicate "the class is a neighborhood of ".
(Contributed by FL, 25Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)



Theorem  neiint 12328 
An intuitive definition of a neighborhood in terms of interior.
(Contributed by Szymon Jaroszewicz, 18Dec2007.) (Revised by Mario
Carneiro, 11Nov2013.)



Theorem  isneip 12329* 
The predicate "the class is a neighborhood of point ".
(Contributed by NM, 26Feb2007.)



Theorem  neii1 12330 
A neighborhood is included in the topology's base set. (Contributed by
NM, 12Feb2007.)



Theorem  neisspw 12331 
The neighborhoods of any set are subsets of the base set. (Contributed
by Stefan O'Rear, 6Aug2015.)



Theorem  neii2 12332* 
Property of a neighborhood. (Contributed by NM, 12Feb2007.)



Theorem  neiss 12333 
Any neighborhood of a set is also a neighborhood of any subset
. Similar to Proposition 1 of [BourbakiTop1] p. I.2.
(Contributed by FL, 25Sep2006.)



Theorem  ssnei 12334 
A set is included in any of its neighborhoods. Generalization to
subsets of elnei 12335. (Contributed by FL, 16Nov2006.)



Theorem  elnei 12335 
A point belongs to any of its neighborhoods. Property V_{iii} of
[BourbakiTop1] p. I.3. (Contributed
by FL, 28Sep2006.)



Theorem  0nnei 12336 
The empty set is not a neighborhood of a nonempty set. (Contributed by
FL, 18Sep2007.)



Theorem  neipsm 12337* 
A neighborhood of a set is a neighborhood of every point in the set.
Proposition 1 of [BourbakiTop1] p.
I.2. (Contributed by FL,
16Nov2006.) (Revised by Jim Kingdon, 22Mar2023.)



Theorem  opnneissb 12338 
An open set is a neighborhood of any of its subsets. (Contributed by
FL, 2Oct2006.)



Theorem  opnssneib 12339 
Any superset of an open set is a neighborhood of it. (Contributed by
NM, 14Feb2007.)



Theorem  ssnei2 12340 
Any subset of containing a neighborhood
of a set
is a neighborhood of this set. Generalization to subsets of Property
V_{i} of [BourbakiTop1] p. I.3. (Contributed by FL,
2Oct2006.)



Theorem  opnneiss 12341 
An open set is a neighborhood of any of its subsets. (Contributed by NM,
13Feb2007.)



Theorem  opnneip 12342 
An open set is a neighborhood of any of its members. (Contributed by NM,
8Mar2007.)



Theorem  tpnei 12343 
The underlying set of a topology is a neighborhood of any of its
subsets. Special case of opnneiss 12341. (Contributed by FL,
2Oct2006.)



Theorem  neiuni 12344 
The union of the neighborhoods of a set equals the topology's underlying
set. (Contributed by FL, 18Sep2007.) (Revised by Mario Carneiro,
9Apr2015.)



Theorem  topssnei 12345 
A finer topology has more neighborhoods. (Contributed by Mario
Carneiro, 9Apr2015.)



Theorem  innei 12346 
The intersection of two neighborhoods of a set is also a neighborhood of
the set. Generalization to subsets of Property V_{ii} of [BourbakiTop1]
p. I.3 for binary intersections. (Contributed by FL, 28Sep2006.)



Theorem  opnneiid 12347 
Only an open set is a neighborhood of itself. (Contributed by FL,
2Oct2006.)



Theorem  neissex 12348* 
For any neighborhood
of , there is a
neighborhood of
such that is a neighborhood of all
subsets of .
Generalization to subsets of Property V_{iv} of [BourbakiTop1] p. I.3.
(Contributed by FL, 2Oct2006.)



Theorem  0nei 12349 
The empty set is a neighborhood of itself. (Contributed by FL,
10Dec2006.)



7.1.6 Subspace topologies


Theorem  restrcl 12350 
Reverse closure for the subspace topology. (Contributed by Mario
Carneiro, 19Mar2015.) (Proof shortened by Jim Kingdon,
23Mar2023.)

↾_{t}


Theorem  restbasg 12351 
A subspace topology basis is a basis. (Contributed by Mario Carneiro,
19Mar2015.)

↾_{t} 

Theorem  tgrest 12352 
A subspace can be generated by restricted sets from a basis for the
original topology. (Contributed by Mario Carneiro, 19Mar2015.)
(Proof shortened by Mario Carneiro, 30Aug2015.)

↾_{t} ↾_{t} 

Theorem  resttop 12353 
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, 15Apr2007.) (Revised by Mario Carneiro,
1May2015.)

↾_{t} 

Theorem  resttopon 12354 
A subspace topology is a topology on the base set. (Contributed by
Mario Carneiro, 13Aug2015.)

TopOn
↾_{t} TopOn 

Theorem  restuni 12355 
The underlying set of a subspace topology. (Contributed by FL,
5Jan2009.) (Revised by Mario Carneiro, 13Aug2015.)

↾_{t} 

Theorem  stoig 12356 
The topological space built with a subspace topology. (Contributed by
FL, 5Jan2009.) (Proof shortened by Mario Carneiro, 1May2015.)

TopSet
↾_{t} 

Theorem  restco 12357 
Composition of subspaces. (Contributed by Mario Carneiro, 15Dec2013.)
(Revised by Mario Carneiro, 1May2015.)

↾_{t} ↾_{t} ↾_{t} 

Theorem  restabs 12358 
Equivalence of being a subspace of a subspace and being a subspace of the
original. (Contributed by Jeff Hankins, 11Jul2009.) (Proof shortened
by Mario Carneiro, 1May2015.)

↾_{t} ↾_{t} ↾_{t} 

Theorem  restin 12359 
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, 15Dec2013.)

↾_{t} ↾_{t} 

Theorem  restuni2 12360 
The underlying set of a subspace topology. (Contributed by Mario
Carneiro, 21Mar2015.)

↾_{t} 

Theorem  resttopon2 12361 
The underlying set of a subspace topology. (Contributed by Mario
Carneiro, 13Aug2015.)

TopOn
↾_{t} TopOn 

Theorem  rest0 12362 
The subspace topology induced by the topology on the empty set.
(Contributed by FL, 22Dec2008.) (Revised by Mario Carneiro,
1May2015.)

↾_{t} 

Theorem  restsn 12363 
The only subspace topology induced by the topology .
(Contributed by FL, 5Jan2009.) (Revised by Mario Carneiro,
15Dec2013.)

↾_{t}


Theorem  restopnb 12364 
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, 2Mar2015.)

↾_{t} 

Theorem  ssrest 12365 
If is a finer
topology than , then
the subspace topologies
induced by
maintain this relationship. (Contributed by Mario
Carneiro, 21Mar2015.) (Revised by Mario Carneiro, 1May2015.)

↾_{t} ↾_{t} 

Theorem  restopn2 12366 
If is open, then is open in iff it is an open subset
of
. (Contributed
by Mario Carneiro, 2Mar2015.)

↾_{t}


Theorem  restdis 12367 
A subspace of a discrete topology is discrete. (Contributed by Mario
Carneiro, 19Mar2015.)

↾_{t}


7.1.7 Limits and continuity in topological
spaces


Syntax  ccn 12368 
Extend class notation with the class of continuous functions between
topologies.



Syntax  ccnp 12369 
Extend class notation with the class of functions between topologies
continuous at a given point.



Syntax  clm 12370 
Extend class notation with a function on topological spaces whose value is
the convergence relation for limit sequences in the space.



Definition  dfcn 12371* 
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 12380 for the predicate
form. (Contributed by NM, 17Oct2006.)



Definition  dfcnp 12372* 
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, 17Oct2006.)



Definition  dflm 12373* 
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
realvalued function
converges to zero (in the standard topology on the reals) with this
definition. (Contributed by NM, 7Sep2006.)



Theorem  lmrcl 12374 
Reverse closure for the convergence relation. (Contributed by Mario
Carneiro, 7Sep2015.)



Theorem  lmfval 12375* 
The relation "sequence converges to point " in a metric
space. (Contributed by NM, 7Sep2006.) (Revised by Mario Carneiro,
21Aug2015.)

TopOn


Theorem  lmreltop 12376 
The topological space convergence relation is a relation. (Contributed
by Jim Kingdon, 25Mar2023.)



Theorem  cnfval 12377* 
The set of all continuous functions from topology to topology
. (Contributed
by NM, 17Oct2006.) (Revised by Mario Carneiro,
21Aug2015.)

TopOn
TopOn


Theorem  cnpfval 12378* 
The function mapping the points in a topology to the set of all
functions from
to topology
continuous at that point.
(Contributed by NM, 17Oct2006.) (Revised by Mario Carneiro,
21Aug2015.)

TopOn
TopOn


Theorem  cnovex 12379 
The class of all continuous functions from a topology to another is a
set. (Contributed by Jim Kingdon, 14Dec2023.)



Theorem  iscn 12380* 
The predicate "the class is a continuous function from topology
to topology
". Definition of
continuous function in
[Munkres] p. 102. (Contributed by NM,
17Oct2006.) (Revised by Mario
Carneiro, 21Aug2015.)

TopOn
TopOn


Theorem  cnpval 12381* 
The set of all functions from topology to topology that are
continuous at a point . (Contributed by NM, 17Oct2006.)
(Revised by Mario Carneiro, 11Nov2013.)

TopOn
TopOn


Theorem  iscnp 12382* 
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,
17Oct2006.) (Revised by Mario
Carneiro, 21Aug2015.)

TopOn
TopOn


Theorem  iscn2 12383* 
The predicate "the class is a continuous function from topology
to topology
". Definition of
continuous function in
[Munkres] p. 102. (Contributed by Mario
Carneiro, 21Aug2015.)



Theorem  cntop1 12384 
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21Aug2015.)



Theorem  cntop2 12385 
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21Aug2015.)



Theorem  iscnp3 12386* 
The predicate "the class is a continuous function from topology
to topology
at point ". (Contributed by
NM,
15May2007.)

TopOn
TopOn


Theorem  cnf 12387 
A continuous function is a mapping. (Contributed by FL, 8Dec2006.)
(Revised by Mario Carneiro, 21Aug2015.)



Theorem  cnf2 12388 
A continuous function is a mapping. (Contributed by Mario Carneiro,
21Aug2015.)

TopOn
TopOn 

Theorem  cnprcl2k 12389 
Reverse closure for a function continuous at a point. (Contributed by
Mario Carneiro, 21Aug2015.) (Revised by Jim Kingdon, 28Mar2023.)

TopOn


Theorem  cnpf2 12390 
A continuous function at point is a mapping. (Contributed by
Mario Carneiro, 21Aug2015.) (Revised by Jim Kingdon, 28Mar2023.)

TopOn
TopOn 

Theorem  tgcn 12391* 
The continuity predicate when the range is given by a basis for a
topology. (Contributed by Mario Carneiro, 7Feb2015.) (Revised by
Mario Carneiro, 22Aug2015.)

TopOn TopOn


Theorem  tgcnp 12392* 
The "continuous at a point" predicate when the range is given by a
basis
for a topology. (Contributed by Mario Carneiro, 3Feb2015.) (Revised
by Mario Carneiro, 22Aug2015.)

TopOn TopOn


Theorem  ssidcn 12393 
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, 21Mar2015.) (Revised by
Mario Carneiro, 21Aug2015.)

TopOn
TopOn


Theorem  icnpimaex 12394* 
Property of a function continuous at a point. (Contributed by FL,
31Dec2006.) (Revised by Jim Kingdon, 28Mar2023.)

TopOn TopOn


Theorem  idcn 12395 
A restricted identity function is a continuous function. (Contributed
by FL, 27Dec2006.) (Proof shortened by Mario Carneiro,
21Mar2015.)

TopOn 

Theorem  lmbr 12396* 
Express the binary relation "sequence converges to point
" in a
topological space. Definition 1.41 of [Kreyszig] p. 25.
The condition
allows us to use objects
more general
than sequences when convenient; see the comment in dflm 12373.
(Contributed by Mario Carneiro, 14Nov2013.)

TopOn


Theorem  lmbr2 12397* 
Express the binary relation "sequence converges to point
" in a
metric space using an arbitrary upper set of integers.
(Contributed by Mario Carneiro, 14Nov2013.)

TopOn


Theorem  lmbrf 12398* 
Express the binary relation "sequence converges to point
" in a
metric space using an arbitrary upper set of integers.
This version of lmbr2 12397 presupposes that is a function.
(Contributed by Mario Carneiro, 14Nov2013.)

TopOn


Theorem  lmconst 12399 
A constant sequence converges to its value. (Contributed by NM,
8Nov2007.) (Revised by Mario Carneiro, 14Nov2013.)

TopOn


Theorem  lmcvg 12400* 
Convergence property of a converging sequence. (Contributed by Mario
Carneiro, 14Nov2013.)

