| Metamath
Proof Explorer Theorem List (p. 230 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | istopg 22901* |
Express the predicate "𝐽 is a topology". See istop2g 22902 for another
characterization using nonempty finite intersections instead of binary
intersections.
Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use 𝑇 to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
| ⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))) | ||
| Theorem | istop2g 22902* | Express the predicate "𝐽 is a topology" using nonempty finite intersections instead of binary intersections as in istopg 22901. (Contributed by NM, 19-Jul-2006.) |
| ⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐽)))) | ||
| Theorem | uniopn 22903 | The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006.) |
| ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽) → ∪ 𝐴 ∈ 𝐽) | ||
| Theorem | iunopn 22904* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) |
| ⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) | ||
| Theorem | inopn 22905 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
| ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) | ||
| Theorem | fitop 22906 | A topology is closed under finite intersections. (Contributed by Jeff Hankins, 7-Oct-2009.) |
| ⊢ (𝐽 ∈ Top → (fi‘𝐽) = 𝐽) | ||
| Theorem | fiinopn 22907 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) |
| ⊢ (𝐽 ∈ Top → ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → ∩ 𝐴 ∈ 𝐽)) | ||
| Theorem | iinopn 22908* | The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014.) |
| ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) | ||
| Theorem | unopn 22909 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∪ 𝐵) ∈ 𝐽) | ||
| Theorem | 0opn 22910 | The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.) |
| ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽) | ||
| Theorem | 0ntop 22911 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) |
| ⊢ ¬ ∅ ∈ Top | ||
| Theorem | topopn 22912 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) | ||
| Theorem | eltopss 22913 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) | ||
| Theorem | riinopn 22914* | A finite indexed relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ 𝐽) | ||
| Theorem | rintopn 22915 | A finite relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ∧ 𝐴 ∈ Fin) → (𝑋 ∩ ∩ 𝐴) ∈ 𝐽) | ||
| Syntax | ctopon 22916 | Syntax for the function of topologies on sets. |
| class TopOn | ||
| Definition | df-topon 22917* | 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 | istopon 22918 | 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 22919 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) | ||
| Theorem | toponuni 22920 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) | ||
| Theorem | topontopi 22921 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ 𝐽 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐽 ∈ Top | ||
| Theorem | toponunii 22922 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ 𝐽 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐵 = ∪ 𝐽 | ||
| Theorem | toptopon 22923 | Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) | ||
| Theorem | toptopon2 22924 | 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 22925 | A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ (TopOn‘∪ 𝐽)) | ||
| Theorem | funtopon 22926 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) |
| ⊢ Fun TopOn | ||
| Theorem | toponrestid 22927 | 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 | toponsspwpw 22928 | The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) |
| ⊢ (TopOn‘𝐴) ⊆ 𝒫 𝒫 𝐴 | ||
| Theorem | dmtopon 22929 | The domain of TopOn is the universal class V. (Contributed by BJ, 29-Apr-2021.) |
| ⊢ dom TopOn = V | ||
| Theorem | fntopon 22930 | The class TopOn is a function with domain the universal class V. Analogue for topologies of fnmre 17634 for Moore collections. (Contributed by BJ, 29-Apr-2021.) |
| ⊢ TopOn Fn V | ||
| Theorem | toprntopon 22931 | A topology is the same thing as a topology on a set (variable-free version). (Contributed by BJ, 27-Apr-2021.) |
| ⊢ Top = ∪ ran TopOn | ||
| Theorem | toponmax 22932 | The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽) | ||
| Theorem | toponss 22933 | A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) | ||
| Theorem | toponcom 22934 | 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 22935 | Biconditional form of toponcom 22934. (Contributed by BJ, 5-Dec-2021.) |
| ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ∈ (TopOn‘∪ 𝐾) ↔ 𝐾 ∈ (TopOn‘∪ 𝐽))) | ||
| Theorem | topgele 22936 | 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‘𝑋) → ({∅, 𝑋} ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋)) | ||
| Theorem | topsn 22937 | The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn 4900). (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
| ⊢ (𝐽 ∈ (TopOn‘{𝐴}) → 𝐽 = 𝒫 {𝐴}) | ||
| Syntax | ctps 22938 | Syntax for the class of topological spaces. |
| class TopSp | ||
| Definition | df-topsp 22939 | Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.) |
| ⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} | ||
| Theorem | istps 22940 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴)) | ||
| Theorem | istps2 22941 | Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.) |
| ⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp ↔ (𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽)) | ||
| Theorem | tpsuni 22942 | The base set of a topological space. (Contributed by FL, 27-Jun-2014.) |
| ⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp → 𝐴 = ∪ 𝐽) | ||
| Theorem | tpstop 22943 | The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.) |
| ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp → 𝐽 ∈ Top) | ||
| Theorem | tpspropd 22944 | 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 | tpsprop2d 22945 | A topological space depends only on the base and topology components. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp)) | ||
| Theorem | topontopn 22946 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopSet‘𝐾) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾)) | ||
| Theorem | tsettps 22947 | 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 22948 | Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.) |
| ⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = 𝐽 & ⊢ 𝐴 = ∪ 𝐽 & ⊢ 𝐽 ∈ Top ⇒ ⊢ 𝐾 ∈ TopSp | ||
| Theorem | eltpsg 22949 | 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 22950 | Obsolete version of eltpsg 22949 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 22951 | 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 22952 | Syntax for the class of topological bases. |
| class TopBases | ||
| Definition | df-bases 22953* | Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 22955). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.) |
| ⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))} | ||
| Theorem | isbasisg 22954* | Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
| ⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | ||
| Theorem | isbasis2g 22955* | Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
| ⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦)))) | ||
| Theorem | isbasis3g 22956* | 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 22957 | Property of a basis. (Contributed by NM, 16-Jul-2006.) |
| ⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪ (𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷))) | ||
| Theorem | basis2 22958* | Property of a basis. (Contributed by NM, 17-Jul-2006.) |
| ⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷))) | ||
| Theorem | fiinbas 22959* | 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 22960 | 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 22961* | A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| ⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases) | ||
| Theorem | tgval 22962* | The topology generated by a basis. See also tgval2 22963 and tgval3 22970. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| ⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)}) | ||
| Theorem | tgval2 22963* | Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 22976) that (topGen‘𝐵) is indeed a topology (on ∪ 𝐵, see unitg 22974). See also tgval 22962 and tgval3 22970. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| ⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))}) | ||
| Theorem | eltg 22964 | Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪ (𝐵 ∩ 𝒫 𝐴))) | ||
| Theorem | eltg2 22965* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))) | ||
| Theorem | eltg2b 22966* | 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 22967 | 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 22968 | The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
| ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵)) | ||
| Theorem | eltg3 22969* | 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 22970* | Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 22962 and tgval2 22963. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.) |
| ⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)}) | ||
| Theorem | tg1 22971 | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
| ⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵) | ||
| Theorem | tg2 22972* | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
| ⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) | ||
| Theorem | bastg 22973 | 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 22974 | 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 22975 | Subset relation for generated topologies. (Contributed by NM, 7-May-2007.) |
| ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶)) | ||
| Theorem | tgcl 22976 | Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.) |
| ⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top) | ||
| Theorem | tgclb 22977 | The property tgcl 22976 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 22978 | A basis generates a topology on ∪ 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵)) | ||
| Theorem | topbas 22979 | A topology is its own basis. (Contributed by NM, 17-Jul-2006.) |
| ⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases) | ||
| Theorem | tgtop 22980 | A topology is its own basis. (Contributed by NM, 18-Jul-2006.) |
| ⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽) | ||
| Theorem | eltop 22981 | Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.) |
| ⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ (𝐽 ∩ 𝒫 𝐴))) | ||
| Theorem | eltop2 22982* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
| ⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) | ||
| Theorem | eltop3 22983* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
| ⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥))) | ||
| Theorem | fibas 22984 | 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 22985 | 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 22986* | 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 22987 | The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.) |
| ⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵)) | ||
| Theorem | bastop 22988 | Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.) |
| ⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵)) | ||
| Theorem | tgtop11 22989 | 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 22990 | 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 22991 | {∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.) |
| ⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅})) | ||
| Theorem | en2top 22992 | 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 22993 | 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 22994* | 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 22995 | 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 22996* | 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 22997 | 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 22998 | 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 22999 | 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 23000* | 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‘𝐵) = 𝐽 ↔ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |