HomeHome Intuitionistic Logic Explorer
Theorem List (p. 122 of 132)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 12101-12200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem0ntop 12101 The empty set is not a topology. (Contributed by FL, 1-Jun-2008.)
¬ ∅ ∈ Top
 
Theoremtopopn 12102 The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
𝑋 = 𝐽       (𝐽 ∈ Top → 𝑋𝐽)
 
Theoremeltopss 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
 
Syntaxctopon 12104 Syntax for the function of topologies on sets.
class TopOn
 
Definitiondf-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 ∣ 𝑏 = 𝑗})
 
Theoremfuntopon 12106 The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.)
Fun TopOn
 
Theoremistopon 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 ∧ 𝐵 = 𝐽))
 
Theoremtopontop 12108 A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
(𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
 
Theoremtoponuni 12109 The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
(𝐽 ∈ (TopOn‘𝐵) → 𝐵 = 𝐽)
 
Theoremtopontopi 12110 A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
𝐽 ∈ (TopOn‘𝐵)       𝐽 ∈ Top
 
Theoremtoponunii 12111 The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
𝐽 ∈ (TopOn‘𝐵)       𝐵 = 𝐽
 
Theoremtoptopon 12112 Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)
𝑋 = 𝐽       (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
 
Theoremtoptopon2 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‘ 𝐽))
 
Theoremtopontopon 12114 A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
(𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ (TopOn‘ 𝐽))
 
Theoremtoponrestid 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 𝐵)
 
Theoremtoponsspwpwg 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‘𝐴) ⊆ 𝒫 𝒫 𝐴)
 
Theoremdmtopon 12117 The domain of TopOn is V. (Contributed by BJ, 29-Apr-2021.)
dom TopOn = V
 
Theoremfntopon 12118 The class TopOn is a function with domain V. (Contributed by BJ, 29-Apr-2021.)
TopOn Fn V
 
Theoremtoponmax 12119 The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.)
(𝐽 ∈ (TopOn‘𝐵) → 𝐵𝐽)
 
Theoremtoponss 12120 A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.)
((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴𝐽) → 𝐴𝑋)
 
Theoremtoponcom 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‘ 𝐾))
 
Theoremtoponcomb 12122 Biconditional form of toponcom 12121. (Contributed by BJ, 5-Dec-2021.)
((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ∈ (TopOn‘ 𝐾) ↔ 𝐾 ∈ (TopOn‘ 𝐽)))
 
Theoremtopgele 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
 
Syntaxctps 12124 Syntax for the class of topological spaces.
class TopSp
 
Definitiondf-topsp 12125 Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
 
Theoremistps 12126 Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
𝐴 = (Base‘𝐾)    &   𝐽 = (TopOpen‘𝐾)       (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴))
 
Theoremistps2 12127 Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.)
𝐴 = (Base‘𝐾)    &   𝐽 = (TopOpen‘𝐾)       (𝐾 ∈ TopSp ↔ (𝐽 ∈ Top ∧ 𝐴 = 𝐽))
 
Theoremtpsuni 12128 The base set of a topological space. (Contributed by FL, 27-Jun-2014.)
𝐴 = (Base‘𝐾)    &   𝐽 = (TopOpen‘𝐾)       (𝐾 ∈ TopSp → 𝐴 = 𝐽)
 
Theoremtpstop 12129 The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.)
𝐽 = (TopOpen‘𝐾)       (𝐾 ∈ TopSp → 𝐽 ∈ Top)
 
Theoremtpspropd 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))
 
Theoremtopontopn 12131 Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
𝐴 = (Base‘𝐾)    &   𝐽 = (TopSet‘𝐾)       (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾))
 
Theoremtsettps 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)
 
Theoremistpsi 12133 Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
(Base‘𝐾) = 𝐴    &   (TopOpen‘𝐾) = 𝐽    &   𝐴 = 𝐽    &   𝐽 ∈ Top       𝐾 ∈ TopSp
 
Theoremeltpsg 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)
 
Theoremeltpsi 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
 
Syntaxctb 12136 Syntax for the class of topological bases.
class TopBases
 
Definitiondf-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 = {𝑥 ∣ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ⊆ (𝑥 ∩ 𝒫 (𝑦𝑧))}
 
Theoremisbasisg 12138* Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
(𝐵𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥𝐵𝑦𝐵 (𝑥𝑦) ⊆ (𝐵 ∩ 𝒫 (𝑥𝑦))))
 
Theoremisbasis2g 12139* Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
(𝐵𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥𝐵𝑦𝐵𝑧 ∈ (𝑥𝑦)∃𝑤𝐵 (𝑧𝑤𝑤 ⊆ (𝑥𝑦))))
 
Theoremisbasis3g 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 ↔ (∀𝑥𝐵 𝑥 𝐵 ∧ ∀𝑥 𝐵𝑦𝐵 𝑥𝑦 ∧ ∀𝑥𝐵𝑦𝐵𝑧 ∈ (𝑥𝑦)∃𝑤𝐵 (𝑧𝑤𝑤 ⊆ (𝑥𝑦)))))
 
Theorembasis1 12141 Property of a basis. (Contributed by NM, 16-Jul-2006.)
((𝐵 ∈ TopBases ∧ 𝐶𝐵𝐷𝐵) → (𝐶𝐷) ⊆ (𝐵 ∩ 𝒫 (𝐶𝐷)))
 
Theorembasis2 12142* Property of a basis. (Contributed by NM, 17-Jul-2006.)
(((𝐵 ∈ TopBases ∧ 𝐶𝐵) ∧ (𝐷𝐵𝐴 ∈ (𝐶𝐷))) → ∃𝑥𝐵 (𝐴𝑥𝑥 ⊆ (𝐶𝐷)))
 
Theoremfiinbas 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)
 
Theorembaspartn 12144* A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
((𝑃𝑉 ∧ ∀𝑥𝑃𝑦𝑃 (𝑥 = 𝑦 ∨ (𝑥𝑦) = ∅)) → 𝑃 ∈ TopBases)
 
Theoremtgval 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‘𝐵) = {𝑥𝑥 (𝐵 ∩ 𝒫 𝑥)})
 
Theoremtgvalex 12146 The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.)
(𝐵𝑉 → (topGen‘𝐵) ∈ V)
 
Theoremtgval2 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‘𝐵) = {𝑥 ∣ (𝑥 𝐵 ∧ ∀𝑦𝑥𝑧𝐵 (𝑦𝑧𝑧𝑥))})
 
Theoremeltg 12148 Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 (𝐵 ∩ 𝒫 𝐴)))
 
Theoremeltg2 12149* Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 (𝑥𝑦𝑦𝐴))))
 
Theoremeltg2b 12150* Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥𝑦𝑦𝐴)))
 
Theoremeltg4i 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‘𝐵) → 𝐴 = (𝐵 ∩ 𝒫 𝐴))
 
Theoremeltg3i 12152 The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
((𝐵𝑉𝐴𝐵) → 𝐴 ∈ (topGen‘𝐵))
 
Theoremeltg3 12153* Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥𝐵𝐴 = 𝑥)))
 
Theoremtgval3 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‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦𝐵𝑥 = 𝑦)})
 
Theoremtg1 12155 Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
(𝐴 ∈ (topGen‘𝐵) → 𝐴 𝐵)
 
Theoremtg2 12156* Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶𝐴) → ∃𝑥𝐵 (𝐶𝑥𝑥𝐴))
 
Theorembastg 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‘𝐵))
 
Theoremunitg 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‘𝐵) = 𝐵)
 
Theoremtgss 12159 Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
((𝐶𝑉𝐵𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶))
 
Theoremtgcl 12160 Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
(𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
 
Theoremtgclb 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)
 
Theoremtgtopon 12162 A basis generates a topology on 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.)
(𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘ 𝐵))
 
Theoremtopbas 12163 A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
(𝐽 ∈ Top → 𝐽 ∈ TopBases)
 
Theoremtgtop 12164 A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
(𝐽 ∈ Top → (topGen‘𝐽) = 𝐽)
 
Theoremeltop 12165 Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
(𝐽 ∈ Top → (𝐴𝐽𝐴 (𝐽 ∩ 𝒫 𝐴)))
 
Theoremeltop2 12166* Membership in a topology. (Contributed by NM, 19-Jul-2006.)
(𝐽 ∈ Top → (𝐴𝐽 ↔ ∀𝑥𝐴𝑦𝐽 (𝑥𝑦𝑦𝐴)))
 
Theoremeltop3 12167* Membership in a topology. (Contributed by NM, 19-Jul-2006.)
(𝐽 ∈ Top → (𝐴𝐽 ↔ ∃𝑥(𝑥𝐽𝐴 = 𝑥)))
 
Theoremtgdom 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‘𝐵) ≼ 𝒫 𝐵)
 
Theoremtgiun 12169* The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
((𝐵𝑉 ∧ ∀𝑥𝐴 𝐶𝐵) → 𝑥𝐴 𝐶 ∈ (topGen‘𝐵))
 
Theoremtgidm 12170 The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
(𝐵𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵))
 
Theorembastop 12171 Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
(𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵))
 
Theoremtgtop11 12172 The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.)
((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾)
 
Theoremen1top 12173 {∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
(𝐽 ∈ Top → (𝐽 ≈ 1o𝐽 = {∅}))
 
Theoremtgss3 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‘𝐶)))
 
Theoremtgss2 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‘𝐶) ↔ ∀𝑥 𝐵𝑦𝐵 (𝑥𝑦 → ∃𝑧𝐶 (𝑥𝑧𝑧𝑦))))
 
Theorembasgen 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‘𝐵) = 𝐽)
 
Theorembasgen2 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‘𝐵) = 𝐽)
 
Theorem2basgeng 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‘𝐶))
 
Theorembastop1 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‘𝐵) = 𝐽 ↔ ∀𝑥𝐽𝑦(𝑦𝐵𝑥 = 𝑦)))
 
Theorembastop2 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
 
Theoremdistop 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)
 
Theoremtopnex 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
 
Theoremdistopon 12183 The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
(𝐴𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))
 
Theoremsn0topon 12184 The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
{∅} ∈ (TopOn‘∅)
 
Theoremsn0top 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
 
Theoremepttop 12186* The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ (TopOn‘𝐴))
 
Theoremdistps 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
 
Syntaxccld 12188 Extend class notation with the set of closed sets of a topology.
class Clsd
 
Syntaxcnt 12189 Extend class notation with interior of a subset of a topology base set.
class int
 
Syntaxccl 12190 Extend class notation with closure of a subset of a topology base set.
class cls
 
Definitiondf-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 ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
 
Definitiondf-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 ↦ (𝑥 ∈ 𝒫 𝑗 (𝑗 ∩ 𝒫 𝑥)))
 
Definitiondf-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‘𝑗) ∣ 𝑥𝑦}))
 
Theoremfncld 12194 The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Clsd Fn Top
 
Theoremcldval 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‘𝐽) = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑥) ∈ 𝐽})
 
Theoremntrfval 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‘𝐽) = (𝑥 ∈ 𝒫 𝑋 (𝐽 ∩ 𝒫 𝑥)))
 
Theoremclsfval 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‘𝐽) ∣ 𝑥𝑦}))
 
Theoremcldrcl 12198 Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
(𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top)
 
Theoremiscld 12199 The predicate "the class 𝑆 is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆𝑋 ∧ (𝑋𝑆) ∈ 𝐽)))
 
Theoremiscld2 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‘𝐽) ↔ (𝑋𝑆) ∈ 𝐽))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13177
  Copyright terms: Public domain < Previous  Next >