Type  Label  Description 
Statement 

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



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



Theorem  neiuni 12403 
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 12404 
A finer topology has more neighborhoods. (Contributed by Mario
Carneiro, 9Apr2015.)



Theorem  innei 12405 
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 12406 
Only an open set is a neighborhood of itself. (Contributed by FL,
2Oct2006.)



Theorem  neissex 12407* 
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 12408 
The empty set is a neighborhood of itself. (Contributed by FL,
10Dec2006.)



7.1.6 Subspace topologies


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

↾_{t}


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

↾_{t} 

Theorem  tgrest 12411 
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 12412 
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 12413 
A subspace topology is a topology on the base set. (Contributed by
Mario Carneiro, 13Aug2015.)

TopOn
↾_{t} TopOn 

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

↾_{t} 

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

TopSet
↾_{t} 

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

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

Theorem  restabs 12417 
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 12418 
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 12419 
The underlying set of a subspace topology. (Contributed by Mario
Carneiro, 21Mar2015.)

↾_{t} 

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

TopOn
↾_{t} TopOn 

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

↾_{t} 

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

↾_{t}


Theorem  restopnb 12423 
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 12424 
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 12425 
If is open, then is open in iff it is an open subset
of
. (Contributed
by Mario Carneiro, 2Mar2015.)

↾_{t}


Theorem  restdis 12426 
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 12427 
Extend class notation with the class of continuous functions between
topologies.



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



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



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



Definition  dfcnp 12431* 
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 12432* 
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 12433 
Reverse closure for the convergence relation. (Contributed by Mario
Carneiro, 7Sep2015.)



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

TopOn


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



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

TopOn
TopOn


Theorem  cnpfval 12437* 
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 12438 
The class of all continuous functions from a topology to another is a
set. (Contributed by Jim Kingdon, 14Dec2023.)



Theorem  iscn 12439* 
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 12440* 
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 12441* 
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 12442* 
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 12443 
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21Aug2015.)



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



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

TopOn
TopOn


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



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

TopOn
TopOn 

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

TopOn


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

TopOn
TopOn 

Theorem  tgcn 12450* 
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 12451* 
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 12452 
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 12453* 
Property of a function continuous at a point. (Contributed by FL,
31Dec2006.) (Revised by Jim Kingdon, 28Mar2023.)

TopOn TopOn


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

TopOn 

Theorem  lmbr 12455* 
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 12432.
(Contributed by Mario Carneiro, 14Nov2013.)

TopOn


Theorem  lmbr2 12456* 
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 12457* 
Express the binary relation "sequence converges to point
" in a
metric space using an arbitrary upper set of integers.
This version of lmbr2 12456 presupposes that is a function.
(Contributed by Mario Carneiro, 14Nov2013.)

TopOn


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

TopOn


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



Theorem  iscnp4 12460* 
The predicate "the class is a continuous function from topology
to topology
at point " in terms of
neighborhoods.
(Contributed by FL, 18Jul2011.) (Revised by Mario Carneiro,
10Sep2015.)

TopOn
TopOn


Theorem  cnpnei 12461* 
A condition for continuity at a point in terms of neighborhoods.
(Contributed by Jeff Hankins, 7Sep2009.)



Theorem  cnima 12462 
An open subset of the codomain of a continuous function has an open
preimage. (Contributed by FL, 15Dec2006.)



Theorem  cnco 12463 
The composition of two continuous functions is a continuous function.
(Contributed by FL, 8Dec2006.) (Revised by Mario Carneiro,
21Aug2015.)



Theorem  cnptopco 12464 
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, 16Nov2006.) (Proof
shortened by Mario Carneiro, 27Dec2014.)



Theorem  cnclima 12465 
A closed subset of the codomain of a continuous function has a closed
preimage. (Contributed by NM, 15Mar2007.) (Revised by Mario Carneiro,
21Aug2015.)



Theorem  cnntri 12466 
Property of the preimage of an interior. (Contributed by Mario
Carneiro, 25Aug2015.)



Theorem  cnntr 12467* 
Continuity in terms of interior. (Contributed by Jeff Hankins,
2Oct2009.) (Proof shortened by Mario Carneiro, 25Aug2015.)

TopOn
TopOn


Theorem  cnss1 12468 
If the topology is
finer than , then
there are more
continuous functions from than from .
(Contributed by Mario
Carneiro, 19Mar2015.) (Revised by Mario Carneiro, 21Aug2015.)

TopOn


Theorem  cnss2 12469 
If the topology is
finer than , then
there are fewer
continuous functions into than into
from some other space.
(Contributed by Mario Carneiro, 19Mar2015.) (Revised by Mario
Carneiro, 21Aug2015.)

TopOn


Theorem  cncnpi 12470 
A continuous function is continuous at all points. One direction of
Theorem 7.2(g) of [Munkres] p. 107.
(Contributed by Raph Levien,
20Nov2006.) (Proof shortened by Mario Carneiro, 21Aug2015.)



Theorem  cnsscnp 12471 
The set of continuous functions is a subset of the set of continuous
functions at a point. (Contributed by Raph Levien, 21Oct2006.)
(Revised by Mario Carneiro, 21Aug2015.)



Theorem  cncnp 12472* 
A continuous function is continuous at all points. Theorem 7.2(g) of
[Munkres] p. 107. (Contributed by NM,
15May2007.) (Proof shortened
by Mario Carneiro, 21Aug2015.)

TopOn
TopOn


Theorem  cncnp2m 12473* 
A continuous function is continuous at all points. Theorem 7.2(g) of
[Munkres] p. 107. (Contributed by Raph
Levien, 20Nov2006.) (Revised
by Jim Kingdon, 30Mar2023.)



Theorem  cnnei 12474* 
Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux,
3Jan2018.)



Theorem  cnconst2 12475 
A constant function is continuous. (Contributed by Mario Carneiro,
19Mar2015.)

TopOn
TopOn 

Theorem  cnconst 12476 
A constant function is continuous. (Contributed by FL, 15Jan2007.)
(Proof shortened by Mario Carneiro, 19Mar2015.)

TopOn TopOn


Theorem  cnrest 12477 
Continuity of a restriction from a subspace. (Contributed by Jeff
Hankins, 11Jul2009.) (Revised by Mario Carneiro, 21Aug2015.)

↾_{t} 

Theorem  cnrest2 12478 
Equivalence of continuity in the parent topology and continuity in a
subspace. (Contributed by Jeff Hankins, 10Jul2009.) (Proof shortened
by Mario Carneiro, 21Aug2015.)

TopOn
↾_{t} 

Theorem  cnrest2r 12479 
Equivalence of continuity in the parent topology and continuity in a
subspace. (Contributed by Jeff Madsen, 2Sep2009.) (Revised by Mario
Carneiro, 7Jun2014.)

↾_{t}


Theorem  cnptopresti 12480 
One direction of cnptoprest 12481 under the weaker condition that the point
is in the subset rather than the interior of the subset. (Contributed
by Mario Carneiro, 9Feb2015.) (Revised by Jim Kingdon,
31Mar2023.)

TopOn
↾_{t} 

Theorem  cnptoprest 12481 
Equivalence of continuity at a point and continuity of the restricted
function at a point. (Contributed by Mario Carneiro, 8Aug2014.)
(Revised by Jim Kingdon, 5Apr2023.)

↾_{t} 

Theorem  cnptoprest2 12482 
Equivalence of pointcontinuity in the parent topology and
pointcontinuity in a subspace. (Contributed by Mario Carneiro,
9Aug2014.) (Revised by Jim Kingdon, 6Apr2023.)

↾_{t} 

Theorem  cndis 12483 
Every function is continuous when the domain is discrete. (Contributed
by Mario Carneiro, 19Mar2015.) (Revised by Mario Carneiro,
21Aug2015.)

TopOn


Theorem  cnpdis 12484 
If is an isolated
point in (or
equivalently, the singleton
is open in ), then every function is continuous at
. (Contributed
by Mario Carneiro, 9Sep2015.)

TopOn TopOn


Theorem  lmfpm 12485 
If converges, then
is a partial
function. (Contributed by
Mario Carneiro, 23Dec2013.)

TopOn 

Theorem  lmfss 12486 
Inclusion of a function having a limit (used to ensure the limit
relation is a set, under our definition). (Contributed by NM,
7Dec2006.) (Revised by Mario Carneiro, 23Dec2013.)

TopOn


Theorem  lmcl 12487 
Closure of a limit. (Contributed by NM, 19Dec2006.) (Revised by
Mario Carneiro, 23Dec2013.)

TopOn 

Theorem  lmss 12488 
Limit on a subspace. (Contributed by NM, 30Jan2008.) (Revised by
Mario Carneiro, 30Dec2013.)

↾_{t} 

Theorem  sslm 12489 
A finer topology has fewer convergent sequences (but the sequences that
do converge, converge to the same value). (Contributed by Mario
Carneiro, 15Sep2015.)

TopOn
TopOn


Theorem  lmres 12490 
A function converges iff its restriction to an upper integers set
converges. (Contributed by Mario Carneiro, 31Dec2013.)

TopOn 

Theorem  lmff 12491* 
If converges, there
is some upper integer set on which is
a total function. (Contributed by Mario Carneiro, 31Dec2013.)

TopOn 

Theorem  lmtopcnp 12492 
The image of a convergent sequence under a continuous map is
convergent to the image of the original point. (Contributed by Mario
Carneiro, 3May2014.) (Revised by Jim Kingdon, 6Apr2023.)



Theorem  lmcn 12493 
The image of a convergent sequence under a continuous map is convergent
to the image of the original point. (Contributed by Mario Carneiro,
3May2014.)



7.1.8 Product topologies


Syntax  ctx 12494 
Extend class notation with the binary topological product operation.



Definition  dftx 12495* 
Define the binary topological product, which is homeomorphic to the
general topological product over a two element set, but is more
convenient to use. (Contributed by Jeff Madsen, 2Sep2009.)



Theorem  txvalex 12496 
Existence of the binary topological product. If and are
known to be topologies, see txtop 12502. (Contributed by Jim Kingdon,
3Aug2023.)



Theorem  txval 12497* 
Value of the binary topological product operation. (Contributed by Jeff
Madsen, 2Sep2009.) (Revised by Mario Carneiro, 30Aug2015.)



Theorem  txuni2 12498* 
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 31Aug2015.)



Theorem  txbasex 12499* 
The basis for the product topology is a set. (Contributed by Mario
Carneiro, 2Sep2015.)



Theorem  txbas 12500* 
The set of Cartesian products of elements from two topological bases is
a basis. (Contributed by Jeff Madsen, 2Sep2009.) (Revised by Mario
Carneiro, 31Aug2015.)

