Type  Label  Description 
Statement 

Theorem  tpstop 11901 
The topology extractor on a topological space is a topology.
(Contributed by FL, 27Jun2014.)



Theorem  tpspropd 11902 
A topological space depends only on the base and topology components.
(Contributed by NM, 18Jul2006.) (Revised by Mario Carneiro,
13Aug2015.)



Theorem  topontopn 11903 
Express the predicate "is a topological space." (Contributed by
Mario
Carneiro, 13Aug2015.)

TopSet TopOn 

Theorem  tsettps 11904 
If the topology component is already correctly truncated, then it forms
a topological space (with the topology extractor function coming out the
same as the component). (Contributed by Mario Carneiro,
13Aug2015.)

TopSet TopOn 

Theorem  istpsi 11905 
Properties that determine a topological space. (Contributed by NM,
20Oct2012.)



Theorem  eltpsg 11906 
Properties that determine a topological space from a construction (using
no explicit indices). (Contributed by Mario Carneiro, 13Aug2015.)

TopSet
TopOn 

Theorem  eltpsi 11907 
Properties that determine a topological space from a construction (using
no explicit indices). (Contributed by NM, 20Oct2012.) (Revised by
Mario Carneiro, 13Aug2015.)

TopSet


6.1.2 Topological bases


Syntax  ctb 11908 
Syntax for the class of topological bases.



Definition  dfbases 11909* 
Define the class of topological bases. Equivalent to definition of
basis in [Munkres] p. 78 (see isbasis2g 11911). Note that "bases" is the
plural of "basis". (Contributed by NM, 17Jul2006.)



Theorem  isbasisg 11910* 
Express the predicate "the set is a basis for a topology".
(Contributed by NM, 17Jul2006.)



Theorem  isbasis2g 11911* 
Express the predicate "the set is a basis for a topology".
(Contributed by NM, 17Jul2006.)



Theorem  isbasis3g 11912* 
Express the predicate "the set is a basis for a topology".
Definition of basis in [Munkres] p. 78.
(Contributed by NM,
17Jul2006.)



Theorem  basis1 11913 
Property of a basis. (Contributed by NM, 16Jul2006.)



Theorem  basis2 11914* 
Property of a basis. (Contributed by NM, 17Jul2006.)



Theorem  fiinbas 11915* 
If a set is closed under finite intersection, then it is a basis for a
topology. (Contributed by Jeff Madsen, 2Sep2009.)



