Type  Label  Description 
Statement 

Definition  dfcld 12301* 
Define a function on topologies whose value is the set of closed sets of
the topology. (Contributed by NM, 2Oct2006.)

⊢ Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗
∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗}) 

Definition  dfntr 12302* 
Define a function on topologies whose value is the interior function on
the subsets of the base set. See ntrval 12316. (Contributed by NM,
10Sep2006.)

⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∪ (𝑗 ∩ 𝒫 𝑥))) 

Definition  dfcls 12303* 
Define a function on topologies whose value is the closure function on
the subsets of the base set. See clsval 12317. (Contributed by NM,
3Oct2006.)

⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) 

Theorem  fncld 12304 
The closedset generator is a wellbehaved function. (Contributed by
Stefan O'Rear, 1Feb2015.)

⊢ Clsd Fn Top 

Theorem  cldval 12305* 
The set of closed sets of a topology. (Note that the set of open sets
is just the topology itself, so we don't have a separate definition.)
(Contributed by NM, 2Oct2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ 𝐽}) 

Theorem  ntrfval 12306* 
The interior function on the subsets of a topology's base set.
(Contributed by NM, 10Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (int‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∪
(𝐽 ∩ 𝒫 𝑥))) 

Theorem  clsfval 12307* 
The closure function on the subsets of a topology's base set.
(Contributed by NM, 3Oct2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (cls‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∩
{𝑦 ∈
(Clsd‘𝐽) ∣
𝑥 ⊆ 𝑦})) 

Theorem  cldrcl 12308 
Reverse closure of the closed set operation. (Contributed by Stefan
O'Rear, 22Feb2015.)

⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) 

Theorem  iscld 12309 
The predicate "the class 𝑆 is a closed set". (Contributed
by NM,
2Oct2006.) (Revised by Mario Carneiro, 11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽))) 

Theorem  iscld2 12310 
A subset of the underlying set of a topology is closed iff its
complement is open. (Contributed by NM, 4Oct2006.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑆) ∈ 𝐽)) 

Theorem  cldss 12311 
A closed set is a subset of the underlying set of a topology.
(Contributed by NM, 5Oct2006.) (Revised by Stefan O'Rear,
22Feb2015.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ 𝑋) 

Theorem  cldss2 12312 
The set of closed sets is contained in the powerset of the base.
(Contributed by Mario Carneiro, 6Jan2014.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋 

Theorem  cldopn 12313 
The complement of a closed set is open. (Contributed by NM,
5Oct2006.) (Revised by Stefan O'Rear, 22Feb2015.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑆 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑆) ∈ 𝐽) 

Theorem  difopn 12314 
The difference of a closed set with an open set is open. (Contributed
by Mario Carneiro, 6Jan2014.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽) 

Theorem  topcld 12315 
The underlying set of a topology is closed. Part of Theorem 6.1(1) of
[Munkres] p. 93. (Contributed by NM,
3Oct2006.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽)) 

Theorem  ntrval 12316 
The interior of a subset of a topology's base set is the union of all
the open sets it includes. Definition of interior of [Munkres] p. 94.
(Contributed by NM, 10Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = ∪ (𝐽 ∩ 𝒫 𝑆)) 

Theorem  clsval 12317* 
The closure of a subset of a topology's base set is the intersection of
all the closed sets that include it. Definition of closure of [Munkres]
p. 94. (Contributed by NM, 10Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥}) 

Theorem  0cld 12318 
The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93.
(Contributed by NM, 4Oct2006.)

⊢ (𝐽 ∈ Top → ∅ ∈
(Clsd‘𝐽)) 

Theorem  uncld 12319 
The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of
[Munkres] p. 93. (Contributed by NM,
5Oct2006.)

⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∪ 𝐵) ∈ (Clsd‘𝐽)) 

Theorem  cldcls 12320 
A closed subset equals its own closure. (Contributed by NM,
15Mar2007.)

⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆) 

Theorem  iuncld 12321* 
A finite indexed union of closed sets is closed. (Contributed by Mario
Carneiro, 19Sep2015.) (Revised by Jim Kingdon, 10Mar2023.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) 

Theorem  unicld 12322 
A finite union of closed sets is closed. (Contributed by Mario
Carneiro, 19Sep2015.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪
𝐴 ∈ (Clsd‘𝐽)) 

Theorem  ntropn 12323 
The interior of a subset of a topology's underlying set is open.
(Contributed by NM, 11Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ∈ 𝐽) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆)) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆)) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆)) → 𝑂 ⊆ ((int‘𝐽)‘𝑆)) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((int‘𝐽)‘(𝐴 ∩ 𝐵)) = (((int‘𝐽)‘𝐴) ∩ ((int‘𝐽)‘𝐵))) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆)) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆)) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐶 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝐶) → ((cls‘𝐽)‘𝑆) ⊆ 𝐶) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑆)) = ∅) → ((int‘𝐽)‘𝑆) = ∅) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((int‘𝐽)‘𝑆) = ∅ ↔ ∀𝑥 ∈ 𝐽 (𝑥 ⊆ 𝑆 → 𝑥 = ∅))) 

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

⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) =
∅) 

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

⊢ (𝐽 ∈ Top → ((int‘𝐽)‘∅) =
∅) 

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

⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆) 

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

⊢ (𝐴 ∈ 𝑉 → (Clsd‘𝒫 𝐴) = 𝒫 𝐴) 

Theorem  sn0cld 12343 
The closed sets of the topology {∅}.
(Contributed by FL,
5Jan2009.)

⊢ (Clsd‘{∅}) =
{∅} 

7.1.5 Neighborhoods


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

class nei 

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

⊢ nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ {𝑦 ∈
𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)})) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (nei‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ {𝑣 ∈ 𝒫 𝑋 ∣ ∃𝑔 ∈ 𝐽 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣)})) 

Theorem  neif 12347 
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.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (nei‘𝐽) Fn 𝒫 𝑋) 

Theorem  neiss2 12348 
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.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋) 

Theorem  neival 12349* 
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.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((nei‘𝐽)‘𝑆) = {𝑣 ∈ 𝒫 𝑋 ∣ ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣)}) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁)))) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ 𝑆 ⊆ ((int‘𝐽)‘𝑁))) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁)))) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑁 ⊆ 𝑋) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋) 

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

⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁)) 

Theorem  neiss 12356 
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.)

⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑅 ⊆ 𝑆) → 𝑁 ∈ ((nei‘𝐽)‘𝑅)) 

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

⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑁) 

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

⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝐴 ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑃 ∈ 𝑁) 

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

⊢ ((𝐽 ∈ Top ∧ 𝑆 ≠ ∅) → ¬ ∅ ∈
((nei‘𝐽)‘𝑆)) 

Theorem  neipsm 12360* 
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.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ∃𝑥 𝑥 ∈ 𝑆) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ ∀𝑝 ∈ 𝑆 𝑁 ∈ ((nei‘𝐽)‘{𝑝}))) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) 

Theorem  ssnei2 12363 
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.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) ∧ (𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ 𝑋)) → 𝑀 ∈ ((nei‘𝐽)‘𝑆)) 

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

⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘𝑆)) 

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

⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ((nei‘𝐽)‘𝑆))) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑋 = ∪
((nei‘𝐽)‘𝑆)) 

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

⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾
⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌) ∧ 𝐽 ⊆ 𝐾) → ((nei‘𝐽)‘𝑆) ⊆ ((nei‘𝐾)‘𝑆)) 

Theorem  innei 12369 
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.)

⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑀 ∈ ((nei‘𝐽)‘𝑆)) → (𝑁 ∩ 𝑀) ∈ ((nei‘𝐽)‘𝑆)) 

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

⊢ (𝐽 ∈ Top → (𝑁 ∈ ((nei‘𝐽)‘𝑁) ↔ 𝑁 ∈ 𝐽)) 

