Home | Metamath
Proof Explorer Theorem List (p. 222 of 466) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eltpsg 22101 | Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by AV, 31-Oct-2024.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) | ||
Theorem | eltpsgOLD 22102 | Obsolete version of eltpsg 22101 as of 31-Oct-2024. Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) | ||
Theorem | eltpsi 22103 | 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 | ||
Syntax | ctb 22104 | Syntax for the class of topological bases. |
class TopBases | ||
Definition | df-bases 22105* | Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 22107). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.) |
⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))} | ||
Theorem | isbasisg 22106* | Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | ||
Theorem | isbasis2g 22107* | Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦)))) | ||
Theorem | isbasis3g 22108* | 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 22109 | Property of a basis. (Contributed by NM, 16-Jul-2006.) |
⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪ (𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷))) | ||
Theorem | basis2 22110* | Property of a basis. (Contributed by NM, 17-Jul-2006.) |
⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷))) | ||
Theorem | fiinbas 22111* | 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 | basdif0 22112 | A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ ((𝐵 ∖ {∅}) ∈ TopBases ↔ 𝐵 ∈ TopBases) | ||
Theorem | baspartn 22113* | A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases) | ||
Theorem | tgval 22114* | The topology generated by a basis. See also tgval2 22115 and tgval3 22122. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)}) | ||
Theorem | tgval2 22115* | Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 22128) that (topGen‘𝐵) is indeed a topology (on ∪ 𝐵, see unitg 22126). See also tgval 22114 and tgval3 22122. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))}) | ||
Theorem | eltg 22116 | Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪ (𝐵 ∩ 𝒫 𝐴))) | ||
Theorem | eltg2 22117* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))) | ||
Theorem | eltg2b 22118* | 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 22119 | 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 22120 | The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵)) | ||
Theorem | eltg3 22121* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Mario Carneiro, 30-Aug-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥))) | ||
Theorem | tgval3 22122* | Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 22114 and tgval2 22115. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)}) | ||
Theorem | tg1 22123 | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | tg2 22124* | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) | ||
Theorem | bastg 22125 | 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 22126 | 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 22127 | Subset relation for generated topologies. (Contributed by NM, 7-May-2007.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶)) | ||
Theorem | tgcl 22128 | Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.) |
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top) | ||
Theorem | tgclb 22129 | The property tgcl 22128 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 22130 | A basis generates a topology on ∪ 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵)) | ||
Theorem | topbas 22131 | A topology is its own basis. (Contributed by NM, 17-Jul-2006.) |
⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases) | ||
Theorem | tgtop 22132 | A topology is its own basis. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽) | ||
Theorem | eltop 22133 | Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ (𝐽 ∩ 𝒫 𝐴))) | ||
Theorem | eltop2 22134* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) | ||
Theorem | eltop3 22135* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥))) | ||
Theorem | fibas 22136 | A collection of finite intersections is a basis. The initial set is a subbasis for the topology. (Contributed by Jeff Hankins, 25-Aug-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (fi‘𝐴) ∈ TopBases | ||
Theorem | tgdom 22137 | 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 22138* | 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 22139 | The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.) |
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵)) | ||
Theorem | bastop 22140 | Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵)) | ||
Theorem | tgtop11 22141 | The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾) | ||
Theorem | 0top 22142 | The singleton of the empty set is the only topology possible for an empty underlying set. (Contributed by NM, 9-Sep-2006.) |
⊢ (𝐽 ∈ Top → (∪ 𝐽 = ∅ ↔ 𝐽 = {∅})) | ||
Theorem | en1top 22143 | {∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.) |
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅})) | ||
Theorem | en2top 22144 | If a topology has two elements, it is the indiscrete topology. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ≈ 2o ↔ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅))) | ||
Theorem | tgss3 22145 | 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 22146* | 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 22147 | 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 22148* | 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 | 2basgen 22149 | Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 2-Sep-2015.) |
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = (topGen‘𝐶)) | ||
Theorem | tgfiss 22150 | If a subbase is included into a topology, so is the generated topology. (Contributed by FL, 20-Apr-2012.) (Proof shortened by Mario Carneiro, 10-Jan-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽) → (topGen‘(fi‘𝐴)) ⊆ 𝐽) | ||
Theorem | tgdif0 22151 | A generated topology is not affected by the addition or removal of the empty set from the base. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (topGen‘(𝐵 ∖ {∅})) = (topGen‘𝐵) | ||
Theorem | bastop1 22152* | 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 22153* | A version of bastop1 22152 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.) |
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)))) | ||
Theorem | distop 22154 | 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 22155 | The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7618; an alternate proof uses indiscrete topologies (see indistop 22161) and the analogue of pwnex 7618 with pairs {∅, 𝑥} instead of power sets 𝒫 𝑥 (that analogue is also a consequence of abnex 7616). (Contributed by BJ, 2-May-2021.) |
⊢ Top ∉ V | ||
Theorem | distopon 22156 | The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) | ||
Theorem | sn0topon 22157 | The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ {∅} ∈ (TopOn‘∅) | ||
Theorem | sn0top 22158 | 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 | indislem 22159 | A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ {∅, ( I ‘𝐴)} = {∅, 𝐴} | ||
Theorem | indistopon 22160 | The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴)) | ||
Theorem | indistop 22161 | The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 16-Jul-2006.) (Revised by Stefan Allan, 6-Nov-2008.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ {∅, 𝐴} ∈ Top | ||
Theorem | indisuni 22162 | The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ( I ‘𝐴) = ∪ {∅, 𝐴} | ||
Theorem | fctop 22163* | The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (Contributed by FL, 15-Aug-2006.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | fctop2 22164* | The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (This version of fctop 22163 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≺ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | cctop 22165* | The countable complement topology on a set 𝐴. Example 4 in [Munkres] p. 77. (Contributed by FL, 23-Aug-2006.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | ppttop 22166* | The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | pptbas 22167* | The particular point topology is generated by a basis consisting of pairs {𝑥, 𝑃} for each 𝑥 ∈ 𝐴. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} = (topGen‘ran (𝑥 ∈ 𝐴 ↦ {𝑥, 𝑃}))) | ||
Theorem | epttop 22168* | The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴)) | ||
Theorem | indistpsx 22169 | The indiscrete topology on a set 𝐴 expressed as a topological space, using explicit structure component references. Compare with indistps 22170 and indistps2 22171. The advantage of this version is that the actual function for the structure is evident, and df-ndx 16904 is not needed, nor any other special definition outside of basic set theory. The disadvantage is that if the indices of the component definitions df-base 16922 and df-tset 16990 are changed in the future, this theorem will also have to be changed. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use indistps 22170 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈1, 𝐴〉, 〈9, {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistps 22170 | The indiscrete topology on a set 𝐴 expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 22169 is that it is independent of the indices of the component definitions df-base 16922 and df-tset 16990, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 22171 is that it is easy to eliminate the hypotheses with eqid 2739 and vtoclg 3506 to result in a closed theorem. Theorems indistpsALT 22172 and indistps2ALT 22174 show that the two forms can be derived from each other. (Contributed by FL, 19-Jul-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistps2 22171 | The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 22170. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 22172 and indistps2ALT 22174 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.) |
⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = {∅, 𝐴} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistpsALT 22172 | The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 22170 from the direct component assignment version indistps2 22171. (Contributed by NM, 24-Oct-2012.) (Revised by AV, 31-Oct-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistpsALTOLD 22173 | Obsolete proof of indistpsALT 22172 as of 31-Oct-2024. The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 22170 from the direct component assignment version indistps2 22171. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistps2ALT 22174 | The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Here we show how to derive the direct component assignment version indistps2 22171 from the structural version indistps 22170. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = {∅, 𝐴} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | distps 22175 | The discrete topology on a set 𝐴 expressed as a topological space. (Contributed by FL, 20-Aug-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), 𝒫 𝐴〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Syntax | ccld 22176 | Extend class notation with the set of closed sets of a topology. |
class Clsd | ||
Syntax | cnt 22177 | Extend class notation with interior of a subset of a topology base set. |
class int | ||
Syntax | ccl 22178 | Extend class notation with closure of a subset of a topology base set. |
class cls | ||
Definition | df-cld 22179* | 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 22180* | Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 22196. (Contributed by NM, 10-Sep-2006.) |
⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥))) | ||
Definition | df-cls 22181* | Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 22197. (Contributed by NM, 3-Oct-2006.) |
⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) | ||
Theorem | fncld 22182 | The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ Clsd Fn Top | ||
Theorem | cldval 22183* | 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 22184* | 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 22185* | 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 22186 | Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) | ||
Theorem | iscld 22187 | 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 22188 | A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑆) ∈ 𝐽)) | ||
Theorem | cldss 22189 | 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‘𝐽) → 𝑆 ⊆ 𝑋) | ||
Theorem | cldss2 22190 | The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋 | ||
Theorem | cldopn 22191 | The complement of a closed set is open. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑆 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑆) ∈ 𝐽) | ||
Theorem | isopn2 22192 | A subset of the underlying set of a topology is open iff its complement is closed. (Contributed by NM, 4-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 ↔ (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽))) | ||
Theorem | opncld 22193 | The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽)) | ||
Theorem | difopn 22194 | The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽) | ||
Theorem | topcld 22195 | 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‘𝐽)) | ||
Theorem | ntrval 22196 | 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‘𝐽)‘𝑆) = ∪ (𝐽 ∩ 𝒫 𝑆)) | ||
Theorem | clsval 22197* | 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‘𝐽) ∣ 𝑆 ⊆ 𝑥}) | ||
Theorem | 0cld 22198 | The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 4-Oct-2006.) |
⊢ (𝐽 ∈ Top → ∅ ∈ (Clsd‘𝐽)) | ||
Theorem | iincld 22199* | The indexed intersection of a collection 𝐵(𝑥) of closed sets is closed. Theorem 6.1(2) of [Munkres] p. 93. (Contributed by NM, 5-Oct-2006.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) | ||
Theorem | intcld 22200 | The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∩ 𝐴 ∈ (Clsd‘𝐽)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |