HomeHome Intuitionistic Logic Explorer
Theorem List (p. 133 of 145)
< 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 - 13201-13300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremtpspropd 13201 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 13202 Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.)
𝐴 = (Base‘𝐾)    &   𝐽 = (TopSet‘𝐾)       (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾))
 
Theoremtsettps 13203 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 13204 Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
(Base‘𝐾) = 𝐴    &   (TopOpen‘𝐾) = 𝐽    &   𝐴 = 𝐽    &   𝐽 ∈ Top       𝐾 ∈ TopSp
 
Theoremeltpsg 13205 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 13206 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
 
8.1.2  Topological bases
 
Syntaxctb 13207 Syntax for the class of topological bases.
class TopBases
 
Definitiondf-bases 13208* Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 13210). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.)
TopBases = {𝑥 ∣ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ⊆ (𝑥 ∩ 𝒫 (𝑦𝑧))}
 
Theoremisbasisg 13209* Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
(𝐵𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥𝐵𝑦𝐵 (𝑥𝑦) ⊆ (𝐵 ∩ 𝒫 (𝑥𝑦))))
 
Theoremisbasis2g 13210* Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
(𝐵𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥𝐵𝑦𝐵𝑧 ∈ (𝑥𝑦)∃𝑤𝐵 (𝑧𝑤𝑤 ⊆ (𝑥𝑦))))
 
Theoremisbasis3g 13211* 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 13212 Property of a basis. (Contributed by NM, 16-Jul-2006.)
((𝐵 ∈ TopBases ∧ 𝐶𝐵𝐷𝐵) → (𝐶𝐷) ⊆ (𝐵 ∩ 𝒫 (𝐶𝐷)))
 
Theorembasis2 13213* Property of a basis. (Contributed by NM, 17-Jul-2006.)
(((𝐵 ∈ TopBases ∧ 𝐶𝐵) ∧ (𝐷𝐵𝐴 ∈ (𝐶𝐷))) → ∃𝑥𝐵 (𝐴𝑥𝑥 ⊆ (𝐶𝐷)))
 
Theoremfiinbas 13214* 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 13215* A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
((𝑃𝑉 ∧ ∀𝑥𝑃𝑦𝑃 (𝑥 = 𝑦 ∨ (𝑥𝑦) = ∅)) → 𝑃 ∈ TopBases)
 
Theoremtgval 13216* The topology generated by a basis. See also tgval2 13218 and tgval3 13225. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (topGen‘𝐵) = {𝑥𝑥 (𝐵 ∩ 𝒫 𝑥)})
 
Theoremtgvalex 13217 The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.)
(𝐵𝑉 → (topGen‘𝐵) ∈ V)
 
Theoremtgval2 13218* Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 13231) that (topGen‘𝐵) is indeed a topology (on 𝐵, see unitg 13229). See also tgval 13216 and tgval3 13225. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 𝐵 ∧ ∀𝑦𝑥𝑧𝐵 (𝑦𝑧𝑧𝑥))})
 
Theoremeltg 13219 Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 (𝐵 ∩ 𝒫 𝐴)))
 
Theoremeltg2 13220* Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 (𝑥𝑦𝑦𝐴))))
 
Theoremeltg2b 13221* Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥𝑦𝑦𝐴)))
 
Theoremeltg4i 13222 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 13223 The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
((𝐵𝑉𝐴𝐵) → 𝐴 ∈ (topGen‘𝐵))
 
Theoremeltg3 13224* Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥𝐵𝐴 = 𝑥)))
 
Theoremtgval3 13225* Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 13216 and tgval2 13218. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
(𝐵𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦𝐵𝑥 = 𝑦)})
 
Theoremtg1 13226 Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
(𝐴 ∈ (topGen‘𝐵) → 𝐴 𝐵)
 
Theoremtg2 13227* Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶𝐴) → ∃𝑥𝐵 (𝐶𝑥𝑥𝐴))
 
Theorembastg 13228 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 13229 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 13230 Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
((𝐶𝑉𝐵𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶))
 
Theoremtgcl 13231 Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
(𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
 
Theoremtgclb 13232 The property tgcl 13231 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 13233 A basis generates a topology on 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.)
(𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘ 𝐵))
 
Theoremtopbas 13234 A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
(𝐽 ∈ Top → 𝐽 ∈ TopBases)
 
Theoremtgtop 13235 A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
(𝐽 ∈ Top → (topGen‘𝐽) = 𝐽)
 
Theoremeltop 13236 Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
(𝐽 ∈ Top → (𝐴𝐽𝐴 (𝐽 ∩ 𝒫 𝐴)))
 
Theoremeltop2 13237* Membership in a topology. (Contributed by NM, 19-Jul-2006.)
(𝐽 ∈ Top → (𝐴𝐽 ↔ ∀𝑥𝐴𝑦𝐽 (𝑥𝑦𝑦𝐴)))
 
Theoremeltop3 13238* Membership in a topology. (Contributed by NM, 19-Jul-2006.)
(𝐽 ∈ Top → (𝐴𝐽 ↔ ∃𝑥(𝑥𝐽𝐴 = 𝑥)))
 
Theoremtgdom 13239 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 13240* The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
((𝐵𝑉 ∧ ∀𝑥𝐴 𝐶𝐵) → 𝑥𝐴 𝐶 ∈ (topGen‘𝐵))
 
Theoremtgidm 13241 The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
(𝐵𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵))
 
Theorembastop 13242 Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
(𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵))
 
Theoremtgtop11 13243 The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.)
((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾)
 
Theoremen1top 13244 {∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
(𝐽 ∈ Top → (𝐽 ≈ 1o𝐽 = {∅}))
 
Theoremtgss3 13245 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 13246* 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 13247 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 13248* 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 13249 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 13250* 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 13251* A version of bastop1 13250 that doesn't have 𝐵𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.)
(𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵𝐽 ∧ ∀𝑥𝐽𝑦(𝑦𝐵𝑥 = 𝑦))))
 
8.1.3  Examples of topologies
 
Theoremdistop 13252 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 13253 The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 4446. (Contributed by BJ, 2-May-2021.)
Top ∉ V
 
Theoremdistopon 13254 The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
(𝐴𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))
 
Theoremsn0topon 13255 The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
{∅} ∈ (TopOn‘∅)
 
Theoremsn0top 13256 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 13257* The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ (TopOn‘𝐴))
 
Theoremdistps 13258 The discrete topology on a set 𝐴 expressed as a topological space. (Contributed by FL, 20-Aug-2006.)
𝐴 ∈ V    &   𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝒫 𝐴⟩}       𝐾 ∈ TopSp
 
8.1.4  Closure and interior
 
Syntaxccld 13259 Extend class notation with the set of closed sets of a topology.
class Clsd
 
Syntaxcnt 13260 Extend class notation with interior of a subset of a topology base set.
class int
 
Syntaxccl 13261 Extend class notation with closure of a subset of a topology base set.
class cls
 
Definitiondf-cld 13262* 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 13263* Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 13277. (Contributed by NM, 10-Sep-2006.)
int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 (𝑗 ∩ 𝒫 𝑥)))
 
Definitiondf-cls 13264* Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 13278. (Contributed by NM, 3-Oct-2006.)
cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦}))
 
Theoremfncld 13265 The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Clsd Fn Top
 
Theoremcldval 13266* 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 13267* 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 13268* 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 13269 Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
(𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top)
 
Theoremiscld 13270 The predicate "the class 𝑆 is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆𝑋 ∧ (𝑋𝑆) ∈ 𝐽)))
 
Theoremiscld2 13271 A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑋𝑆) ∈ 𝐽))
 
Theoremcldss 13272 A closed set is a subset of the underlying set of a topology. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
𝑋 = 𝐽       (𝑆 ∈ (Clsd‘𝐽) → 𝑆𝑋)
 
Theoremcldss2 13273 The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.)
𝑋 = 𝐽       (Clsd‘𝐽) ⊆ 𝒫 𝑋
 
Theoremcldopn 13274 The complement of a closed set is open. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
𝑋 = 𝐽       (𝑆 ∈ (Clsd‘𝐽) → (𝑋𝑆) ∈ 𝐽)
 
Theoremdifopn 13275 The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.)
𝑋 = 𝐽       ((𝐴𝐽𝐵 ∈ (Clsd‘𝐽)) → (𝐴𝐵) ∈ 𝐽)
 
Theoremtopcld 13276 The underlying set of a topology is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 3-Oct-2006.)
𝑋 = 𝐽       (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
 
Theoremntrval 13277 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, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((int‘𝐽)‘𝑆) = (𝐽 ∩ 𝒫 𝑆))
 
Theoremclsval 13278* 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, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((cls‘𝐽)‘𝑆) = {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆𝑥})
 
Theorem0cld 13279 The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 4-Oct-2006.)
(𝐽 ∈ Top → ∅ ∈ (Clsd‘𝐽))
 
Theoremuncld 13280 The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of [Munkres] p. 93. (Contributed by NM, 5-Oct-2006.)
((𝐴 ∈ (Clsd‘𝐽) ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴𝐵) ∈ (Clsd‘𝐽))
 
Theoremcldcls 13281 A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
(𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆)
 
Theoremiuncld 13282* A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) (Revised by Jim Kingdon, 10-Mar-2023.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵 ∈ (Clsd‘𝐽)) → 𝑥𝐴 𝐵 ∈ (Clsd‘𝐽))
 
Theoremunicld 13283 A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → 𝐴 ∈ (Clsd‘𝐽))
 
Theoremntropn 13284 The interior of a subset of a topology's underlying set is open. (Contributed by NM, 11-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((int‘𝐽)‘𝑆) ∈ 𝐽)
 
Theoremclsss 13285 Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆))
 
Theoremntrss 13286 Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆))
 
Theoremsscls 13287 A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
 
Theoremntrss2 13288 A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆)
 
Theoremssntr 13289 An open subset of a set is a subset of the set's interior. (Contributed by Jeff Hankins, 31-Aug-2009.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       (((𝐽 ∈ Top ∧ 𝑆𝑋) ∧ (𝑂𝐽𝑂𝑆)) → 𝑂 ⊆ ((int‘𝐽)‘𝑆))
 
Theoremntrss3 13290 The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋)
 
Theoremntrin 13291 A pairwise intersection of interiors is the interior of the intersection. This does not always hold for arbitrary intersections. (Contributed by Jeff Hankins, 31-Aug-2009.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝑋) → ((int‘𝐽)‘(𝐴𝐵)) = (((int‘𝐽)‘𝐴) ∩ ((int‘𝐽)‘𝐵)))
 
Theoremisopn3 13292 A subset is open iff it equals its own interior. (Contributed by NM, 9-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → (𝑆𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆))
 
Theoremntridm 13293 The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆))
 
Theoremclstop 13294 The closure of a topology's underlying set is the entire set. (Contributed by NM, 5-Oct-2007.) (Proof shortened by Jim Kingdon, 11-Mar-2023.)
𝑋 = 𝐽       (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
 
Theoremntrtop 13295 The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.)
𝑋 = 𝐽       (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋)
 
Theoremclsss2 13296 If a subset is included in a closed set, so is the subset's closure. (Contributed by NM, 22-Feb-2007.)
𝑋 = 𝐽       ((𝐶 ∈ (Clsd‘𝐽) ∧ 𝑆𝐶) → ((cls‘𝐽)‘𝑆) ⊆ 𝐶)
 
Theoremclsss3 13297 The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
 
Theoremntrcls0 13298 A subset whose closure has an empty interior also has an empty interior. (Contributed by NM, 4-Oct-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋 ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑆)) = ∅) → ((int‘𝐽)‘𝑆) = ∅)
 
Theoremntreq0 13299* Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → (((int‘𝐽)‘𝑆) = ∅ ↔ ∀𝑥𝐽 (𝑥𝑆𝑥 = ∅)))
 
Theoremcls0 13300 The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.)
(𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅)
    < 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-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14485
  Copyright terms: Public domain < Previous  Next >