Theorem  neissex 12371* 
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.)

⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑥 ∈ ((nei‘𝐽)‘𝑆)∀𝑦(𝑦 ⊆ 𝑥 → 𝑁 ∈ ((nei‘𝐽)‘𝑦))) 

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

⊢ (𝐽 ∈ Top → ∅ ∈
((nei‘𝐽)‘∅)) 

7.1.6 Subspace topologies


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

⊢ ((𝐽 ↾_{t} 𝐴) ∈ Top → (𝐽 ∈ V ∧ 𝐴 ∈ V)) 

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

⊢ ((𝐵 ∈ TopBases ∧ 𝐴 ∈ 𝑉) → (𝐵 ↾_{t} 𝐴) ∈ TopBases) 

Theorem  tgrest 12375 
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.)

⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (topGen‘(𝐵 ↾_{t} 𝐴)) = ((topGen‘𝐵) ↾_{t} 𝐴)) 

Theorem  resttop 12376 
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.)

⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾_{t} 𝐴) ∈ Top) 

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

⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾_{t} 𝐴) ∈ (TopOn‘𝐴)) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾_{t} 𝐴)) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → {⟨(Base‘ndx), 𝐴⟩,
⟨(TopSet‘ndx), (𝐽 ↾_{t} 𝐴)⟩} ∈ TopSp) 

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

⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝐽 ↾_{t} 𝐴) ↾_{t} 𝐵) = (𝐽 ↾_{t} (𝐴 ∩ 𝐵))) 

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

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝑋) = ∪ (𝐽 ↾_{t} 𝐴)) 

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

⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾_{t} 𝐴) ∈ (TopOn‘(𝐴 ∩ 𝑋))) 

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

⊢ (𝐽 ∈ Top → (𝐽 ↾_{t} ∅) =
{∅}) 

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

⊢ (𝐴 ∈ 𝑉 → ({∅} ↾_{t}
𝐴) =
{∅}) 

Theorem  restopnb 12387 
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.)

⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐵)) → (𝐶 ∈ 𝐽 ↔ 𝐶 ∈ (𝐽 ↾_{t} 𝐴))) 

Theorem  ssrest 12388 
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 12389 
If 𝐴 is open, then 𝐵 is open in 𝐴 iff it
is an open subset of
𝐴. (Contributed by Mario Carneiro,
2Mar2015.)

⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → (𝐵 ∈ (𝐽 ↾_{t} 𝐴) ↔ (𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴))) 

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

class Cn 

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

class CnP 

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

class ⇝_{𝑡} 

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

⊢ Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑_{𝑚}
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (^{◡}𝑓 “ 𝑦) ∈ 𝑗}) 

Definition  dfcnp 12395* 
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.)

⊢ CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑_{𝑚}
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})) 

Definition  dflm 12396* 
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 (𝑥 ∈ ℝ ↦ (sin‘(π
· 𝑥)))
converges to zero (in the standard topology on the reals) with this
definition. (Contributed by NM, 7Sep2006.)

⊢ ⇝_{𝑡} = (𝑗 ∈ Top ↦
{⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗
↑_{pm} ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ_{≥}(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) 

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

⊢ (𝐹(⇝_{𝑡}‘𝐽)𝑃 → 𝐽 ∈ Top) 

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

⊢ (𝐽 ∈ (TopOn‘𝑋) →
(⇝_{𝑡}‘𝐽) = {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋 ↑_{pm} ℂ) ∧
𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ_{≥}(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) 

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

⊢ (𝐽 ∈ Top → Rel
(⇝_{𝑡}‘𝐽)) 

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

⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 Cn 𝐾) = {𝑓 ∈ (𝑌 ↑_{𝑚} 𝑋) ∣ ∀𝑦 ∈ 𝐾 (^{◡}𝑓 “ 𝑦) ∈ 𝐽}) 