![]() |
Metamath
Proof Explorer Theorem List (p. 230 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 | indistps 22901 | The indiscrete topology on a set π΄ expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 22900 is that it is independent of the indices of the component definitions df-base 17172 and df-tset 17243, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 22902 is that it is easy to eliminate the hypotheses with eqid 2727 and vtoclg 3538 to result in a closed theorem. Theorems indistpsALT 22903 and indistps2ALT 22905 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 22902 | The indiscrete topology on a set π΄ expressed as a topological space, using direct component assignments. Compare with indistps 22901. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 22903 and indistps2ALT 22905 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.) |
β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = {β , π΄} β β’ πΎ β TopSp | ||
Theorem | indistpsALT 22903 | The indiscrete topology on a set π΄ expressed as a topological space. Here we show how to derive the structural version indistps 22901 from the direct component assignment version indistps2 22902. (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 22904 | Obsolete version of indistpsALT 22903 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 22901 from the direct component assignment version indistps2 22902. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ β V & β’ πΎ = {β¨(Baseβndx), π΄β©, β¨(TopSetβndx), {β , π΄}β©} β β’ πΎ β TopSp | ||
Theorem | indistps2ALT 22905 | 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 22902 from the structural version indistps 22901. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = {β , π΄} β β’ πΎ β TopSp | ||
Theorem | distps 22906 | 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 22907 | Extend class notation with the set of closed sets of a topology. |
class Clsd | ||
Syntax | cnt 22908 | Extend class notation with interior of a subset of a topology base set. |
class int | ||
Syntax | ccl 22909 | Extend class notation with closure of a subset of a topology base set. |
class cls | ||
Definition | df-cld 22910* | 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 22911* | Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 22927. (Contributed by NM, 10-Sep-2006.) |
β’ int = (π β Top β¦ (π₯ β π« βͺ π β¦ βͺ (π β© π« π₯))) | ||
Definition | df-cls 22912* | Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 22928. (Contributed by NM, 3-Oct-2006.) |
β’ cls = (π β Top β¦ (π₯ β π« βͺ π β¦ β© {π¦ β (Clsdβπ) β£ π₯ β π¦})) | ||
Theorem | fncld 22913 | The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ Clsd Fn Top | ||
Theorem | cldval 22914* | 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 22915* | 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 22916* | 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 22917 | Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (πΆ β (Clsdβπ½) β π½ β Top) | ||
Theorem | iscld 22918 | 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 22919 | 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 22920 | 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 22921 | The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.) |
β’ π = βͺ π½ β β’ (Clsdβπ½) β π« π | ||
Theorem | cldopn 22922 | 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 22923 | 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 22924 | The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π½) β (π β π) β (Clsdβπ½)) | ||
Theorem | difopn 22925 | The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.) |
β’ π = βͺ π½ β β’ ((π΄ β π½ β§ π΅ β (Clsdβπ½)) β (π΄ β π΅) β π½) | ||
Theorem | topcld 22926 | 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 22927 | 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 22928* | 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 22929 | 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 22930* | 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 22931 | The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.) |
β’ ((π΄ β β β§ π΄ β (Clsdβπ½)) β β© π΄ β (Clsdβπ½)) | ||
Theorem | uncld 22932 | 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 22933 | A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.) |
β’ (π β (Clsdβπ½) β ((clsβπ½)βπ) = π) | ||
Theorem | incld 22934 | 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 22935* | An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ βπ₯ β π΄ π΅ β (Clsdβπ½)) β (π β© β© π₯ β π΄ π΅) β (Clsdβπ½)) | ||
Theorem | iuncld 22936* | A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β Fin β§ βπ₯ β π΄ π΅ β (Clsdβπ½)) β βͺ π₯ β π΄ π΅ β (Clsdβπ½)) | ||
Theorem | unicld 22937 | A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β Fin β§ π΄ β (Clsdβπ½)) β βͺ π΄ β (Clsdβπ½)) | ||
Theorem | clscld 22938 | The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β (Clsdβπ½)) | ||
Theorem | clsf 22939 | 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 22940 | 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 22941 | Express closure in terms of interior. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) = (π β ((intβπ½)β(π β π)))) | ||
Theorem | ntrval2 22942 | Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) = (π β ((clsβπ½)β(π β π)))) | ||
Theorem | ntrdif 22943 | 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 22944 | A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β ((clsβπ½)β(π β π΄)) = (π β ((intβπ½)βπ΄))) | ||
Theorem | clsss 22945 | Subset relationship for closure. (Contributed by NM, 10-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β ((clsβπ½)βπ) β ((clsβπ½)βπ)) | ||
Theorem | ntrss 22946 | Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β ((intβπ½)βπ) β ((intβπ½)βπ)) | ||
Theorem | sscls 22947 | A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β π β ((clsβπ½)βπ)) | ||
Theorem | ntrss2 22948 | A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π) | ||
Theorem | ssntr 22949 | 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 22950 | The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β π) | ||
Theorem | ntrss3 22951 | The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) β π) | ||
Theorem | ntrin 22952 | 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 22953 | The complement of a closure is open. (Contributed by NM, 11-Sep-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((clsβπ½)βπ)) β π½) | ||
Theorem | cmntrcld 22954 | 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 22955 | A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β (Clsdβπ½) β ((clsβπ½)βπ) = π)) | ||
Theorem | iscld4 22956 | A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β (Clsdβπ½) β ((clsβπ½)βπ) β π)) | ||
Theorem | isopn3 22957 | 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 22958 | The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)β((clsβπ½)βπ)) = ((clsβπ½)βπ)) | ||
Theorem | ntridm 22959 | The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((intβπ½)β((intβπ½)βπ)) = ((intβπ½)βπ)) | ||
Theorem | clstop 22960 | 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 22961 | The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.) |
β’ π = βͺ π½ β β’ (π½ β Top β ((intβπ½)βπ) = π) | ||
Theorem | 0ntr 22962 | A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π β β ) β§ (π β π β§ ((intβπ½)βπ) = β )) β (π β π) β β ) | ||
Theorem | clsss2 22963 | 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 22964* | Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((clsβπ½)βπ) β βπ₯ β π½ (π β π₯ β (π₯ β© π) β β ))) | ||
Theorem | elcls2 22965* | Membership in a closure. (Contributed by NM, 5-Mar-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((clsβπ½)βπ) β (π β π β§ βπ₯ β π½ (π β π₯ β (π₯ β© π) β β )))) | ||
Theorem | clsndisj 22966 | 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 22967 | A subset whose closure has an empty interior also has an empty interior. (Contributed by NM, 4-Oct-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ ((intβπ½)β((clsβπ½)βπ)) = β ) β ((intβπ½)βπ) = β ) | ||
Theorem | ntreq0 22968* | Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (((intβπ½)βπ) = β β βπ₯ β π½ (π₯ β π β π₯ = β ))) | ||
Theorem | cldmre 22969 | The closed sets of a topology comprise a Moore system on the points of the topology. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ π = βͺ π½ β β’ (π½ β Top β (Clsdβπ½) β (Mooreβπ)) | ||
Theorem | mrccls 22970 | Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΉ = (mrClsβ(Clsdβπ½)) β β’ (π½ β Top β (clsβπ½) = πΉ) | ||
Theorem | cls0 22971 | The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.) |
β’ (π½ β Top β ((clsβπ½)ββ ) = β ) | ||
Theorem | ntr0 22972 | The interior of the empty set. (Contributed by NM, 2-Oct-2007.) |
β’ (π½ β Top β ((intβπ½)ββ ) = β ) | ||
Theorem | isopn3i 22973 | An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ ((π½ β Top β§ π β π½) β ((intβπ½)βπ) = π) | ||
Theorem | elcls3 22974* | Membership in a closure in terms of the members of a basis. Theorem 6.5(b) of [Munkres] p. 95. (Contributed by NM, 26-Feb-2007.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ (π β π½ = (topGenβπ΅)) & β’ (π β π = βͺ π½) & β’ (π β π΅ β TopBases) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β ((clsβπ½)βπ) β βπ₯ β π΅ (π β π₯ β (π₯ β© π) β β ))) | ||
Theorem | opncldf1 22975* | A bijection useful for converting statements about open sets to statements about closed sets and vice versa. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
β’ π = βͺ π½ & β’ πΉ = (π’ β π½ β¦ (π β π’)) β β’ (π½ β Top β (πΉ:π½β1-1-ontoβ(Clsdβπ½) β§ β‘πΉ = (π₯ β (Clsdβπ½) β¦ (π β π₯)))) | ||
Theorem | opncldf2 22976* | The values of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
β’ π = βͺ π½ & β’ πΉ = (π’ β π½ β¦ (π β π’)) β β’ ((π½ β Top β§ π΄ β π½) β (πΉβπ΄) = (π β π΄)) | ||
Theorem | opncldf3 22977* | The values of the converse/inverse of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
β’ π = βͺ π½ & β’ πΉ = (π’ β π½ β¦ (π β π’)) β β’ (π΅ β (Clsdβπ½) β (β‘πΉβπ΅) = (π β π΅)) | ||
Theorem | isclo 22978* | A set π΄ is clopen iff for every point π₯ in the space there is a neighborhood π¦ such that all the points in π¦ are in π΄ iff π₯ is. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β (π½ β© (Clsdβπ½)) β βπ₯ β π βπ¦ β π½ (π₯ β π¦ β§ βπ§ β π¦ (π₯ β π΄ β π§ β π΄)))) | ||
Theorem | isclo2 22979* | A set π΄ is clopen iff for every point π₯ in the space there is a neighborhood π¦ of π₯ which is either disjoint from π΄ or contained in π΄. (Contributed by Mario Carneiro, 7-Jul-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β (π½ β© (Clsdβπ½)) β βπ₯ β π βπ¦ β π½ (π₯ β π¦ β§ βπ§ β π¦ (π§ β π΄ β π¦ β π΄)))) | ||
Theorem | discld 22980 | The open sets of a discrete topology are closed and its closed sets are open. (Contributed by FL, 7-Jun-2007.) (Revised by Mario Carneiro, 7-Apr-2015.) |
β’ (π΄ β π β (Clsdβπ« π΄) = π« π΄) | ||
Theorem | sn0cld 22981 | The closed sets of the topology {β }. (Contributed by FL, 5-Jan-2009.) |
β’ (Clsdβ{β }) = {β } | ||
Theorem | indiscld 22982 | The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.) |
β’ (Clsdβ{β , π΄}) = {β , π΄} | ||
Theorem | mretopd 22983* | A Moore collection which is closed under finite unions called topological; such a collection is the closed sets of a canonically associated topology. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π β π β (Mooreβπ΅)) & β’ (π β β β π) & β’ ((π β§ π₯ β π β§ π¦ β π) β (π₯ βͺ π¦) β π) & β’ π½ = {π§ β π« π΅ β£ (π΅ β π§) β π} β β’ (π β (π½ β (TopOnβπ΅) β§ π = (Clsdβπ½))) | ||
Theorem | toponmre 22984 | The topologies over a given base set form a Moore collection: the intersection of any family of them is a topology, including the empty (relative) intersection which gives the discrete topology distop 22885. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
β’ (π΅ β π β (TopOnβπ΅) β (Mooreβπ« π΅)) | ||
Theorem | cldmreon 22985 | The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ (π½ β (TopOnβπ΅) β (Clsdβπ½) β (Mooreβπ΅)) | ||
Theorem | iscldtop 22986* | A family is the closed sets of a topology iff it is a Moore collection and closed under finite union. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (πΎ β (Clsd β (TopOnβπ΅)) β (πΎ β (Mooreβπ΅) β§ β β πΎ β§ βπ₯ β πΎ βπ¦ β πΎ (π₯ βͺ π¦) β πΎ)) | ||
Theorem | mreclatdemoBAD 22987 | The closed subspaces of a topology-bearing module form a complete lattice. Demonstration for mreclatBAD 18546. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7370 update): This proof uses the old df-clat 18482 and references the required instance of mreclatBAD 18546 as a hypothesis. When mreclatBAD 18546 is corrected to become mreclat, delete this theorem and uncomment the mreclatdemo below. |
β’ (((LSubSpβπ) β© (Clsdβ(TopOpenβπ))) β (Mooreββͺ (TopOpenβπ)) β (toIncβ((LSubSpβπ) β© (Clsdβ(TopOpenβπ)))) β CLat) β β’ (π β (TopSp β© LMod) β (toIncβ((LSubSpβπ) β© (Clsdβ(TopOpenβπ)))) β CLat) | ||
Syntax | cnei 22988 | Extend class notation with neighborhood relation for topologies. |
class nei | ||
Definition | df-nei 22989* | Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007.) |
β’ nei = (π β Top β¦ (π₯ β π« βͺ π β¦ {π¦ β π« βͺ π β£ βπ β π (π₯ β π β§ π β π¦)})) | ||
Theorem | neifval 22990* | Value of the neighborhood function on the subsets of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ (π½ β Top β (neiβπ½) = (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)})) | ||
Theorem | neif 22991 | The neighborhood function is a function from the set of the subsets of the base set of a topology. (Contributed by NM, 12-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ (π½ β Top β (neiβπ½) Fn π« π) | ||
Theorem | neiss2 22992 | A set with a neighborhood is a subset of the base set of a topology. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by NM, 12-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β π β π) | ||
Theorem | neival 22993* | Value of the set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((neiβπ½)βπ) = {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)}) | ||
Theorem | isnei 22994* | The predicate "the class π is a neighborhood of π". (Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)βπ) β (π β π β§ βπ β π½ (π β π β§ π β π)))) | ||
Theorem | neiint 22995 | An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((neiβπ½)βπ) β π β ((intβπ½)βπ))) | ||
Theorem | isneip 22996* | The predicate "the class π is a neighborhood of point π". (Contributed by NM, 26-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)β{π}) β (π β π β§ βπ β π½ (π β π β§ π β π)))) | ||
Theorem | neii1 22997 | A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β π β π) | ||
Theorem | neisspw 22998 | The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β Top β ((neiβπ½)βπ) β π« π) | ||
Theorem | neii2 22999* | Property of a neighborhood. (Contributed by NM, 12-Feb-2007.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β βπ β π½ (π β π β§ π β π)) | ||
Theorem | neiss 23000 | Any neighborhood of a set π is also a neighborhood of any subset π β π. Similar to Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 25-Sep-2006.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ) β§ π β π) β π β ((neiβπ½)βπ )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |