![]() |
Intuitionistic Logic Explorer Theorem List (p. 136 of 149) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-top 13501* |
Define the class of topologies. It is a proper class. See istopg 13502 and
istopfin 13503 for the corresponding characterizations,
using respectively
binary intersections like in this definition and nonempty finite
intersections.
The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.) |
β’ Top = {π₯ β£ (βπ¦ β π« π₯βͺ π¦ β π₯ β§ βπ¦ β π₯ βπ§ β π₯ (π¦ β© π§) β π₯)} | ||
Theorem | istopg 13502* |
Express the predicate "π½ is a topology". See istopfin 13503 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 | istopfin 13503* | Express the predicate "π½ is a topology" using nonempty finite intersections instead of binary intersections as in istopg 13502. It is not clear we can prove the converse without adding additional conditions. (Contributed by NM, 19-Jul-2006.) (Revised by Jim Kingdon, 14-Jan-2023.) |
β’ (π½ β Top β (βπ₯(π₯ β π½ β βͺ π₯ β π½) β§ βπ₯((π₯ β π½ β§ π₯ β β β§ π₯ β Fin) β β© π₯ β π½))) | ||
Theorem | uniopn 13504 | 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 13505* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) |
β’ ((π½ β Top β§ βπ₯ β π΄ π΅ β π½) β βͺ π₯ β π΄ π΅ β π½) | ||
Theorem | inopn 13506 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ β© π΅) β π½) | ||
Theorem | fiinopn 13507 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) |
β’ (π½ β Top β ((π΄ β π½ β§ π΄ β β β§ π΄ β Fin) β β© π΄ β π½)) | ||
Theorem | unopn 13508 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ βͺ π΅) β π½) | ||
Theorem | 0opn 13509 | The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.) |
β’ (π½ β Top β β β π½) | ||
Theorem | 0ntop 13510 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) |
β’ Β¬ β β Top | ||
Theorem | topopn 13511 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
β’ π = βͺ π½ β β’ (π½ β Top β π β π½) | ||
Theorem | eltopss 13512 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π½) β π΄ β π) | ||
Syntax | ctopon 13513 | Syntax for the function of topologies on sets. |
class TopOn | ||
Definition | df-topon 13514* | 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 | funtopon 13515 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) |
β’ Fun TopOn | ||
Theorem | istopon 13516 | 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 13517 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π½ β Top) | ||
Theorem | toponuni 13518 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) | ||
Theorem | topontopi 13519 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π½ β (TopOnβπ΅) β β’ π½ β Top | ||
Theorem | toponunii 13520 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π½ β (TopOnβπ΅) β β’ π΅ = βͺ π½ | ||
Theorem | toptopon 13521 | Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β Top β π½ β (TopOnβπ)) | ||
Theorem | toptopon2 13522 | 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 13523 | A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) |
β’ (π½ β (TopOnβπ) β π½ β (TopOnββͺ π½)) | ||
Theorem | toponrestid 13524 | 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 | toponsspwpwg 13525 | The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) (Revised by Jim Kingdon, 16-Jan-2023.) |
β’ (π΄ β π β (TopOnβπ΄) β π« π« π΄) | ||
Theorem | dmtopon 13526 | The domain of TopOn is V. (Contributed by BJ, 29-Apr-2021.) |
β’ dom TopOn = V | ||
Theorem | fntopon 13527 | The class TopOn is a function with domain V. (Contributed by BJ, 29-Apr-2021.) |
β’ TopOn Fn V | ||
Theorem | toponmax 13528 | The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π΅ β π½) | ||
Theorem | toponss 13529 | A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π½) β π΄ β π) | ||
Theorem | toponcom 13530 | 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 13531 | Biconditional form of toponcom 13530. (Contributed by BJ, 5-Dec-2021.) |
β’ ((π½ β Top β§ πΎ β Top) β (π½ β (TopOnββͺ πΎ) β πΎ β (TopOnββͺ π½))) | ||
Theorem | topgele 13532 | 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βπ) β ({β , π} β π½ β§ π½ β π« π)) | ||
Syntax | ctps 13533 | Syntax for the class of topological spaces. |
class TopSp | ||
Definition | df-topsp 13534 | Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.) |
β’ TopSp = {π β£ (TopOpenβπ) β (TopOnβ(Baseβπ))} | ||
Theorem | istps 13535 | Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π½ β (TopOnβπ΄)) | ||
Theorem | istps2 13536 | Express the predicate "is a topological space". (Contributed by NM, 20-Oct-2012.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β (π½ β Top β§ π΄ = βͺ π½)) | ||
Theorem | tpsuni 13537 | The base set of a topological space. (Contributed by FL, 27-Jun-2014.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π΄ = βͺ π½) | ||
Theorem | tpstop 13538 | The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.) |
β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π½ β Top) | ||
Theorem | tpspropd 13539 | 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 | topontopn 13540 | Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π΄ = (BaseβπΎ) & β’ π½ = (TopSetβπΎ) β β’ (π½ β (TopOnβπ΄) β π½ = (TopOpenβπΎ)) | ||
Theorem | tsettps 13541 | 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 13542 | Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.) |
β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = π½ & β’ π΄ = βͺ π½ & β’ π½ β Top β β’ πΎ β TopSp | ||
Theorem | eltpsg 13543 | Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ πΎ = {β¨(Baseβndx), π΄β©, β¨(TopSetβndx), π½β©} β β’ (π½ β (TopOnβπ΄) β πΎ β TopSp) | ||
Theorem | eltpsi 13544 | 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 13545 | Syntax for the class of topological bases. |
class TopBases | ||
Definition | df-bases 13546* | Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 13548). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.) |
β’ TopBases = {π₯ β£ βπ¦ β π₯ βπ§ β π₯ (π¦ β© π§) β βͺ (π₯ β© π« (π¦ β© π§))} | ||
Theorem | isbasisg 13547* | Express the predicate "the set π΅ is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
β’ (π΅ β πΆ β (π΅ β TopBases β βπ₯ β π΅ βπ¦ β π΅ (π₯ β© π¦) β βͺ (π΅ β© π« (π₯ β© π¦)))) | ||
Theorem | isbasis2g 13548* | Express the predicate "the set π΅ is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
β’ (π΅ β πΆ β (π΅ β TopBases β βπ₯ β π΅ βπ¦ β π΅ βπ§ β (π₯ β© π¦)βπ€ β π΅ (π§ β π€ β§ π€ β (π₯ β© π¦)))) | ||
Theorem | isbasis3g 13549* | 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 13550 | Property of a basis. (Contributed by NM, 16-Jul-2006.) |
β’ ((π΅ β TopBases β§ πΆ β π΅ β§ π· β π΅) β (πΆ β© π·) β βͺ (π΅ β© π« (πΆ β© π·))) | ||
Theorem | basis2 13551* | Property of a basis. (Contributed by NM, 17-Jul-2006.) |
β’ (((π΅ β TopBases β§ πΆ β π΅) β§ (π· β π΅ β§ π΄ β (πΆ β© π·))) β βπ₯ β π΅ (π΄ β π₯ β§ π₯ β (πΆ β© π·))) | ||
Theorem | fiinbas 13552* | 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 | baspartn 13553* | A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π β π β§ βπ₯ β π βπ¦ β π (π₯ = π¦ β¨ (π₯ β© π¦) = β )) β π β TopBases) | ||
Theorem | tgval2 13554* | Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 13567) that (topGenβπ΅) is indeed a topology (on βͺ π΅, see unitg 13565). See also tgval 12711 and tgval3 13561. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ (π₯ β βͺ π΅ β§ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯))}) | ||
Theorem | eltg 13555 | Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (π΄ β (topGenβπ΅) β π΄ β βͺ (π΅ β© π« π΄))) | ||
Theorem | eltg2 13556* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (π΄ β (topGenβπ΅) β (π΄ β βͺ π΅ β§ βπ₯ β π΄ βπ¦ β π΅ (π₯ β π¦ β§ π¦ β π΄)))) | ||
Theorem | eltg2b 13557* | 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 13558 | 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 13559 | The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ ((π΅ β π β§ π΄ β π΅) β βͺ π΄ β (topGenβπ΅)) | ||
Theorem | eltg3 13560* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.) |
β’ (π΅ β π β (π΄ β (topGenβπ΅) β βπ₯(π₯ β π΅ β§ π΄ = βͺ π₯))) | ||
Theorem | tgval3 13561* | Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 12711 and tgval2 13554. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)}) | ||
Theorem | tg1 13562 | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
β’ (π΄ β (topGenβπ΅) β π΄ β βͺ π΅) | ||
Theorem | tg2 13563* | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
β’ ((π΄ β (topGenβπ΅) β§ πΆ β π΄) β βπ₯ β π΅ (πΆ β π₯ β§ π₯ β π΄)) | ||
Theorem | bastg 13564 | 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 13565 | 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 13566 | Subset relation for generated topologies. (Contributed by NM, 7-May-2007.) |
β’ ((πΆ β π β§ π΅ β πΆ) β (topGenβπ΅) β (topGenβπΆ)) | ||
Theorem | tgcl 13567 | Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.) |
β’ (π΅ β TopBases β (topGenβπ΅) β Top) | ||
Theorem | tgclb 13568 | The property tgcl 13567 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 13569 | A basis generates a topology on βͺ π΅. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (π΅ β TopBases β (topGenβπ΅) β (TopOnββͺ π΅)) | ||
Theorem | topbas 13570 | A topology is its own basis. (Contributed by NM, 17-Jul-2006.) |
β’ (π½ β Top β π½ β TopBases) | ||
Theorem | tgtop 13571 | A topology is its own basis. (Contributed by NM, 18-Jul-2006.) |
β’ (π½ β Top β (topGenβπ½) = π½) | ||
Theorem | eltop 13572 | Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.) |
β’ (π½ β Top β (π΄ β π½ β π΄ β βͺ (π½ β© π« π΄))) | ||
Theorem | eltop2 13573* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
β’ (π½ β Top β (π΄ β π½ β βπ₯ β π΄ βπ¦ β π½ (π₯ β π¦ β§ π¦ β π΄))) | ||
Theorem | eltop3 13574* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
β’ (π½ β Top β (π΄ β π½ β βπ₯(π₯ β π½ β§ π΄ = βͺ π₯))) | ||
Theorem | tgdom 13575 | 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 13576* | 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 13577 | The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.) |
β’ (π΅ β π β (topGenβ(topGenβπ΅)) = (topGenβπ΅)) | ||
Theorem | bastop 13578 | Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.) |
β’ (π΅ β TopBases β (π΅ β Top β (topGenβπ΅) = π΅)) | ||
Theorem | tgtop11 13579 | The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.) |
β’ ((π½ β Top β§ πΎ β Top β§ (topGenβπ½) = (topGenβπΎ)) β π½ = πΎ) | ||
Theorem | en1top 13580 | {β } is the only topology with one element. (Contributed by FL, 18-Aug-2008.) |
β’ (π½ β Top β (π½ β 1o β π½ = {β })) | ||
Theorem | tgss3 13581 | 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 13582* | 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 13583 | 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 13584* | 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 | 2basgeng 13585 | Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon, 5-Mar-2023.) |
β’ ((π΅ β π β§ π΅ β πΆ β§ πΆ β (topGenβπ΅)) β (topGenβπ΅) = (topGenβπΆ)) | ||
Theorem | bastop1 13586* | 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 13587* | A version of bastop1 13586 that doesn't have π΅ β π½ in the antecedent. (Contributed by NM, 3-Feb-2008.) |
β’ (π½ β Top β ((topGenβπ΅) = π½ β (π΅ β π½ β§ βπ₯ β π½ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)))) | ||
Theorem | distop 13588 | 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 13589 | The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 4450. (Contributed by BJ, 2-May-2021.) |
β’ Top β V | ||
Theorem | distopon 13590 | The discrete topology on a set π΄, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π΄ β π β π« π΄ β (TopOnβπ΄)) | ||
Theorem | sn0topon 13591 | The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ {β } β (TopOnββ ) | ||
Theorem | sn0top 13592 | 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 | epttop 13593* | The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β (TopOnβπ΄)) | ||
Theorem | distps 13594 | 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 13595 | Extend class notation with the set of closed sets of a topology. |
class Clsd | ||
Syntax | cnt 13596 | Extend class notation with interior of a subset of a topology base set. |
class int | ||
Syntax | ccl 13597 | Extend class notation with closure of a subset of a topology base set. |
class cls | ||
Definition | df-cld 13598* | 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 13599* | Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 13613. (Contributed by NM, 10-Sep-2006.) |
β’ int = (π β Top β¦ (π₯ β π« βͺ π β¦ βͺ (π β© π« π₯))) | ||
Definition | df-cls 13600* | Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 13614. (Contributed by NM, 3-Oct-2006.) |
β’ cls = (π β Top β¦ (π₯ β π« βͺ π β¦ β© {π¦ β (Clsdβπ) β£ π₯ β π¦})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |