Home | Metamath
Proof Explorer Theorem List (p. 208 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | istop2g 20701* | Express the predicate " is a topology," using nonempty finite intersections instead of binary intersections as in istopg 20700. (Contributed by NM, 19-Jul-2006.) |
Theorem | uniopn 20702 | 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.) |
Theorem | iunopn 20703* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) |
Theorem | inopn 20704 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
Theorem | fitop 20705 | A topology is closed under finite intersections. (Contributed by Jeff Hankins, 7-Oct-2009.) |
Theorem | fiinopn 20706 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) |
Theorem | iinopn 20707* | The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014.) |
Theorem | unopn 20708 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | 0opn 20709 | The empty set is an open subset of a topology. (Contributed by Stefan Allan, 27-Feb-2006.) |
Theorem | 0ntop 20710 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) |
Theorem | topopn 20711 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
Theorem | eltopss 20712 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) |
Theorem | riinopn 20713* | A finite indexed relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) |
Theorem | rintopn 20714 | A finite relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) |
Syntax | ctopon 20715 | Syntax for the function of topologies on sets. |
TopOn | ||
Definition | df-topon 20716* | Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
TopOn | ||
Theorem | istopon 20717 | 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 | ||
Theorem | topontop 20718 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopOn | ||
Theorem | toponuni 20719 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopOn | ||
Theorem | topontopi 20720 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopOn | ||
Theorem | toponunii 20721 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopOn | ||
Theorem | toptopon 20722 | Alternative definition of in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopOn | ||
Theorem | toptopon2 20723 | A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) |
TopOn | ||
Theorem | topontopon 20724 | 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 20725 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) |
TopOn | ||
Theorem | toponsspwpw 20726 | 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 20727 | The domain of TopOn is . (Contributed by BJ, 29-Apr-2021.) |
TopOn | ||
Theorem | fntopon 20728 | The class TopOn is a function with domain . Analogue for topologies of fnmre 16251 for Moore collections. (Contributed by BJ, 29-Apr-2021.) |
TopOn | ||
Theorem | toprntopon 20729 | A topology is the same thing as a topology on a set (variable-free version). (Contributed by BJ, 27-Apr-2021.) |
TopOn | ||
Theorem | toponmax 20730 | The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopOn | ||
Theorem | toponss 20731 | A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
TopOn | ||
Theorem | toponcom 20732 | 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.) |
TopOn TopOn | ||
Theorem | toponcomb 20733 | Biconditional form of toponcom 20732. (Contributed by BJ, 5-Dec-2021.) |
TopOn TopOn | ||
Theorem | topgele 20734 | 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 20735 | The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn 4428). (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
TopOn | ||
Syntax | ctps 20736 | Syntax for the class of topological spaces. |
Definition | df-topsp 20737 | Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.) |
TopOn | ||
Theorem | istps 20738 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopOn | ||
Theorem | istps2 20739 | Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.) |
Theorem | tpsuni 20740 | The base set of a topological space. (Contributed by FL, 27-Jun-2014.) |
Theorem | tpstop 20741 | The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.) |
Theorem | tpspropd 20742 | A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.) |
Theorem | tpsprop2d 20743 | A topological space depends only on the base and topology components. (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopSet TopSet | ||
Theorem | topontopn 20744 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopSet TopOn | ||
Theorem | tsettps 20745 | 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.) |
TopSet TopOn | ||
Theorem | istpsi 20746 | Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.) |
Theorem | eltpsg 20747 | Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) |
TopSet TopOn | ||
Theorem | eltpsi 20748 | 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.) |
TopSet | ||
Syntax | ctb 20749 | Syntax for the class of topological bases. |
Definition | df-bases 20750* | Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 20752). Note that "bases" is the plural of "basis." (Contributed by NM, 17-Jul-2006.) |
Theorem | isbasisg 20751* | Express the predicate " is a basis for a topology." (Contributed by NM, 17-Jul-2006.) |
Theorem | isbasis2g 20752* | Express the predicate " is a basis for a topology." (Contributed by NM, 17-Jul-2006.) |
Theorem | isbasis3g 20753* | Express the predicate " is a basis for a topology." Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.) |
Theorem | basis1 20754 | Property of a basis. (Contributed by NM, 16-Jul-2006.) |
Theorem | basis2 20755* | Property of a basis. (Contributed by NM, 17-Jul-2006.) |
Theorem | fiinbas 20756* | If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | basdif0 20757 | A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015.) |
Theorem | baspartn 20758* | A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Theorem | tgval 20759* | The topology generated by a basis. See also tgval2 20760 and tgval3 20767. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
Theorem | tgval2 20760* | Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 20773) that is indeed a topology (on , see unitg 20771). See also tgval 20759 and tgval3 20767. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
Theorem | eltg 20761 | Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
Theorem | eltg2 20762* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
Theorem | eltg2b 20763* | Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.) |
Theorem | eltg4i 20764 | 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.) |
Theorem | eltg3i 20765 | The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
Theorem | eltg3 20766* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Mario Carneiro, 30-Aug-2015.) |
Theorem | tgval3 20767* | Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 20759 and tgval2 20760. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.) |
Theorem | tg1 20768 | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
Theorem | tg2 20769* | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
Theorem | bastg 20770 | 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.) |
Theorem | unitg 20771 | 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 completely specifies the basis it corresponds to. (Contributed by NM, 16-Jul-2006.) (Proof shortened by OpenAI, 30-Mar-2020.) |
Theorem | tgss 20772 | Subset relation for generated topologies. (Contributed by NM, 7-May-2007.) |
Theorem | tgcl 20773 | Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.) |
Theorem | tgclb 20774 | The property tgcl 20773 can be reversed: if the topology generated by is actually a topology, then must be a topological basis. This yields an alternative definition of . (Contributed by Mario Carneiro, 2-Sep-2015.) |
Theorem | tgtopon 20775 | A basis generates a topology on . (Contributed by Mario Carneiro, 14-Aug-2015.) |
TopOn | ||
Theorem | topbas 20776 | A topology is its own basis. (Contributed by NM, 17-Jul-2006.) |
Theorem | tgtop 20777 | A topology is its own basis. (Contributed by NM, 18-Jul-2006.) |
Theorem | eltop 20778 | Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.) |
Theorem | eltop2 20779* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
Theorem | eltop3 20780* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
Theorem | fibas 20781 | 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.) |
Theorem | tgdom 20782 | 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.) |
Theorem | tgiun 20783* | The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
Theorem | tgidm 20784 | The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.) |
Theorem | bastop 20785 | Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.) |
Theorem | tgtop11 20786 | The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.) |
Theorem | 0top 20787 | The singleton of the empty set is the only topology possible for an empty underlying set. (Contributed by NM, 9-Sep-2006.) |
Theorem | en1top 20788 | is the only topology with one element. (Contributed by FL, 18-Aug-2008.) |
Theorem | en2top 20789 | 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 | ||
Theorem | tgss3 20790 | 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.) |
Theorem | tgss2 20791* | 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.) |
Theorem | basgen 20792 | 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.) |
Theorem | basgen2 20793* | 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.) |
Theorem | 2basgen 20794 | Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 2-Sep-2015.) |
Theorem | tgfiss 20795 | 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.) |
Theorem | tgdif0 20796 | 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.) |
Theorem | bastop1 20797* | 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 " " 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.) |
Theorem | bastop2 20798* | A version of bastop1 20797 that doesn't have in the antecedent. (Contributed by NM, 3-Feb-2008.) |
Theorem | distop 20799 | 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.) |
Theorem | topnex 20800 | The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 6968; an alternate proof uses indiscrete topologies (see indistop 20806) and the analogue of pwnex 6968 with pairs instead of power sets (that analogue is also a consequence of abnex 6965). (Contributed by BJ, 2-May-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |