Home | Metamath
Proof Explorer Theorem List (p. 223 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | topgele 22201 | 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 22202 | The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn 4856). (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
β’ (π½ β (TopOnβ{π΄}) β π½ = π« {π΄}) | ||
Syntax | ctps 22203 | Syntax for the class of topological spaces. |
class TopSp | ||
Definition | df-topsp 22204 | Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.) |
β’ TopSp = {π β£ (TopOpenβπ) β (TopOnβ(Baseβπ))} | ||
Theorem | istps 22205 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π½ β (TopOnβπ΄)) | ||
Theorem | istps2 22206 | Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β (π½ β Top β§ π΄ = βͺ π½)) | ||
Theorem | tpsuni 22207 | The base set of a topological space. (Contributed by FL, 27-Jun-2014.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π΄ = βͺ π½) | ||
Theorem | tpstop 22208 | The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.) |
β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π½ β Top) | ||
Theorem | tpspropd 22209 | 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 22210 | 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 22211 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopSetβπΎ) β β’ (π½ β (TopOnβπ΄) β π½ = (TopOpenβπΎ)) | ||
Theorem | tsettps 22212 | 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 22213 | Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.) |
β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = π½ & β’ π΄ = βͺ π½ & β’ π½ β Top β β’ πΎ β TopSp | ||
Theorem | eltpsg 22214 | 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 22215 | Obsolete version of eltpsg 22214 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 22216 | 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 22217 | Syntax for the class of topological bases. |
class TopBases | ||
Definition | df-bases 22218* | Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 22220). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.) |
β’ TopBases = {π₯ β£ βπ¦ β π₯ βπ§ β π₯ (π¦ β© π§) β βͺ (π₯ β© π« (π¦ β© π§))} | ||
Theorem | isbasisg 22219* | Express the predicate "the set π΅ is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
β’ (π΅ β πΆ β (π΅ β TopBases β βπ₯ β π΅ βπ¦ β π΅ (π₯ β© π¦) β βͺ (π΅ β© π« (π₯ β© π¦)))) | ||
Theorem | isbasis2g 22220* | Express the predicate "the set π΅ is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
β’ (π΅ β πΆ β (π΅ β TopBases β βπ₯ β π΅ βπ¦ β π΅ βπ§ β (π₯ β© π¦)βπ€ β π΅ (π§ β π€ β§ π€ β (π₯ β© π¦)))) | ||
Theorem | isbasis3g 22221* | 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 22222 | Property of a basis. (Contributed by NM, 16-Jul-2006.) |
β’ ((π΅ β TopBases β§ πΆ β π΅ β§ π· β π΅) β (πΆ β© π·) β βͺ (π΅ β© π« (πΆ β© π·))) | ||
Theorem | basis2 22223* | Property of a basis. (Contributed by NM, 17-Jul-2006.) |
β’ (((π΅ β TopBases β§ πΆ β π΅) β§ (π· β π΅ β§ π΄ β (πΆ β© π·))) β βπ₯ β π΅ (π΄ β π₯ β§ π₯ β (πΆ β© π·))) | ||
Theorem | fiinbas 22224* | 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 22225 | 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 22226* | A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π β π β§ βπ₯ β π βπ¦ β π (π₯ = π¦ β¨ (π₯ β© π¦) = β )) β π β TopBases) | ||
Theorem | tgval 22227* | The topology generated by a basis. See also tgval2 22228 and tgval3 22235. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) | ||
Theorem | tgval2 22228* | Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 22241) that (topGenβπ΅) is indeed a topology (on βͺ π΅, see unitg 22239). See also tgval 22227 and tgval3 22235. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ (π₯ β βͺ π΅ β§ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯))}) | ||
Theorem | eltg 22229 | Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (π΄ β (topGenβπ΅) β π΄ β βͺ (π΅ β© π« π΄))) | ||
Theorem | eltg2 22230* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (π΄ β (topGenβπ΅) β (π΄ β βͺ π΅ β§ βπ₯ β π΄ βπ¦ β π΅ (π₯ β π¦ β§ π¦ β π΄)))) | ||
Theorem | eltg2b 22231* | 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 22232 | 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 22233 | The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ ((π΅ β π β§ π΄ β π΅) β βͺ π΄ β (topGenβπ΅)) | ||
Theorem | eltg3 22234* | 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 22235* | Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 22227 and tgval2 22228. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)}) | ||
Theorem | tg1 22236 | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
β’ (π΄ β (topGenβπ΅) β π΄ β βͺ π΅) | ||
Theorem | tg2 22237* | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
β’ ((π΄ β (topGenβπ΅) β§ πΆ β π΄) β βπ₯ β π΅ (πΆ β π₯ β§ π₯ β π΄)) | ||
Theorem | bastg 22238 | 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 22239 | 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 22240 | Subset relation for generated topologies. (Contributed by NM, 7-May-2007.) |
β’ ((πΆ β π β§ π΅ β πΆ) β (topGenβπ΅) β (topGenβπΆ)) | ||
Theorem | tgcl 22241 | Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.) |
β’ (π΅ β TopBases β (topGenβπ΅) β Top) | ||
Theorem | tgclb 22242 | The property tgcl 22241 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 22243 | A basis generates a topology on βͺ π΅. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (π΅ β TopBases β (topGenβπ΅) β (TopOnββͺ π΅)) | ||
Theorem | topbas 22244 | A topology is its own basis. (Contributed by NM, 17-Jul-2006.) |
β’ (π½ β Top β π½ β TopBases) | ||
Theorem | tgtop 22245 | A topology is its own basis. (Contributed by NM, 18-Jul-2006.) |
β’ (π½ β Top β (topGenβπ½) = π½) | ||
Theorem | eltop 22246 | Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.) |
β’ (π½ β Top β (π΄ β π½ β π΄ β βͺ (π½ β© π« π΄))) | ||
Theorem | eltop2 22247* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
β’ (π½ β Top β (π΄ β π½ β βπ₯ β π΄ βπ¦ β π½ (π₯ β π¦ β§ π¦ β π΄))) | ||
Theorem | eltop3 22248* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
β’ (π½ β Top β (π΄ β π½ β βπ₯(π₯ β π½ β§ π΄ = βͺ π₯))) | ||
Theorem | fibas 22249 | 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 22250 | 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 22251* | 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 22252 | The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.) |
β’ (π΅ β π β (topGenβ(topGenβπ΅)) = (topGenβπ΅)) | ||
Theorem | bastop 22253 | Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.) |
β’ (π΅ β TopBases β (π΅ β Top β (topGenβπ΅) = π΅)) | ||
Theorem | tgtop11 22254 | 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 22255 | 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 22256 | {β } is the only topology with one element. (Contributed by FL, 18-Aug-2008.) |
β’ (π½ β Top β (π½ β 1o β π½ = {β })) | ||
Theorem | en2top 22257 | 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 22258 | 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 22259* | 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 22260 | 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 22261* | 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 22262 | 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 22263 | 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 22264 | 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 22265* | 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 22266* | A version of bastop1 22265 that doesn't have π΅ β π½ in the antecedent. (Contributed by NM, 3-Feb-2008.) |
β’ (π½ β Top β ((topGenβπ΅) = π½ β (π΅ β π½ β§ βπ₯ β π½ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)))) | ||
Theorem | distop 22267 | 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 22268 | The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7684; an alternate proof uses indiscrete topologies (see indistop 22274) and the analogue of pwnex 7684 with pairs {β , π₯} instead of power sets π« π₯ (that analogue is also a consequence of abnex 7682). (Contributed by BJ, 2-May-2021.) |
β’ Top β V | ||
Theorem | distopon 22269 | The discrete topology on a set π΄, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π΄ β π β π« π΄ β (TopOnβπ΄)) | ||
Theorem | sn0topon 22270 | The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ {β } β (TopOnββ ) | ||
Theorem | sn0top 22271 | 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 22272 | A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ {β , ( I βπ΄)} = {β , π΄} | ||
Theorem | indistopon 22273 | The indiscrete topology on a set π΄. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π΄ β π β {β , π΄} β (TopOnβπ΄)) | ||
Theorem | indistop 22274 | 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 22275 | The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ( I βπ΄) = βͺ {β , π΄} | ||
Theorem | fctop 22276* | 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 22277* | The finite complement topology on a set π΄. Example 3 in [Munkres] p. 77. (This version of fctop 22276 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.) |
β’ (π΄ β π β {π₯ β π« π΄ β£ ((π΄ β π₯) βΊ Ο β¨ π₯ = β )} β (TopOnβπ΄)) | ||
Theorem | cctop 22278* | 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 22279* | The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β )} β (TopOnβπ΄)) | ||
Theorem | pptbas 22280* | 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 22281* | The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β (TopOnβπ΄)) | ||
Theorem | indistpsx 22282 | The indiscrete topology on a set π΄ expressed as a topological space, using explicit structure component references. Compare with indistps 22283 and indistps2 22284. The advantage of this version is that the actual function for the structure is evident, and df-ndx 17001 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 17019 and df-tset 17087 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 22283 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.) |
β’ π΄ β V & β’ πΎ = {β¨1, π΄β©, β¨9, {β , π΄}β©} β β’ πΎ β TopSp | ||
Theorem | indistps 22283 | The indiscrete topology on a set π΄ expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 22282 is that it is independent of the indices of the component definitions df-base 17019 and df-tset 17087, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 22284 is that it is easy to eliminate the hypotheses with eqid 2738 and vtoclg 3524 to result in a closed theorem. Theorems indistpsALT 22285 and indistps2ALT 22287 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 22284 | The indiscrete topology on a set π΄ expressed as a topological space, using direct component assignments. Compare with indistps 22283. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 22285 and indistps2ALT 22287 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.) |
β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = {β , π΄} β β’ πΎ β TopSp | ||
Theorem | indistpsALT 22285 | The indiscrete topology on a set π΄ expressed as a topological space. Here we show how to derive the structural version indistps 22283 from the direct component assignment version indistps2 22284. (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 22286 | Obsolete proof of indistpsALT 22285 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 22283 from the direct component assignment version indistps2 22284. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ β V & β’ πΎ = {β¨(Baseβndx), π΄β©, β¨(TopSetβndx), {β , π΄}β©} β β’ πΎ β TopSp | ||
Theorem | indistps2ALT 22287 | 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 22284 from the structural version indistps 22283. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = {β , π΄} β β’ πΎ β TopSp | ||
Theorem | distps 22288 | 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 22289 | Extend class notation with the set of closed sets of a topology. |
class Clsd | ||
Syntax | cnt 22290 | Extend class notation with interior of a subset of a topology base set. |
class int | ||
Syntax | ccl 22291 | Extend class notation with closure of a subset of a topology base set. |
class cls | ||
Definition | df-cld 22292* | 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 22293* | Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 22309. (Contributed by NM, 10-Sep-2006.) |
β’ int = (π β Top β¦ (π₯ β π« βͺ π β¦ βͺ (π β© π« π₯))) | ||
Definition | df-cls 22294* | Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 22310. (Contributed by NM, 3-Oct-2006.) |
β’ cls = (π β Top β¦ (π₯ β π« βͺ π β¦ β© {π¦ β (Clsdβπ) β£ π₯ β π¦})) | ||
Theorem | fncld 22295 | The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ Clsd Fn Top | ||
Theorem | cldval 22296* | 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 22297* | 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 22298* | 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 22299 | Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (πΆ β (Clsdβπ½) β π½ β Top) | ||
Theorem | iscld 22300 | The predicate "the class π is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ (π½ β Top β (π β (Clsdβπ½) β (π β π β§ (π β π) β π½))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |