![]() |
Metamath
Proof Explorer Theorem List (p. 228 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tgdom 22701 | 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 22702* | 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 22703 | The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.) |
β’ (π΅ β π β (topGenβ(topGenβπ΅)) = (topGenβπ΅)) | ||
Theorem | bastop 22704 | Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.) |
β’ (π΅ β TopBases β (π΅ β Top β (topGenβπ΅) = π΅)) | ||
Theorem | tgtop11 22705 | 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 22706 | 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 22707 | {β } is the only topology with one element. (Contributed by FL, 18-Aug-2008.) |
β’ (π½ β Top β (π½ β 1o β π½ = {β })) | ||
Theorem | en2top 22708 | 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 22709 | 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 22710* | 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 22711 | 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 22712* | 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 22713 | 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 22714 | 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 22715 | 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 22716* | 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 22717* | A version of bastop1 22716 that doesn't have π΅ β π½ in the antecedent. (Contributed by NM, 3-Feb-2008.) |
β’ (π½ β Top β ((topGenβπ΅) = π½ β (π΅ β π½ β§ βπ₯ β π½ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)))) | ||
Theorem | distop 22718 | 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 22719 | The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7748; an alternate proof uses indiscrete topologies (see indistop 22725) and the analogue of pwnex 7748 with pairs {β , π₯} instead of power sets π« π₯ (that analogue is also a consequence of abnex 7746). (Contributed by BJ, 2-May-2021.) |
β’ Top β V | ||
Theorem | distopon 22720 | The discrete topology on a set π΄, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π΄ β π β π« π΄ β (TopOnβπ΄)) | ||
Theorem | sn0topon 22721 | The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ {β } β (TopOnββ ) | ||
Theorem | sn0top 22722 | 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 22723 | A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ {β , ( I βπ΄)} = {β , π΄} | ||
Theorem | indistopon 22724 | The indiscrete topology on a set π΄. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π΄ β π β {β , π΄} β (TopOnβπ΄)) | ||
Theorem | indistop 22725 | 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 22726 | The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ( I βπ΄) = βͺ {β , π΄} | ||
Theorem | fctop 22727* | 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 22728* | The finite complement topology on a set π΄. Example 3 in [Munkres] p. 77. (This version of fctop 22727 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.) |
β’ (π΄ β π β {π₯ β π« π΄ β£ ((π΄ β π₯) βΊ Ο β¨ π₯ = β )} β (TopOnβπ΄)) | ||
Theorem | cctop 22729* | 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 22730* | The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β )} β (TopOnβπ΄)) | ||
Theorem | pptbas 22731* | 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 22732* | The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β (TopOnβπ΄)) | ||
Theorem | indistpsx 22733 | The indiscrete topology on a set π΄ expressed as a topological space, using explicit structure component references. Compare with indistps 22734 and indistps2 22735. The advantage of this version is that the actual function for the structure is evident, and df-ndx 17131 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 17149 and df-tset 17220 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 22734 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.) |
β’ π΄ β V & β’ πΎ = {β¨1, π΄β©, β¨9, {β , π΄}β©} β β’ πΎ β TopSp | ||
Theorem | indistps 22734 | The indiscrete topology on a set π΄ expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 22733 is that it is independent of the indices of the component definitions df-base 17149 and df-tset 17220, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 22735 is that it is easy to eliminate the hypotheses with eqid 2730 and vtoclg 3541 to result in a closed theorem. Theorems indistpsALT 22736 and indistps2ALT 22738 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 22735 | The indiscrete topology on a set π΄ expressed as a topological space, using direct component assignments. Compare with indistps 22734. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 22736 and indistps2ALT 22738 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.) |
β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = {β , π΄} β β’ πΎ β TopSp | ||
Theorem | indistpsALT 22736 | The indiscrete topology on a set π΄ expressed as a topological space. Here we show how to derive the structural version indistps 22734 from the direct component assignment version indistps2 22735. (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 22737 | Obsolete version of indistpsALT 22736 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 22734 from the direct component assignment version indistps2 22735. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ β V & β’ πΎ = {β¨(Baseβndx), π΄β©, β¨(TopSetβndx), {β , π΄}β©} β β’ πΎ β TopSp | ||
Theorem | indistps2ALT 22738 | 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 22735 from the structural version indistps 22734. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = {β , π΄} β β’ πΎ β TopSp | ||
Theorem | distps 22739 | 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 22740 | Extend class notation with the set of closed sets of a topology. |
class Clsd | ||
Syntax | cnt 22741 | Extend class notation with interior of a subset of a topology base set. |
class int | ||
Syntax | ccl 22742 | Extend class notation with closure of a subset of a topology base set. |
class cls | ||
Definition | df-cld 22743* | 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 22744* | Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 22760. (Contributed by NM, 10-Sep-2006.) |
β’ int = (π β Top β¦ (π₯ β π« βͺ π β¦ βͺ (π β© π« π₯))) | ||
Definition | df-cls 22745* | Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 22761. (Contributed by NM, 3-Oct-2006.) |
β’ cls = (π β Top β¦ (π₯ β π« βͺ π β¦ β© {π¦ β (Clsdβπ) β£ π₯ β π¦})) | ||
Theorem | fncld 22746 | The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ Clsd Fn Top | ||
Theorem | cldval 22747* | 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 22748* | 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 22749* | 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 22750 | Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (πΆ β (Clsdβπ½) β π½ β Top) | ||
Theorem | iscld 22751 | The predicate "the class π is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ (π½ β Top β (π β (Clsdβπ½) β (π β π β§ (π β π) β π½))) | ||
Theorem | iscld2 22752 | A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β (Clsdβπ½) β (π β π) β π½)) | ||
Theorem | cldss 22753 | A closed set is a subset of the underlying set of a topology. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.) |
β’ π = βͺ π½ β β’ (π β (Clsdβπ½) β π β π) | ||
Theorem | cldss2 22754 | The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.) |
β’ π = βͺ π½ β β’ (Clsdβπ½) β π« π | ||
Theorem | cldopn 22755 | The complement of a closed set is open. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.) |
β’ π = βͺ π½ β β’ (π β (Clsdβπ½) β (π β π) β π½) | ||
Theorem | isopn2 22756 | A subset of the underlying set of a topology is open iff its complement is closed. (Contributed by NM, 4-Oct-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β π½ β (π β π) β (Clsdβπ½))) | ||
Theorem | opncld 22757 | The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π½) β (π β π) β (Clsdβπ½)) | ||
Theorem | difopn 22758 | The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.) |
β’ π = βͺ π½ β β’ ((π΄ β π½ β§ π΅ β (Clsdβπ½)) β (π΄ β π΅) β π½) | ||
Theorem | topcld 22759 | The underlying set of a topology is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 3-Oct-2006.) |
β’ π = βͺ π½ β β’ (π½ β Top β π β (Clsdβπ½)) | ||
Theorem | ntrval 22760 | The interior of a subset of a topology's base set is the union of all the open sets it includes. Definition of interior of [Munkres] p. 94. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) = βͺ (π½ β© π« π)) | ||
Theorem | clsval 22761* | The closure of a subset of a topology's base set is the intersection of all the closed sets that include it. Definition of closure of [Munkres] p. 94. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) = β© {π₯ β (Clsdβπ½) β£ π β π₯}) | ||
Theorem | 0cld 22762 | The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 4-Oct-2006.) |
β’ (π½ β Top β β β (Clsdβπ½)) | ||
Theorem | iincld 22763* | The indexed intersection of a collection π΅(π₯) of closed sets is closed. Theorem 6.1(2) of [Munkres] p. 93. (Contributed by NM, 5-Oct-2006.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β β β§ βπ₯ β π΄ π΅ β (Clsdβπ½)) β β© π₯ β π΄ π΅ β (Clsdβπ½)) | ||
Theorem | intcld 22764 | The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.) |
β’ ((π΄ β β β§ π΄ β (Clsdβπ½)) β β© π΄ β (Clsdβπ½)) | ||
Theorem | uncld 22765 | The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of [Munkres] p. 93. (Contributed by NM, 5-Oct-2006.) |
β’ ((π΄ β (Clsdβπ½) β§ π΅ β (Clsdβπ½)) β (π΄ βͺ π΅) β (Clsdβπ½)) | ||
Theorem | cldcls 22766 | A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.) |
β’ (π β (Clsdβπ½) β ((clsβπ½)βπ) = π) | ||
Theorem | incld 22767 | The intersection of two closed sets is closed. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β (Clsdβπ½) β§ π΅ β (Clsdβπ½)) β (π΄ β© π΅) β (Clsdβπ½)) | ||
Theorem | riincld 22768* | An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ βπ₯ β π΄ π΅ β (Clsdβπ½)) β (π β© β© π₯ β π΄ π΅) β (Clsdβπ½)) | ||
Theorem | iuncld 22769* | A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β Fin β§ βπ₯ β π΄ π΅ β (Clsdβπ½)) β βͺ π₯ β π΄ π΅ β (Clsdβπ½)) | ||
Theorem | unicld 22770 | A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β Fin β§ π΄ β (Clsdβπ½)) β βͺ π΄ β (Clsdβπ½)) | ||
Theorem | clscld 22771 | The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β (Clsdβπ½)) | ||
Theorem | clsf 22772 | The closure function is a function from subsets of the base to closed sets. (Contributed by Mario Carneiro, 11-Apr-2015.) |
β’ π = βͺ π½ β β’ (π½ β Top β (clsβπ½):π« πβΆ(Clsdβπ½)) | ||
Theorem | ntropn 22773 | The interior of a subset of a topology's underlying set is open. (Contributed by NM, 11-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π½) | ||
Theorem | clsval2 22774 | Express closure in terms of interior. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) = (π β ((intβπ½)β(π β π)))) | ||
Theorem | ntrval2 22775 | Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) = (π β ((clsβπ½)β(π β π)))) | ||
Theorem | ntrdif 22776 | An interior of a complement is the complement of the closure. This set is also known as the exterior of π΄. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β ((intβπ½)β(π β π΄)) = (π β ((clsβπ½)βπ΄))) | ||
Theorem | clsdif 22777 | A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β ((clsβπ½)β(π β π΄)) = (π β ((intβπ½)βπ΄))) | ||
Theorem | clsss 22778 | Subset relationship for closure. (Contributed by NM, 10-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β ((clsβπ½)βπ) β ((clsβπ½)βπ)) | ||
Theorem | ntrss 22779 | Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β ((intβπ½)βπ) β ((intβπ½)βπ)) | ||
Theorem | sscls 22780 | A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β π β ((clsβπ½)βπ)) | ||
Theorem | ntrss2 22781 | A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π) | ||
Theorem | ssntr 22782 | An open subset of a set is a subset of the set's interior. (Contributed by Jeff Hankins, 31-Aug-2009.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π β π) β§ (π β π½ β§ π β π)) β π β ((intβπ½)βπ)) | ||
Theorem | clsss3 22783 | The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β π) | ||
Theorem | ntrss3 22784 | The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π) | ||
Theorem | ntrin 22785 | A pairwise intersection of interiors is the interior of the intersection. This does not always hold for arbitrary intersections. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β(π΄ β© π΅)) = (((intβπ½)βπ΄) β© ((intβπ½)βπ΅))) | ||
Theorem | cmclsopn 22786 | The complement of a closure is open. (Contributed by NM, 11-Sep-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((clsβπ½)βπ)) β π½) | ||
Theorem | cmntrcld 22787 | The complement of an interior is closed. (Contributed by NM, 1-Oct-2007.) (Proof shortened by OpenAI, 3-Jul-2020.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((intβπ½)βπ)) β (Clsdβπ½)) | ||
Theorem | iscld3 22788 | A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β (Clsdβπ½) β ((clsβπ½)βπ) = π)) | ||
Theorem | iscld4 22789 | A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β (Clsdβπ½) β ((clsβπ½)βπ) β π)) | ||
Theorem | isopn3 22790 | A subset is open iff it equals its own interior. (Contributed by NM, 9-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β π½ β ((intβπ½)βπ) = π)) | ||
Theorem | clsidm 22791 | The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)β((clsβπ½)βπ)) = ((clsβπ½)βπ)) | ||
Theorem | ntridm 22792 | The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)β((intβπ½)βπ)) = ((intβπ½)βπ)) | ||
Theorem | clstop 22793 | The closure of a topology's underlying set is the entire set. (Contributed by NM, 5-Oct-2007.) (Proof shortened by Jim Kingdon, 11-Mar-2023.) |
β’ π = βͺ π½ β β’ (π½ β Top β ((clsβπ½)βπ) = π) | ||
Theorem | ntrtop 22794 | The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.) |
β’ π = βͺ π½ β β’ (π½ β Top β ((intβπ½)βπ) = π) | ||
Theorem | 0ntr 22795 | A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π β β ) β§ (π β π β§ ((intβπ½)βπ) = β )) β (π β π) β β ) | ||
Theorem | clsss2 22796 | If a subset is included in a closed set, so is the subset's closure. (Contributed by NM, 22-Feb-2007.) |
β’ π = βͺ π½ β β’ ((πΆ β (Clsdβπ½) β§ π β πΆ) β ((clsβπ½)βπ) β πΆ) | ||
Theorem | elcls 22797* | Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((clsβπ½)βπ) β βπ₯ β π½ (π β π₯ β (π₯ β© π) β β ))) | ||
Theorem | elcls2 22798* | Membership in a closure. (Contributed by NM, 5-Mar-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((clsβπ½)βπ) β (π β π β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β )))) | ||
Theorem | clsndisj 22799 | Any open set containing a point that belongs to the closure of a subset intersects the subset. One direction of Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 26-Feb-2007.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π β π β§ π β ((clsβπ½)βπ)) β§ (π β π½ β§ π β π)) β (π β© π) β β ) | ||
Theorem | ntrcls0 22800 | A subset whose closure has an empty interior also has an empty interior. (Contributed by NM, 4-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ ((intβπ½)β((clsβπ½)βπ)) = β ) β ((intβπ½)βπ) = β ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |