![]() |
Metamath
Proof Explorer Theorem List (p. 229 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | istopon 22801 | 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 22802 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π½ β Top) | ||
Theorem | toponuni 22803 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) | ||
Theorem | topontopi 22804 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π½ β (TopOnβπ΅) β β’ π½ β Top | ||
Theorem | toponunii 22805 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π½ β (TopOnβπ΅) β β’ π΅ = βͺ π½ | ||
Theorem | toptopon 22806 | Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β Top β π½ β (TopOnβπ)) | ||
Theorem | toptopon2 22807 | 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 22808 | 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 22809 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) |
β’ Fun TopOn | ||
Theorem | toponrestid 22810 | 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 22811 | 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 22812 | The domain of TopOn is the universal class V. (Contributed by BJ, 29-Apr-2021.) |
β’ dom TopOn = V | ||
Theorem | fntopon 22813 | The class TopOn is a function with domain the universal class V. Analogue for topologies of fnmre 17562 for Moore collections. (Contributed by BJ, 29-Apr-2021.) |
β’ TopOn Fn V | ||
Theorem | toprntopon 22814 | 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 22815 | The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π΅ β π½) | ||
Theorem | toponss 22816 | A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π½) β π΄ β π) | ||
Theorem | toponcom 22817 | 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 22818 | Biconditional form of toponcom 22817. (Contributed by BJ, 5-Dec-2021.) |
β’ ((π½ β Top β§ πΎ β Top) β (π½ β (TopOnββͺ πΎ) β πΎ β (TopOnββͺ π½))) | ||
Theorem | topgele 22819 | 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 22820 | The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn 4896). (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
β’ (π½ β (TopOnβ{π΄}) β π½ = π« {π΄}) | ||
Syntax | ctps 22821 | Syntax for the class of topological spaces. |
class TopSp | ||
Definition | df-topsp 22822 | Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.) |
β’ TopSp = {π β£ (TopOpenβπ) β (TopOnβ(Baseβπ))} | ||
Theorem | istps 22823 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π½ β (TopOnβπ΄)) | ||
Theorem | istps2 22824 | Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β (π½ β Top β§ π΄ = βͺ π½)) | ||
Theorem | tpsuni 22825 | The base set of a topological space. (Contributed by FL, 27-Jun-2014.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π΄ = βͺ π½) | ||
Theorem | tpstop 22826 | The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.) |
β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π½ β Top) | ||
Theorem | tpspropd 22827 | 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 22828 | 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 22829 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopSetβπΎ) β β’ (π½ β (TopOnβπ΄) β π½ = (TopOpenβπΎ)) | ||
Theorem | tsettps 22830 | 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 22831 | Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.) |
β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = π½ & β’ π΄ = βͺ π½ & β’ π½ β Top β β’ πΎ β TopSp | ||
Theorem | eltpsg 22832 | 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 22833 | Obsolete version of eltpsg 22832 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 22834 | 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 22835 | Syntax for the class of topological bases. |
class TopBases | ||
Definition | df-bases 22836* | Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 22838). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.) |
β’ TopBases = {π₯ β£ βπ¦ β π₯ βπ§ β π₯ (π¦ β© π§) β βͺ (π₯ β© π« (π¦ β© π§))} | ||
Theorem | isbasisg 22837* | Express the predicate "the set π΅ is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
β’ (π΅ β πΆ β (π΅ β TopBases β βπ₯ β π΅ βπ¦ β π΅ (π₯ β© π¦) β βͺ (π΅ β© π« (π₯ β© π¦)))) | ||
Theorem | isbasis2g 22838* | Express the predicate "the set π΅ is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
β’ (π΅ β πΆ β (π΅ β TopBases β βπ₯ β π΅ βπ¦ β π΅ βπ§ β (π₯ β© π¦)βπ€ β π΅ (π§ β π€ β§ π€ β (π₯ β© π¦)))) | ||
Theorem | isbasis3g 22839* | 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 22840 | Property of a basis. (Contributed by NM, 16-Jul-2006.) |
β’ ((π΅ β TopBases β§ πΆ β π΅ β§ π· β π΅) β (πΆ β© π·) β βͺ (π΅ β© π« (πΆ β© π·))) | ||
Theorem | basis2 22841* | Property of a basis. (Contributed by NM, 17-Jul-2006.) |
β’ (((π΅ β TopBases β§ πΆ β π΅) β§ (π· β π΅ β§ π΄ β (πΆ β© π·))) β βπ₯ β π΅ (π΄ β π₯ β§ π₯ β (πΆ β© π·))) | ||
Theorem | fiinbas 22842* | 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 22843 | 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 22844* | A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π β π β§ βπ₯ β π βπ¦ β π (π₯ = π¦ β¨ (π₯ β© π¦) = β )) β π β TopBases) | ||
Theorem | tgval 22845* | The topology generated by a basis. See also tgval2 22846 and tgval3 22853. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) | ||
Theorem | tgval2 22846* | Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 22859) that (topGenβπ΅) is indeed a topology (on βͺ π΅, see unitg 22857). See also tgval 22845 and tgval3 22853. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ (π₯ β βͺ π΅ β§ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯))}) | ||
Theorem | eltg 22847 | Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (π΄ β (topGenβπ΅) β π΄ β βͺ (π΅ β© π« π΄))) | ||
Theorem | eltg2 22848* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (π΄ β (topGenβπ΅) β (π΄ β βͺ π΅ β§ βπ₯ β π΄ βπ¦ β π΅ (π₯ β π¦ β§ π¦ β π΄)))) | ||
Theorem | eltg2b 22849* | 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 22850 | 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 22851 | The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ ((π΅ β π β§ π΄ β π΅) β βͺ π΄ β (topGenβπ΅)) | ||
Theorem | eltg3 22852* | 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 22853* | Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 22845 and tgval2 22846. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)}) | ||
Theorem | tg1 22854 | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
β’ (π΄ β (topGenβπ΅) β π΄ β βͺ π΅) | ||
Theorem | tg2 22855* | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
β’ ((π΄ β (topGenβπ΅) β§ πΆ β π΄) β βπ₯ β π΅ (πΆ β π₯ β§ π₯ β π΄)) | ||
Theorem | bastg 22856 | 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 22857 | 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 22858 | Subset relation for generated topologies. (Contributed by NM, 7-May-2007.) |
β’ ((πΆ β π β§ π΅ β πΆ) β (topGenβπ΅) β (topGenβπΆ)) | ||
Theorem | tgcl 22859 | Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.) |
β’ (π΅ β TopBases β (topGenβπ΅) β Top) | ||
Theorem | tgclb 22860 | The property tgcl 22859 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 22861 | A basis generates a topology on βͺ π΅. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (π΅ β TopBases β (topGenβπ΅) β (TopOnββͺ π΅)) | ||
Theorem | topbas 22862 | A topology is its own basis. (Contributed by NM, 17-Jul-2006.) |
β’ (π½ β Top β π½ β TopBases) | ||
Theorem | tgtop 22863 | A topology is its own basis. (Contributed by NM, 18-Jul-2006.) |
β’ (π½ β Top β (topGenβπ½) = π½) | ||
Theorem | eltop 22864 | Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.) |
β’ (π½ β Top β (π΄ β π½ β π΄ β βͺ (π½ β© π« π΄))) | ||
Theorem | eltop2 22865* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
β’ (π½ β Top β (π΄ β π½ β βπ₯ β π΄ βπ¦ β π½ (π₯ β π¦ β§ π¦ β π΄))) | ||
Theorem | eltop3 22866* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
β’ (π½ β Top β (π΄ β π½ β βπ₯(π₯ β π½ β§ π΄ = βͺ π₯))) | ||
Theorem | fibas 22867 | 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 22868 | 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 22869* | 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 22870 | The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.) |
β’ (π΅ β π β (topGenβ(topGenβπ΅)) = (topGenβπ΅)) | ||
Theorem | bastop 22871 | Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.) |
β’ (π΅ β TopBases β (π΅ β Top β (topGenβπ΅) = π΅)) | ||
Theorem | tgtop11 22872 | 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 22873 | 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 22874 | {β } is the only topology with one element. (Contributed by FL, 18-Aug-2008.) |
β’ (π½ β Top β (π½ β 1o β π½ = {β })) | ||
Theorem | en2top 22875 | 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 22876 | 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 22877* | 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 22878 | 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 22879* | 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 22880 | 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 22881 | 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 22882 | 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 22883* | 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 22884* | A version of bastop1 22883 that doesn't have π΅ β π½ in the antecedent. (Contributed by NM, 3-Feb-2008.) |
β’ (π½ β Top β ((topGenβπ΅) = π½ β (π΅ β π½ β§ βπ₯ β π½ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)))) | ||
Theorem | distop 22885 | 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 22886 | The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7755; an alternate proof uses indiscrete topologies (see indistop 22892) and the analogue of pwnex 7755 with pairs {β , π₯} instead of power sets π« π₯ (that analogue is also a consequence of abnex 7753). (Contributed by BJ, 2-May-2021.) |
β’ Top β V | ||
Theorem | distopon 22887 | The discrete topology on a set π΄, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π΄ β π β π« π΄ β (TopOnβπ΄)) | ||
Theorem | sn0topon 22888 | The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ {β } β (TopOnββ ) | ||
Theorem | sn0top 22889 | 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 22890 | A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ {β , ( I βπ΄)} = {β , π΄} | ||
Theorem | indistopon 22891 | The indiscrete topology on a set π΄. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π΄ β π β {β , π΄} β (TopOnβπ΄)) | ||
Theorem | indistop 22892 | 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 22893 | The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ( I βπ΄) = βͺ {β , π΄} | ||
Theorem | fctop 22894* | 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 22895* | The finite complement topology on a set π΄. Example 3 in [Munkres] p. 77. (This version of fctop 22894 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.) |
β’ (π΄ β π β {π₯ β π« π΄ β£ ((π΄ β π₯) βΊ Ο β¨ π₯ = β )} β (TopOnβπ΄)) | ||
Theorem | cctop 22896* | 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 22897* | The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β )} β (TopOnβπ΄)) | ||
Theorem | pptbas 22898* | 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 22899* | The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β (TopOnβπ΄)) | ||
Theorem | indistpsx 22900 | The indiscrete topology on a set π΄ expressed as a topological space, using explicit structure component references. Compare with indistps 22901 and indistps2 22902. The advantage of this version is that the actual function for the structure is evident, and df-ndx 17154 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 17172 and df-tset 17243 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 22901 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.) |
β’ π΄ β V & β’ πΎ = {β¨1, π΄β©, β¨9, {β , π΄}β©} β β’ πΎ β TopSp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |