Theorem List for Intuitionistic Logic Explorer - 12101-12200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 0ntop 12101 |
The empty set is not a topology. (Contributed by FL, 1-Jun-2008.)
|
⊢ ¬ ∅ ∈ Top |
|
Theorem | topopn 12102 |
The underlying set of a topology is an open set. (Contributed by NM,
17-Jul-2006.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
|
Theorem | eltopss 12103 |
A member of a topology is a subset of its underlying set. (Contributed
by NM, 12-Sep-2006.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) |
|
7.1.1.2 Topologies on sets
|
|
Syntax | ctopon 12104 |
Syntax for the function of topologies on sets.
|
class TopOn |
|
Definition | df-topon 12105* |
Define the function that associates with a set the set of topologies on
it. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|
⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗}) |
|
Theorem | funtopon 12106 |
The class TopOn is a function. (Contributed by BJ,
29-Apr-2021.)
|
⊢ Fun TopOn |
|
Theorem | istopon 12107 |
Property of being a topology with a given base set. (Contributed by
Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro,
13-Aug-2015.)
|
⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) |
|
Theorem | topontop 12108 |
A topology on a given base set is a topology. (Contributed by Mario
Carneiro, 13-Aug-2015.)
|
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) |
|
Theorem | toponuni 12109 |
The base set of a topology on a given base set. (Contributed by Mario
Carneiro, 13-Aug-2015.)
|
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
|
Theorem | topontopi 12110 |
A topology on a given base set is a topology. (Contributed by Mario
Carneiro, 13-Aug-2015.)
|
⊢ 𝐽 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐽 ∈ Top |
|
Theorem | toponunii 12111 |
The base set of a topology on a given base set. (Contributed by Mario
Carneiro, 13-Aug-2015.)
|
⊢ 𝐽 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐵 = ∪ 𝐽 |
|
Theorem | toptopon 12112 |
Alternative definition of Top in terms of TopOn. (Contributed
by Mario Carneiro, 13-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
|
Theorem | toptopon2 12113 |
A topology is the same thing as a topology on the union of its open sets.
(Contributed by BJ, 27-Apr-2021.)
|
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
|
Theorem | topontopon 12114 |
A topology on a set is a topology on the union of its open sets.
(Contributed by BJ, 27-Apr-2021.)
|
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
|
Theorem | toponrestid 12115 |
Given a topology on a set, restricting it to that same set has no
effect. (Contributed by Jim Kingdon, 6-Jul-2022.)
|
⊢ 𝐴 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐴 = (𝐴 ↾t 𝐵) |
|
Theorem | toponsspwpwg 12116 |
The set of topologies on a set is included in the double power set of
that set. (Contributed by BJ, 29-Apr-2021.) (Revised by Jim Kingdon,
16-Jan-2023.)
|
⊢ (𝐴 ∈ 𝑉 → (TopOn‘𝐴) ⊆ 𝒫 𝒫 𝐴) |
|
Theorem | dmtopon 12117 |
The domain of TopOn is V.
(Contributed by BJ,
29-Apr-2021.)
|
⊢ dom TopOn = V |
|
Theorem | fntopon 12118 |
The class TopOn is a function with domain V. (Contributed by
BJ, 29-Apr-2021.)
|
⊢ TopOn Fn V |
|
Theorem | toponmax 12119 |
The base set of a topology is an open set. (Contributed by Mario
Carneiro, 13-Aug-2015.)
|
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽) |
|
Theorem | toponss 12120 |
A member of a topology is a subset of its underlying set. (Contributed by
Mario Carneiro, 21-Aug-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) |
|
Theorem | toponcom 12121 |
If 𝐾 is a topology on the base set of
topology 𝐽, then 𝐽 is a
topology on the base of 𝐾. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ (TopOn‘∪ 𝐽))
→ 𝐽 ∈
(TopOn‘∪ 𝐾)) |
|
Theorem | toponcomb 12122 |
Biconditional form of toponcom 12121. (Contributed by BJ, 5-Dec-2021.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ∈ (TopOn‘∪ 𝐾)
↔ 𝐾 ∈
(TopOn‘∪ 𝐽))) |
|
Theorem | topgele 12123 |
The topologies over the same set have the greatest element (the discrete
topology) and the least element (the indiscrete topology). (Contributed
by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 16-Sep-2015.)
|
⊢ (𝐽 ∈ (TopOn‘𝑋) → ({∅, 𝑋} ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋)) |
|
7.1.1.3 Topological spaces
|
|
Syntax | ctps 12124 |
Syntax for the class of topological spaces.
|
class TopSp |
|
Definition | df-topsp 12125 |
Define the class of topological spaces (as extensible structures).
(Contributed by Stefan O'Rear, 13-Aug-2015.)
|
⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} |
|
Theorem | istps 12126 |
Express the predicate "is a topological space." (Contributed by
Mario
Carneiro, 13-Aug-2015.)
|
⊢ 𝐴 = (Base‘𝐾)
& ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴)) |
|
Theorem | istps2 12127 |
Express the predicate "is a topological space." (Contributed by NM,
20-Oct-2012.)
|
⊢ 𝐴 = (Base‘𝐾)
& ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp ↔ (𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽)) |
|
Theorem | tpsuni 12128 |
The base set of a topological space. (Contributed by FL,
27-Jun-2014.)
|
⊢ 𝐴 = (Base‘𝐾)
& ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp → 𝐴 = ∪ 𝐽) |
|
Theorem | tpstop 12129 |
The topology extractor on a topological space is a topology.
(Contributed by FL, 27-Jun-2014.)
|
⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp → 𝐽 ∈ Top) |
|
Theorem | tpspropd 12130 |
A topological space depends only on the base and topology components.
(Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro,
13-Aug-2015.)
|
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp)) |
|
Theorem | topontopn 12131 |
Express the predicate "is a topological space." (Contributed by
Mario
Carneiro, 13-Aug-2015.)
|
⊢ 𝐴 = (Base‘𝐾)
& ⊢ 𝐽 = (TopSet‘𝐾) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾)) |
|
Theorem | tsettps 12132 |
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,
13-Aug-2015.)
|
⊢ 𝐴 = (Base‘𝐾)
& ⊢ 𝐽 = (TopSet‘𝐾) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) |
|
Theorem | istpsi 12133 |
Properties that determine a topological space. (Contributed by NM,
20-Oct-2012.)
|
⊢ (Base‘𝐾) = 𝐴
& ⊢ (TopOpen‘𝐾) = 𝐽
& ⊢ 𝐴 = ∪ 𝐽 & ⊢ 𝐽 ∈
Top ⇒ ⊢ 𝐾 ∈ TopSp |
|
Theorem | eltpsg 12134 |
Properties that determine a topological space from a construction (using
no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.)
|
⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉,
〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) |
|
Theorem | eltpsi 12135 |
Properties that determine a topological space from a construction (using
no explicit indices). (Contributed by NM, 20-Oct-2012.) (Revised by
Mario Carneiro, 13-Aug-2015.)
|
⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉,
〈(TopSet‘ndx), 𝐽〉} & ⊢ 𝐴 = ∪
𝐽 & ⊢ 𝐽 ∈
Top ⇒ ⊢ 𝐾 ∈ TopSp |
|
7.1.2 Topological bases
|
|
Syntax | ctb 12136 |
Syntax for the class of topological bases.
|
class TopBases |
|
Definition | df-bases 12137* |
Define the class of topological bases. Equivalent to definition of
basis in [Munkres] p. 78 (see isbasis2g 12139). Note that "bases" is the
plural of "basis". (Contributed by NM, 17-Jul-2006.)
|
⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪
(𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))} |
|
Theorem | isbasisg 12138* |
Express the predicate "the set 𝐵 is a basis for a topology".
(Contributed by NM, 17-Jul-2006.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪
(𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
|
Theorem | isbasis2g 12139* |
Express the predicate "the set 𝐵 is a basis for a topology".
(Contributed by NM, 17-Jul-2006.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦)))) |
|
Theorem | isbasis3g 12140* |
Express the predicate "the set 𝐵 is a basis for a topology".
Definition of basis in [Munkres] p. 78.
(Contributed by NM,
17-Jul-2006.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ (∀𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝐵∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦))))) |
|
Theorem | basis1 12141 |
Property of a basis. (Contributed by NM, 16-Jul-2006.)
|
⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪
(𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷))) |
|
Theorem | basis2 12142* |
Property of a basis. (Contributed by NM, 17-Jul-2006.)
|
⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷))) |
|
Theorem | fiinbas 12143* |
If a set is closed under finite intersection, then it is a basis for a
topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) → 𝐵 ∈ TopBases) |
|
Theorem | baspartn 12144* |
A disjoint system of sets is a basis for a topology. (Contributed by
Stefan O'Rear, 22-Feb-2015.)
|
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases) |
|
Theorem | tgval 12145* |
The topology generated by a basis. See also tgval2 12147 and tgval3 12154.
(Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro,
10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)}) |
|
Theorem | tgvalex 12146 |
The topology generated by a basis is a set. (Contributed by Jim
Kingdon, 4-Mar-2023.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ∈ V) |
|
Theorem | tgval2 12147* |
Definition of a topology generated by a basis in [Munkres] p. 78. Later
we show (in tgcl 12160) that (topGen‘𝐵) is indeed a topology
(on
∪ 𝐵, see unitg 12158). See also tgval 12145 and tgval3 12154. (Contributed
by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))}) |
|
Theorem | eltg 12148 |
Membership in a topology generated by a basis. (Contributed by NM,
16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪
(𝐵 ∩ 𝒫 𝐴))) |
|
Theorem | eltg2 12149* |
Membership in a topology generated by a basis. (Contributed by NM,
15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))) |
|
Theorem | eltg2b 12150* |
Membership in a topology generated by a basis. (Contributed by Mario
Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) |
|
Theorem | eltg4i 12151 |
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,
22-Feb-2015.)
|
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 = ∪ (𝐵 ∩ 𝒫 𝐴)) |
|
Theorem | eltg3i 12152 |
The union of a set of basic open sets is in the generated topology.
(Contributed by Mario Carneiro, 30-Aug-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵)) |
|
Theorem | eltg3 12153* |
Membership in a topology generated by a basis. (Contributed by NM,
15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥))) |
|
Theorem | tgval3 12154* |
Alternate expression for the topology generated by a basis. Lemma 2.1
of [Munkres] p. 80. See also tgval 12145 and tgval2 12147. (Contributed by
NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)}) |
|
Theorem | tg1 12155 |
Property of a member of a topology generated by a basis. (Contributed
by NM, 20-Jul-2006.)
|
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | tg2 12156* |
Property of a member of a topology generated by a basis. (Contributed
by NM, 20-Jul-2006.)
|
⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) |
|
Theorem | bastg 12157 |
A member of a basis is a subset of the topology it generates.
(Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro,
10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵)) |
|
Theorem | unitg 12158 |
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 TopBases
completely specifies the
basis it corresponds to. (Contributed by NM, 16-Jul-2006.) (Proof
shortened by OpenAI, 30-Mar-2020.)
|
⊢ (𝐵 ∈ 𝑉 → ∪
(topGen‘𝐵) = ∪ 𝐵) |
|
Theorem | tgss 12159 |
Subset relation for generated topologies. (Contributed by NM,
7-May-2007.)
|
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶)) |
|
Theorem | tgcl 12160 |
Show that a basis generates a topology. Remark in [Munkres] p. 79.
(Contributed by NM, 17-Jul-2006.)
|
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top) |
|
Theorem | tgclb 12161 |
The property tgcl 12160 can be reversed: if the topology generated
by 𝐵
is actually a topology, then 𝐵 must be a topological basis. This
yields an alternative definition of TopBases.
(Contributed by
Mario Carneiro, 2-Sep-2015.)
|
⊢ (𝐵 ∈ TopBases ↔ (topGen‘𝐵) ∈ Top) |
|
Theorem | tgtopon 12162 |
A basis generates a topology on ∪
𝐵. (Contributed by
Mario
Carneiro, 14-Aug-2015.)
|
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵)) |
|
Theorem | topbas 12163 |
A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
|
⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases) |
|
Theorem | tgtop 12164 |
A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
|
⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽) |
|
Theorem | eltop 12165 |
Membership in a topology, expressed without quantifiers. (Contributed
by NM, 19-Jul-2006.)
|
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪
(𝐽 ∩ 𝒫 𝐴))) |
|
Theorem | eltop2 12166* |
Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) |
|
Theorem | eltop3 12167* |
Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥))) |
|
Theorem | tgdom 12168 |
A space has no more open sets than subsets of a basis. (Contributed by
Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro,
9-Apr-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ≼ 𝒫 𝐵) |
|
Theorem | tgiun 12169* |
The indexed union of a set of basic open sets is in the generated
topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) → ∪ 𝑥 ∈ 𝐴 𝐶 ∈ (topGen‘𝐵)) |
|
Theorem | tgidm 12170 |
The topology generator function is idempotent. (Contributed by NM,
18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵)) |
|
Theorem | bastop 12171 |
Two ways to express that a basis is a topology. (Contributed by NM,
18-Jul-2006.)
|
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵)) |
|
Theorem | tgtop11 12172 |
The topology generation function is one-to-one when applied to completed
topologies. (Contributed by NM, 18-Jul-2006.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾) |
|
Theorem | en1top 12173 |
{∅} is the only topology with one element.
(Contributed by FL,
18-Aug-2008.)
|
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅})) |
|
Theorem | tgss3 12174 |
A criterion for determining whether one topology is finer than another.
Lemma 2.2 of [Munkres] p. 80 using
abbreviations. (Contributed by NM,
20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((topGen‘𝐵) ⊆ (topGen‘𝐶) ↔ 𝐵 ⊆ (topGen‘𝐶))) |
|
Theorem | tgss2 12175* |
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, 20-Jul-2006.) (Proof shortened by Mario Carneiro,
2-Sep-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪
𝐶) →
((topGen‘𝐵) ⊆
(topGen‘𝐶) ↔
∀𝑥 ∈ ∪ 𝐵∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝐶 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)))) |
|
Theorem | basgen 12176 |
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, 22-Jul-2006.) (Revised by Mario
Carneiro, 2-Sep-2015.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = 𝐽) |
|
Theorem | basgen2 12177* |
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, 20-Jul-2006.) (Proof shortened by Mario Carneiro,
2-Sep-2015.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) → (topGen‘𝐵) = 𝐽) |
|
Theorem | 2basgeng 12178 |
Conditions that determine the equality of two generated topologies.
(Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon,
5-Mar-2023.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = (topGen‘𝐶)) |
|
Theorem | bastop1 12179* |
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 "(topGen‘𝐵) = 𝐽 " 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,
2-Feb-2008.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽) → ((topGen‘𝐵) = 𝐽 ↔ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) |
|
Theorem | bastop2 12180* |
A version of bastop1 12179 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent.
(Contributed by NM, 3-Feb-2008.)
|
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)))) |
|
7.1.3 Examples of topologies
|
|
Theorem | distop 12181 |
The discrete topology on a set 𝐴. Part of Example 2 in [Munkres]
p. 77. (Contributed by FL, 17-Jul-2006.) (Revised by Mario Carneiro,
19-Mar-2015.)
|
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) |
|
Theorem | topnex 12182 |
The class of all topologies is a proper class. The proof uses
discrete topologies and pwnex 4340. (Contributed by BJ, 2-May-2021.)
|
⊢ Top ∉ V |
|
Theorem | distopon 12183 |
The discrete topology on a set 𝐴, with base set. (Contributed by
Mario Carneiro, 13-Aug-2015.)
|
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) |
|
Theorem | sn0topon 12184 |
The singleton of the empty set is a topology on the empty set.
(Contributed by Mario Carneiro, 13-Aug-2015.)
|
⊢ {∅} ∈
(TopOn‘∅) |
|
Theorem | sn0top 12185 |
The singleton of the empty set is a topology. (Contributed by Stefan
Allan, 3-Mar-2006.) (Proof shortened by Mario Carneiro,
13-Aug-2015.)
|
⊢ {∅} ∈ Top |
|
Theorem | epttop 12186* |
The excluded point topology. (Contributed by Mario Carneiro,
3-Sep-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴)) |
|
Theorem | distps 12187 |
The discrete topology on a set 𝐴 expressed as a topological space.
(Contributed by FL, 20-Aug-2006.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx),
𝐴〉,
〈(TopSet‘ndx), 𝒫 𝐴〉} ⇒ ⊢ 𝐾 ∈ TopSp |
|
7.1.4 Closure and interior
|
|
Syntax | ccld 12188 |
Extend class notation with the set of closed sets of a topology.
|
class Clsd |
|
Syntax | cnt 12189 |
Extend class notation with interior of a subset of a topology base set.
|
class int |
|
Syntax | ccl 12190 |
Extend class notation with closure of a subset of a topology base set.
|
class cls |
|
Definition | df-cld 12191* |
Define a function on topologies whose value is the set of closed sets of
the topology. (Contributed by NM, 2-Oct-2006.)
|
⊢ Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗
∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗}) |
|
Definition | df-ntr 12192* |
Define a function on topologies whose value is the interior function on
the subsets of the base set. See ntrval 12206. (Contributed by NM,
10-Sep-2006.)
|
⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∪ (𝑗 ∩ 𝒫 𝑥))) |
|
Definition | df-cls 12193* |
Define a function on topologies whose value is the closure function on
the subsets of the base set. See clsval 12207. (Contributed by NM,
3-Oct-2006.)
|
⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) |
|
Theorem | fncld 12194 |
The closed-set generator is a well-behaved function. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
⊢ Clsd Fn Top |
|
Theorem | cldval 12195* |
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, 2-Oct-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ 𝐽}) |
|
Theorem | ntrfval 12196* |
The interior function on the subsets of a topology's base set.
(Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (int‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∪
(𝐽 ∩ 𝒫 𝑥))) |
|
Theorem | clsfval 12197* |
The closure function on the subsets of a topology's base set.
(Contributed by NM, 3-Oct-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (cls‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∩
{𝑦 ∈
(Clsd‘𝐽) ∣
𝑥 ⊆ 𝑦})) |
|
Theorem | cldrcl 12198 |
Reverse closure of the closed set operation. (Contributed by Stefan
O'Rear, 22-Feb-2015.)
|
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
|
Theorem | iscld 12199 |
The predicate "the class 𝑆 is a closed set". (Contributed
by NM,
2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽))) |
|
Theorem | iscld2 12200 |
A subset of the underlying set of a topology is closed iff its
complement is open. (Contributed by NM, 4-Oct-2006.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑆) ∈ 𝐽)) |