 Home Intuitionistic Logic ExplorerTheorem List (p. 120 of 127) < 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 - 11901-12000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremtpspropd 11901 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 11902 Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
𝐴 = (Base‘𝐾)    &   𝐽 = (TopSet‘𝐾)       (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾))

Theoremtsettps 11903 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 11904 Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
(Base‘𝐾) = 𝐴    &   (TopOpen‘𝐾) = 𝐽    &   𝐴 = 𝐽    &   𝐽 ∈ Top       𝐾 ∈ TopSp

Theoremeltpsg 11905 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 11906 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

6.1.2  Topological bases

Syntaxctb 11907 Syntax for the class of topological bases.
class TopBases

Definitiondf-bases 11908* Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 11910). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.)
TopBases = {𝑥 ∣ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ⊆ (𝑥 ∩ 𝒫 (𝑦𝑧))}

Theoremisbasisg 11909* Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
(𝐵𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥𝐵𝑦𝐵 (𝑥𝑦) ⊆ (𝐵 ∩ 𝒫 (𝑥𝑦))))

Theoremisbasis2g 11910* Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
(𝐵𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥𝐵𝑦𝐵𝑧 ∈ (𝑥𝑦)∃𝑤𝐵 (𝑧𝑤𝑤 ⊆ (𝑥𝑦))))

Theoremisbasis3g 11911* 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 11912 Property of a basis. (Contributed by NM, 16-Jul-2006.)
((𝐵 ∈ TopBases ∧ 𝐶𝐵𝐷𝐵) → (𝐶𝐷) ⊆ (𝐵 ∩ 𝒫 (𝐶𝐷)))

Theorembasis2 11913* Property of a basis. (Contributed by NM, 17-Jul-2006.)
(((𝐵 ∈ TopBases ∧ 𝐶𝐵) ∧ (𝐷𝐵𝐴 ∈ (𝐶𝐷))) → ∃𝑥𝐵 (𝐴𝑥𝑥 ⊆ (𝐶𝐷)))

Theoremfiinbas 11914* 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 11915* A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
((𝑃𝑉 ∧ ∀𝑥𝑃𝑦𝑃 (𝑥 = 𝑦 ∨ (𝑥𝑦) = ∅)) → 𝑃 ∈ TopBases)

Theoremtgval 11916* The topology generated by a basis. See also tgval2 11918 and tgval3 11925. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (topGen‘𝐵) = {𝑥𝑥 (𝐵 ∩ 𝒫 𝑥)})

Theoremtgvalex 11917 The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.)
(𝐵𝑉 → (topGen‘𝐵) ∈ V)

Theoremtgval2 11918* Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 11931) that (topGen‘𝐵) is indeed a topology (on 𝐵, see unitg 11929). See also tgval 11916 and tgval3 11925. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 𝐵 ∧ ∀𝑦𝑥𝑧𝐵 (𝑦𝑧𝑧𝑥))})

Theoremeltg 11919 Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 (𝐵 ∩ 𝒫 𝐴)))

Theoremeltg2 11920* Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 (𝑥𝑦𝑦𝐴))))

Theoremeltg2b 11921* Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥𝐴𝑦𝐵 (𝑥𝑦𝑦𝐴)))

Theoremeltg4i 11922 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 11923 The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
((𝐵𝑉𝐴𝐵) → 𝐴 ∈ (topGen‘𝐵))

Theoremeltg3 11924* Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
(𝐵𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥𝐵𝐴 = 𝑥)))

Theoremtgval3 11925* Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 11916 and tgval2 11918. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
(𝐵𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦𝐵𝑥 = 𝑦)})

Theoremtg1 11926 Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
(𝐴 ∈ (topGen‘𝐵) → 𝐴 𝐵)

Theoremtg2 11927* Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶𝐴) → ∃𝑥𝐵 (𝐶𝑥𝑥𝐴))

Theorembastg 11928 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 11929 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 11930 Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
((𝐶𝑉𝐵𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶))

Theoremtgcl 11931 Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
(𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)

Theoremtgclb 11932 The property tgcl 11931 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 11933 A basis generates a topology on 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.)
(𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘ 𝐵))

Theoremtopbas 11934 A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
(𝐽 ∈ Top → 𝐽 ∈ TopBases)

Theoremtgtop 11935 A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
(𝐽 ∈ Top → (topGen‘𝐽) = 𝐽)

Theoremeltop 11936 Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
(𝐽 ∈ Top → (𝐴𝐽𝐴 (𝐽 ∩ 𝒫 𝐴)))

Theoremeltop2 11937* Membership in a topology. (Contributed by NM, 19-Jul-2006.)
(𝐽 ∈ Top → (𝐴𝐽 ↔ ∀𝑥𝐴𝑦𝐽 (𝑥𝑦𝑦𝐴)))

Theoremeltop3 11938* Membership in a topology. (Contributed by NM, 19-Jul-2006.)
(𝐽 ∈ Top → (𝐴𝐽 ↔ ∃𝑥(𝑥𝐽𝐴 = 𝑥)))

Theoremtgdom 11939 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 11940* The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
((𝐵𝑉 ∧ ∀𝑥𝐴 𝐶𝐵) → 𝑥𝐴 𝐶 ∈ (topGen‘𝐵))

Theoremtgidm 11941 The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
(𝐵𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵))

Theorembastop 11942 Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
(𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵))

Theoremtgtop11 11943 The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.)
((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾)

Theoremen1top 11944 {∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
(𝐽 ∈ Top → (𝐽 ≈ 1o𝐽 = {∅}))

Theoremtgss3 11945 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 11946* 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 11947 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 11948* 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 11949 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 11950* 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 11951* A version of bastop1 11950 that doesn't have 𝐵𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.)
(𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵𝐽 ∧ ∀𝑥𝐽𝑦(𝑦𝐵𝑥 = 𝑦))))

6.1.3  Examples of topologies

Theoremdistop 11952 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 11953 The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 4299. (Contributed by BJ, 2-May-2021.)
Top ∉ V

Theoremdistopon 11954 The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
(𝐴𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))

Theoremsn0topon 11955 The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
{∅} ∈ (TopOn‘∅)

Theoremsn0top 11956 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 11957* The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ (TopOn‘𝐴))

Theoremdistps 11958 The discrete topology on a set 𝐴 expressed as a topological space. (Contributed by FL, 20-Aug-2006.)
𝐴 ∈ V    &   𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝒫 𝐴⟩}       𝐾 ∈ TopSp

6.1.4  Closure and interior

Syntaxccld 11959 Extend class notation with the set of closed sets of a topology.
class Clsd

Syntaxcnt 11960 Extend class notation with interior of a subset of a topology base set.
class int

Syntaxccl 11961 Extend class notation with closure of a subset of a topology base set.
class cls

Definitiondf-cld 11962* 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 11963* Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 11977. (Contributed by NM, 10-Sep-2006.)
int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 (𝑗 ∩ 𝒫 𝑥)))

Definitiondf-cls 11964* Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 11978. (Contributed by NM, 3-Oct-2006.)
cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 𝑗 {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥𝑦}))

Theoremfncld 11965 The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Clsd Fn Top

Theoremcldval 11966* 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 11967* 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 11968* 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 11969 Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
(𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top)

Theoremiscld 11970 The predicate "the class 𝑆 is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆𝑋 ∧ (𝑋𝑆) ∈ 𝐽)))

Theoremiscld2 11971 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 11972 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 11973 The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.)
𝑋 = 𝐽       (Clsd‘𝐽) ⊆ 𝒫 𝑋

Theoremcldopn 11974 The complement of a closed set is open. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
𝑋 = 𝐽       (𝑆 ∈ (Clsd‘𝐽) → (𝑋𝑆) ∈ 𝐽)

Theoremdifopn 11975 The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.)
𝑋 = 𝐽       ((𝐴𝐽𝐵 ∈ (Clsd‘𝐽)) → (𝐴𝐵) ∈ 𝐽)

Theoremtopcld 11976 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 11977 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 11978* 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 11979 The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 4-Oct-2006.)
(𝐽 ∈ Top → ∅ ∈ (Clsd‘𝐽))

Theoremuncld 11980 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 11981 A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
(𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆)

Theoremiuncld 11982* 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 11983 A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → 𝐴 ∈ (Clsd‘𝐽))

Theoremntropn 11984 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 11985 Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆))

Theoremntrss 11986 Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆))

Theoremsscls 11987 A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))

Theoremntrss2 11988 A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆)

Theoremssntr 11989 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 11990 The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋)

Theoremntrin 11991 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 11992 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 11993 The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆))

Theoremclstop 11994 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 11995 The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.)
𝑋 = 𝐽       (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋)

Theoremclsss2 11996 If a subset is included in a closed set, so is the subset's closure. (Contributed by NM, 22-Feb-2007.)
𝑋 = 𝐽       ((𝐶 ∈ (Clsd‘𝐽) ∧ 𝑆𝐶) → ((cls‘𝐽)‘𝑆) ⊆ 𝐶)

Theoremclsss3 11997 The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)

Theoremntrcls0 11998 A subset whose closure has an empty interior also has an empty interior. (Contributed by NM, 4-Oct-2007.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋 ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑆)) = ∅) → ((int‘𝐽)‘𝑆) = ∅)

Theoremntreq0 11999* 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 12000 The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.)
(𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅)

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-12636
 Copyright terms: Public domain < Previous  Next >