Type  Label  Description 
Statement 

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

TopSet
TopOn 

Theorem  eltpsi 11802 
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 11803 
Syntax for the class of topological bases.



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  eltg4i 11818 
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 11819 
The union of a set of basic open sets is in the generated topology.
(Contributed by Mario Carneiro, 30Aug2015.)



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



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



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



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



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



Theorem  unitg 11825 
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 11826 
Subset relation for generated topologies. (Contributed by NM,
7May2007.)



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



Theorem  tgclb 11828 
The property tgcl 11827 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 11829 
A basis generates a topology on .
(Contributed by Mario
Carneiro, 14Aug2015.)

TopOn 

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



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



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



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



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



Theorem  tgdom 11835 
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 11836* 
The indexed union of a set of basic open sets is in the generated
topology. (Contributed by Mario Carneiro, 2Sep2015.)



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



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



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



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



Theorem  tgss3 11841 
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 11842* 
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 11843 
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 11844* 
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 11845 
Conditions that determine the equality of two generated topologies.
(Contributed by NM, 8May2007.) (Revised by Jim Kingdon,
5Mar2023.)



Theorem  bastop1 11846* 
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 11847* 
A version of bastop1 11846 that doesn't have in the antecedent.
(Contributed by NM, 3Feb2008.)



6.1.3 Examples of topologies


Theorem  distop 11848 
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 11849 
The class of all topologies is a proper class. The proof uses
discrete topologies and pwnex 4286. (Contributed by BJ, 2May2021.)



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

TopOn 

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

TopOn 

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



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

TopOn 

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

TopSet 

6.1.4 Closure and interior


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



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



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



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



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



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



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



Theorem  cldval 11862* 
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 11863* 
The interior function on the subsets of a topology's base set.
(Contributed by NM, 10Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)



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



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



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



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



Theorem  cldss 11868 
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 11869 
The set of closed sets is contained in the powerset of the base.
(Contributed by Mario Carneiro, 6Jan2014.)



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



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



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



Theorem  ntrval 11873 
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 11874* 
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 11875 
The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93.
(Contributed by NM, 4Oct2006.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  discld 11899 
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 11900 
The closed sets of the topology .
(Contributed by FL,
5Jan2009.)