Theorem  baspartn 11916* 
A disjoint system of sets is a basis for a topology. (Contributed by
Stefan O'Rear, 22Feb2015.)



Theorem  tgval 11917* 
The topology generated by a basis. See also tgval2 11919 and tgval3 11926.
(Contributed by NM, 16Jul2006.) (Revised by Mario Carneiro,
10Jan2015.)



Theorem  tgvalex 11918 
The topology generated by a basis is a set. (Contributed by Jim
Kingdon, 4Mar2023.)



Theorem  tgval2 11919* 
Definition of a topology generated by a basis in [Munkres] p. 78. Later
we show (in tgcl 11932) that is indeed a topology (on
, see unitg 11930). See also tgval 11917 and tgval3 11926. (Contributed
by NM, 15Jul2006.) (Revised by Mario Carneiro, 10Jan2015.)



Theorem  eltg 11920 
Membership in a topology generated by a basis. (Contributed by NM,
16Jul2006.) (Revised by Mario Carneiro, 10Jan2015.)



Theorem  eltg2 11921* 
Membership in a topology generated by a basis. (Contributed by NM,
15Jul2006.) (Revised by Mario Carneiro, 10Jan2015.)



Theorem  eltg2b 11922* 
Membership in a topology generated by a basis. (Contributed by Mario
Carneiro, 17Jun2014.) (Revised by Mario Carneiro, 10Jan2015.)



Theorem  eltg4i 11923 
An open set in a topology generated by a basis is the union of all basic
open sets contained in it. (Contributed by Stefan O'Rear,
22Feb2015.)



Theorem  eltg3i 11924 
The union of a set of basic open sets is in the generated topology.
(Contributed by Mario Carneiro, 30Aug2015.)



Theorem  eltg3 11925* 
Membership in a topology generated by a basis. (Contributed by NM,
15Jul2006.) (Revised by Jim Kingdon, 4Mar2023.)



Theorem  tgval3 11926* 
Alternate expression for the topology generated by a basis. Lemma 2.1
of [Munkres] p. 80. See also tgval 11917 and tgval2 11919. (Contributed by
NM, 17Jul2006.) (Revised by Mario Carneiro, 30Aug2015.)



Theorem  tg1 11927 
Property of a member of a topology generated by a basis. (Contributed
by NM, 20Jul2006.)



Theorem  tg2 11928* 
Property of a member of a topology generated by a basis. (Contributed
by NM, 20Jul2006.)



Theorem  bastg 11929 
A member of a basis is a subset of the topology it generates.
(Contributed by NM, 16Jul2006.) (Revised by Mario Carneiro,
10Jan2015.)



Theorem  unitg 11930 
The topology generated by a basis is a topology on .
Importantly, this theorem means that we don't have to specify separately
the base set for the topological space generated by a basis. In other
words, any member of the class completely specifies the
basis it corresponds to. (Contributed by NM, 16Jul2006.) (Proof
shortened by OpenAI, 30Mar2020.)



Theorem  tgss 11931 
Subset relation for generated topologies. (Contributed by NM,
7May2007.)



Theorem  tgcl 11932 
Show that a basis generates a topology. Remark in [Munkres] p. 79.
(Contributed by NM, 17Jul2006.)



Theorem  tgclb 11933 
The property tgcl 11932 can be reversed: if the topology generated
by
is actually a topology, then must be a topological basis. This
yields an alternative definition of . (Contributed by
Mario Carneiro, 2Sep2015.)



Theorem  tgtopon 11934 
A basis generates a topology on .
(Contributed by Mario
Carneiro, 14Aug2015.)

TopOn 

Theorem  topbas 11935 
A topology is its own basis. (Contributed by NM, 17Jul2006.)



Theorem  tgtop 11936 
A topology is its own basis. (Contributed by NM, 18Jul2006.)



Theorem  eltop 11937 
Membership in a topology, expressed without quantifiers. (Contributed
by NM, 19Jul2006.)



Theorem  eltop2 11938* 
Membership in a topology. (Contributed by NM, 19Jul2006.)



Theorem  eltop3 11939* 
Membership in a topology. (Contributed by NM, 19Jul2006.)



Theorem  tgdom 11940 
A space has no more open sets than subsets of a basis. (Contributed by
Stefan O'Rear, 22Feb2015.) (Revised by Mario Carneiro,
9Apr2015.)



Theorem  tgiun 11941* 
The indexed union of a set of basic open sets is in the generated
topology. (Contributed by Mario Carneiro, 2Sep2015.)



Theorem  tgidm 11942 
The topology generator function is idempotent. (Contributed by NM,
18Jul2006.) (Revised by Mario Carneiro, 2Sep2015.)



Theorem  bastop 11943 
Two ways to express that a basis is a topology. (Contributed by NM,
18Jul2006.)



Theorem  tgtop11 11944 
The topology generation function is onetoone when applied to completed
topologies. (Contributed by NM, 18Jul2006.)



Theorem  en1top 11945 
is the only topology
with one element. (Contributed by FL,
18Aug2008.)



Theorem  tgss3 11946 
A criterion for determining whether one topology is finer than another.
Lemma 2.2 of [Munkres] p. 80 using
abbreviations. (Contributed by NM,
20Jul2006.) (Proof shortened by Mario Carneiro, 2Sep2015.)



Theorem  tgss2 11947* 
A criterion for determining whether one topology is finer than another,
based on a comparison of their bases. Lemma 2.2 of [Munkres] p. 80.
(Contributed by NM, 20Jul2006.) (Proof shortened by Mario Carneiro,
2Sep2015.)



Theorem  basgen 11948 
Given a topology ,
show that a subset
satisfying the third
antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81 using
abbreviations. (Contributed by NM, 22Jul2006.) (Revised by Mario
Carneiro, 2Sep2015.)



Theorem  basgen2 11949* 
Given a topology ,
show that a subset
satisfying the third
antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81.
(Contributed by NM, 20Jul2006.) (Proof shortened by Mario Carneiro,
2Sep2015.)



Theorem  2basgeng 11950 
Conditions that determine the equality of two generated topologies.
(Contributed by NM, 8May2007.) (Revised by Jim Kingdon,
5Mar2023.)



Theorem  bastop1 11951* 
A subset of a topology is a basis for the topology iff every member of
the topology is a union of members of the basis. We use the
idiom " " to express
" is a basis for
topology
" since we do not have a separate notation for this.
Definition 15.35 of [Schechter] p.
428. (Contributed by NM,
2Feb2008.) (Proof shortened by Mario Carneiro, 2Sep2015.)



Theorem  bastop2 11952* 
A version of bastop1 11951 that doesn't have in the antecedent.
(Contributed by NM, 3Feb2008.)



6.1.3 Examples of topologies


Theorem  distop 11953 
The discrete topology on a set . Part of Example 2 in [Munkres]
p. 77. (Contributed by FL, 17Jul2006.) (Revised by Mario Carneiro,
19Mar2015.)



Theorem  topnex 11954 
The class of all topologies is a proper class. The proof uses
discrete topologies and pwnex 4299. (Contributed by BJ, 2May2021.)



Theorem  distopon 11955 
The discrete topology on a set , with base set. (Contributed by
Mario Carneiro, 13Aug2015.)

TopOn 

Theorem  sn0topon 11956 
The singleton of the empty set is a topology on the empty set.
(Contributed by Mario Carneiro, 13Aug2015.)

TopOn 

Theorem  sn0top 11957 
The singleton of the empty set is a topology. (Contributed by Stefan
Allan, 3Mar2006.) (Proof shortened by Mario Carneiro,
13Aug2015.)



Theorem  epttop 11958* 
The excluded point topology. (Contributed by Mario Carneiro,
3Sep2015.)

TopOn 

Theorem  distps 11959 
The discrete topology on a set expressed as a topological space.
(Contributed by FL, 20Aug2006.)

TopSet 

6.1.4 Closure and interior


Syntax  ccld 11960 
Extend class notation with the set of closed sets of a topology.



Syntax  cnt 11961 
Extend class notation with interior of a subset of a topology base set.



Syntax  ccl 11962 
Extend class notation with closure of a subset of a topology base set.



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



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



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



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



Theorem  cldval 11967* 
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.)



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



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



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



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



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



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



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



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



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



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



Theorem  ntrval 11978 
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.)



Theorem  clsval 11979* 
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.)



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



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



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



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



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



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



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



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



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



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



Theorem  ssntr 11990 
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 11991 
The interior of a subset of a topological space is included in the
space. (Contributed by NM, 1Oct2007.)



Theorem  ntrin 11992 
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 11993 
A subset is open iff it equals its own interior. (Contributed by NM,
9Oct2006.) (Revised by Mario Carneiro, 11Nov2013.)



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



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



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



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



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



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



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

