![]() |
Metamath
Proof Explorer Theorem List (p. 231 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnss1 23001 | If the topology πΎ is finer than π½, then there are more continuous functions from πΎ than from π½. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΎ β (TopOnβπ) β§ π½ β πΎ) β (π½ Cn πΏ) β (πΎ Cn πΏ)) | ||
Theorem | cnss2 23002 | If the topology πΎ is finer than π½, then there are fewer continuous functions into πΎ than into π½ from some other space. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ πΎ β β’ ((πΏ β (TopOnβπ) β§ πΏ β πΎ) β (π½ Cn πΎ) β (π½ Cn πΏ)) | ||
Theorem | cncnpi 23003 | A continuous function is continuous at all points. One direction of Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β πΉ β ((π½ CnP πΎ)βπ΄)) | ||
Theorem | cnsscnp 23004 | The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ β β’ (π β π β (π½ Cn πΎ) β ((π½ CnP πΎ)βπ)) | ||
Theorem | cncnp 23005* | A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)))) | ||
Theorem | cncnp2 23006* | A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (π β β β (πΉ β (π½ Cn πΎ) β βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯))) | ||
Theorem | cnnei 23007* | Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (πΉ β (π½ Cn πΎ) β βπ β π βπ€ β ((neiβπΎ)β{(πΉβπ)})βπ£ β ((neiβπ½)β{π})(πΉ β π£) β π€)) | ||
Theorem | cnconst2 23008 | A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β (π Γ {π΅}) β (π½ Cn πΎ)) | ||
Theorem | cnconst 23009 | A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π΅ β π β§ πΉ:πβΆ{π΅})) β πΉ β (π½ Cn πΎ)) | ||
Theorem | cnrest 23010 | Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ)) | ||
Theorem | cnrest2 23011 | Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ ((πΎ β (TopOnβπ) β§ ran πΉ β π΅ β§ π΅ β π) β (πΉ β (π½ Cn πΎ) β πΉ β (π½ Cn (πΎ βΎt π΅)))) | ||
Theorem | cnrest2r 23012 | Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.) |
β’ (πΎ β Top β (π½ Cn (πΎ βΎt π΅)) β (π½ Cn πΎ)) | ||
Theorem | cnpresti 23013 | One direction of cnprest 23014 under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 1-May-2015.) |
β’ π = βͺ π½ β β’ ((π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ)) β (πΉ βΎ π΄) β (((π½ βΎt π΄) CnP πΎ)βπ)) | ||
Theorem | cnprest 23014 | Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((π½ β Top β§ π΄ β π) β§ (π β ((intβπ½)βπ΄) β§ πΉ:πβΆπ)) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ βΎ π΄) β (((π½ βΎt π΄) CnP πΎ)βπ))) | ||
Theorem | cnprest2 23015 | Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β (πΉ β ((π½ CnP πΎ)βπ) β πΉ β ((π½ CnP (πΎ βΎt π΅))βπ))) | ||
Theorem | cndis 23016 | Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ ((π΄ β π β§ π½ β (TopOnβπ)) β (π« π΄ Cn π½) = (π βm π΄)) | ||
Theorem | cnindis 23017 | Every function is continuous when the codomain is indiscrete (trivial). (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ Cn {β , π΄}) = (π΄ βm π)) | ||
Theorem | cnpdis 23018 | If π΄ is an isolated point in π (or equivalently, the singleton {π΄} is open in π), then every function is continuous at π΄. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ {π΄} β π½) β ((π½ CnP πΎ)βπ΄) = (π βm π)) | ||
Theorem | paste 23019 | Pasting lemma. If π΄ and π΅ are closed sets in π with π΄ βͺ π΅ = π, then any function whose restrictions to π΄ and π΅ are continuous is continuous on all of π. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ & β’ (π β π΄ β (Clsdβπ½)) & β’ (π β π΅ β (Clsdβπ½)) & β’ (π β (π΄ βͺ π΅) = π) & β’ (π β πΉ:πβΆπ) & β’ (π β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ)) & β’ (π β (πΉ βΎ π΅) β ((π½ βΎt π΅) Cn πΎ)) β β’ (π β πΉ β (π½ Cn πΎ)) | ||
Theorem | lmfpm 23020 | If πΉ converges, then πΉ is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β πΉ β (π βpm β)) | ||
Theorem | lmfss 23021 | Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition). (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β πΉ β (β Γ π)) | ||
Theorem | lmcl 23022 | Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β π β π) | ||
Theorem | lmss 23023 | Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ πΎ = (π½ βΎt π) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β π½ β Top) & β’ (π β π β π) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ(βπ‘βπ½)π β πΉ(βπ‘βπΎ)π)) | ||
Theorem | sslm 23024 | A finer topology has fewer convergent sequences (but the sequences that do converge, converge to the same value). (Contributed by Mario Carneiro, 15-Sep-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β (βπ‘βπΎ) β (βπ‘βπ½)) | ||
Theorem | lmres 23025 | A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ βΎ (β€β₯βπ))(βπ‘βπ½)π)) | ||
Theorem | lmff 23026* | If πΉ converges, there is some upper integer set on which πΉ is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β β€) & β’ (π β πΉ β dom (βπ‘βπ½)) β β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ) | ||
Theorem | lmcls 23027* | Any convergent sequence of points in a subset of a topological space converges to a point in the closure of the subset. (Contributed by Mario Carneiro, 30-Dec-2013.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β β€) & β’ (π β πΉ(βπ‘βπ½)π) & β’ ((π β§ π β π) β (πΉβπ) β π) & β’ (π β π β π) β β’ (π β π β ((clsβπ½)βπ)) | ||
Theorem | lmcld 23028* | Any convergent sequence of points in a closed subset of a topological space converges to a point in the set. (Contributed by Mario Carneiro, 30-Dec-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β β€) & β’ (π β πΉ(βπ‘βπ½)π) & β’ ((π β§ π β π) β (πΉβπ) β π) & β’ (π β π β (Clsdβπ½)) β β’ (π β π β π) | ||
Theorem | lmcnp 23029 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) |
β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β πΊ β ((π½ CnP πΎ)βπ)) β β’ (π β (πΊ β πΉ)(βπ‘βπΎ)(πΊβπ)) | ||
Theorem | lmcn 23030 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) |
β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β πΊ β (π½ Cn πΎ)) β β’ (π β (πΊ β πΉ)(βπ‘βπΎ)(πΊβπ)) | ||
Syntax | ct0 23031 | Extend class notation with the class of all T0 spaces. |
class Kol2 | ||
Syntax | ct1 23032 | Extend class notation to include T1 spaces (also called FrΓ©chet spaces). |
class Fre | ||
Syntax | cha 23033 | Extend class notation with the class of all Hausdorff spaces. |
class Haus | ||
Syntax | creg 23034 | Extend class notation with the class of all regular topologies. |
class Reg | ||
Syntax | cnrm 23035 | Extend class notation with the class of all normal topologies. |
class Nrm | ||
Syntax | ccnrm 23036 | Extend class notation with the class of all completely normal topologies. |
class CNrm | ||
Syntax | cpnrm 23037 | Extend class notation with the class of all perfectly normal topologies. |
class PNrm | ||
Definition | df-t0 23038* | Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2702): any two points which are members of the same open sets are equal, or in contraposition, for any two distinct points there is an open set which contains one point but not the other. This differs from T1 spaces (see ist1-2 23072) in that in a T1 space you can choose which point will be in the open set and which outside; in a T0 space you only know that one of the two points is in the set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ Kol2 = {π β Top β£ βπ₯ β βͺ πβπ¦ β βͺ π(βπ β π (π₯ β π β π¦ β π) β π₯ = π¦)} | ||
Definition | df-t1 23039* | The class of all T1 spaces, also called FrΓ©chet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007.) |
β’ Fre = {π₯ β Top β£ βπ β βͺ π₯{π} β (Clsdβπ₯)} | ||
Definition | df-haus 23040* | Define the class of all Hausdorff (or T2) spaces. A Hausdorff space is a topology in which distinct points have disjoint open neighborhoods. Definition of Hausdorff space in [Munkres] p. 98. (Contributed by NM, 8-Mar-2007.) |
β’ Haus = {π β Top β£ βπ₯ β βͺ πβπ¦ β βͺ π(π₯ β π¦ β βπ β π βπ β π (π₯ β π β§ π¦ β π β§ (π β© π) = β ))} | ||
Definition | df-reg 23041* | Define regular spaces. A space is regular if a point and a closed set can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ Reg = {π β Top β£ βπ₯ β π βπ¦ β π₯ βπ§ β π (π¦ β π§ β§ ((clsβπ)βπ§) β π₯)} | ||
Definition | df-nrm 23042* | Define normal spaces. A space is normal if disjoint closed sets can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ Nrm = {π β Top β£ βπ₯ β π βπ¦ β ((Clsdβπ) β© π« π₯)βπ§ β π (π¦ β π§ β§ ((clsβπ)βπ§) β π₯)} | ||
Definition | df-cnrm 23043* | Define completely normal spaces. A space is completely normal if all its subspaces are normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ CNrm = {π β Top β£ βπ₯ β π« βͺ π(π βΎt π₯) β Nrm} | ||
Definition | df-pnrm 23044* | Define perfectly normal spaces. A space is perfectly normal if it is normal and every closed set is a Gδ set, meaning that it is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ PNrm = {π β Nrm β£ (Clsdβπ) β ran (π β (π βm β) β¦ β© ran π)} | ||
Theorem | ist0 23045* | The predicate "is a T0 space". Every pair of distinct points is topologically distinguishable. For the way this definition is usually encountered, see ist0-3 23070. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ (π½ β Kol2 β (π½ β Top β§ βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | ist1 23046* | The predicate "is a T1 space". (Contributed by FL, 18-Jun-2007.) |
β’ π = βͺ π½ β β’ (π½ β Fre β (π½ β Top β§ βπ β π {π} β (Clsdβπ½))) | ||
Theorem | ishaus 23047* | The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007.) |
β’ π = βͺ π½ β β’ (π½ β Haus β (π½ β Top β§ βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β )))) | ||
Theorem | iscnrm 23048* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β CNrm β (π½ β Top β§ βπ₯ β π« π(π½ βΎt π₯) β Nrm)) | ||
Theorem | t0sep 23049* | Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ (π΄ β π β§ π΅ β π)) β (βπ₯ β π½ (π΄ β π₯ β π΅ β π₯) β π΄ = π΅)) | ||
Theorem | t0dist 23050* | Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅)) β βπ β π½ Β¬ (π΄ β π β π΅ β π)) | ||
Theorem | t1sncld 23051 | In a T1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π) β {π΄} β (Clsdβπ½)) | ||
Theorem | t1ficld 23052 | In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π β§ π΄ β Fin) β π΄ β (Clsdβπ½)) | ||
Theorem | hausnei 23053* | Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ (π β π β§ π β π β§ π β π)) β βπ β π½ βπ β π½ (π β π β§ π β π β§ (π β© π) = β )) | ||
Theorem | t0top 23054 | A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Kol2 β π½ β Top) | ||
Theorem | t1top 23055 | A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Top) | ||
Theorem | haustop 23056 | A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
β’ (π½ β Haus β π½ β Top) | ||
Theorem | isreg 23057* | The predicate "is a regular space". In a regular space, any open neighborhood has a closed subneighborhood. Note that some authors require the space to be Hausdorff (which would make it the same as T3), but we reserve the phrase "regular Hausdorff" for that as many topologists do. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β Reg β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ§ β π½ (π¦ β π§ β§ ((clsβπ½)βπ§) β π₯))) | ||
Theorem | regtop 23058 | A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Reg β π½ β Top) | ||
Theorem | regsep 23059* | In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Reg β§ π β π½ β§ π΄ β π) β βπ₯ β π½ (π΄ β π₯ β§ ((clsβπ½)βπ₯) β π)) | ||
Theorem | isnrm 23060* | The predicate "is a normal space." Much like the case for regular spaces, normal does not imply Hausdorff or even regular. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β Nrm β (π½ β Top β§ βπ₯ β π½ βπ¦ β ((Clsdβπ½) β© π« π₯)βπ§ β π½ (π¦ β π§ β§ ((clsβπ½)βπ§) β π₯))) | ||
Theorem | nrmtop 23061 | A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Nrm β π½ β Top) | ||
Theorem | cnrmtop 23062 | A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Top) | ||
Theorem | iscnrm2 23063* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β CNrm β βπ₯ β π« π(π½ βΎt π₯) β Nrm)) | ||
Theorem | ispnrm 23064* | The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β (π½ β Nrm β§ (Clsdβπ½) β ran (π β (π½ βm β) β¦ β© ran π))) | ||
Theorem | pnrmnrm 23065 | A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Nrm) | ||
Theorem | pnrmtop 23066 | A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Top) | ||
Theorem | pnrmcld 23067* | A closed set in a perfectly normal space is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β PNrm β§ π΄ β (Clsdβπ½)) β βπ β (π½ βm β)π΄ = β© ran π) | ||
Theorem | pnrmopn 23068* | An open set in a perfectly normal space is a countable union of closed sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β PNrm β§ π΄ β π½) β βπ β ((Clsdβπ½) βm β)π΄ = βͺ ran π) | ||
Theorem | ist0-2 23069* | The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | ist0-3 23070* | The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ ((π₯ β π β§ Β¬ π¦ β π) β¨ (Β¬ π₯ β π β§ π¦ β π))))) | ||
Theorem | cnt0 23071 | The preimage of a T0 topology under an injective map is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((πΎ β Kol2 β§ πΉ:πβ1-1βπ β§ πΉ β (π½ Cn πΎ)) β π½ β Kol2) | ||
Theorem | ist1-2 23072* | An alternate characterization of T1 spaces. (Contributed by Jeff Hankins, 31-Jan-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Fre β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | t1t0 23073 | A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Kol2) | ||
Theorem | ist1-3 23074* | A space is T1 iff every point is the only point in the intersection of all open sets containing that point. (Contributed by Jeff Hankins, 31-Jan-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Fre β βπ₯ β π β© {π β π½ β£ π₯ β π} = {π₯})) | ||
Theorem | cnt1 23075 | The preimage of a T1 topology under an injective map is T1. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((πΎ β Fre β§ πΉ:πβ1-1βπ β§ πΉ β (π½ Cn πΎ)) β π½ β Fre) | ||
Theorem | ishaus2 23076* | Express the predicate "π½ is a Hausdorff space." (Contributed by NM, 8-Mar-2007.) |
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β )))) | ||
Theorem | haust1 23077 | A Hausdorff space is a T1 space. (Contributed by FL, 11-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β Haus β π½ β Fre) | ||
Theorem | hausnei2 23078* | The Hausdorff condition still holds if one considers general neighborhoods instead of open sets. (Contributed by Jeff Hankins, 5-Sep-2009.) |
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β ))) | ||
Theorem | cnhaus 23079 | The preimage of a Hausdorff topology under an injective map is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((πΎ β Haus β§ πΉ:πβ1-1βπ β§ πΉ β (π½ Cn πΎ)) β π½ β Haus) | ||
Theorem | nrmsep3 23080* | In a normal space, given a closed set π΅ inside an open set π΄, there is an open set π₯ such that π΅ β π₯ β cls(π₯) β π΄. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((π½ β Nrm β§ (π΄ β π½ β§ π΅ β (Clsdβπ½) β§ π΅ β π΄)) β βπ₯ β π½ (π΅ β π₯ β§ ((clsβπ½)βπ₯) β π΄)) | ||
Theorem | nrmsep2 23081* | In a normal space, any two disjoint closed sets have the property that each one is a subset of an open set whose closure is disjoint from the other. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 24-Aug-2015.) |
β’ ((π½ β Nrm β§ (πΆ β (Clsdβπ½) β§ π· β (Clsdβπ½) β§ (πΆ β© π·) = β )) β βπ₯ β π½ (πΆ β π₯ β§ (((clsβπ½)βπ₯) β© π·) = β )) | ||
Theorem | nrmsep 23082* | In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ ((π½ β Nrm β§ (πΆ β (Clsdβπ½) β§ π· β (Clsdβπ½) β§ (πΆ β© π·) = β )) β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π· β π¦ β§ (π₯ β© π¦) = β )) | ||
Theorem | isnrm2 23083* | An alternate characterization of normality. This is the important property in the proof of Urysohn's lemma. (Contributed by Jeff Hankins, 1-Feb-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β Nrm β (π½ β Top β§ βπ β (Clsdβπ½)βπ β (Clsdβπ½)((π β© π) = β β βπ β π½ (π β π β§ (((clsβπ½)βπ) β© π) = β )))) | ||
Theorem | isnrm3 23084* | A topological space is normal iff any two disjoint closed sets are separated by open sets. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β Nrm β (π½ β Top β§ βπ β (Clsdβπ½)βπ β (Clsdβπ½)((π β© π) = β β βπ₯ β π½ βπ¦ β π½ (π β π₯ β§ π β π¦ β§ (π₯ β© π¦) = β )))) | ||
Theorem | cnrmi 23085 | A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β Nrm) | ||
Theorem | cnrmnrm 23086 | A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Nrm) | ||
Theorem | restcnrm 23087 | A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β CNrm) | ||
Theorem | resthauslem 23088 | Lemma for resthaus 23093 and similar theorems. If the topological property π΄ is preserved under injective preimages, then property π΄ passes to subspaces. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β π΄ β π½ β Top) & β’ ((π½ β π΄ β§ ( I βΎ (π β© βͺ π½)):(π β© βͺ π½)β1-1β(π β© βͺ π½) β§ ( I βΎ (π β© βͺ π½)) β ((π½ βΎt π) Cn π½)) β (π½ βΎt π) β π΄) β β’ ((π½ β π΄ β§ π β π) β (π½ βΎt π) β π΄) | ||
Theorem | lpcls 23089 | The limit points of the closure of a subset are the same as the limit points of the set in a T1 space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π β π) β ((limPtβπ½)β((clsβπ½)βπ)) = ((limPtβπ½)βπ)) | ||
Theorem | perfcls 23090 | A subset of a perfect space is perfect iff its closure is perfect (and the closure is an actual perfect set, since it is both closed and perfect in the subspace topology). (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π β π) β ((π½ βΎt π) β Perf β (π½ βΎt ((clsβπ½)βπ)) β Perf)) | ||
Theorem | restt0 23091 | A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Kol2 β§ π΄ β π) β (π½ βΎt π΄) β Kol2) | ||
Theorem | restt1 23092 | A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Fre β§ π΄ β π) β (π½ βΎt π΄) β Fre) | ||
Theorem | resthaus 23093 | A subspace of a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Haus β§ π΄ β π) β (π½ βΎt π΄) β Haus) | ||
Theorem | t1sep2 23094* | Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π β§ π΅ β π) β (βπ β π½ (π΄ β π β π΅ β π) β π΄ = π΅)) | ||
Theorem | t1sep 23095* | Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅)) β βπ β π½ (π΄ β π β§ Β¬ π΅ β π)) | ||
Theorem | sncld 23096 | A singleton is closed in a Hausdorff space. (Contributed by NM, 5-Mar-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ π β π) β {π} β (Clsdβπ½)) | ||
Theorem | sshauslem 23097 | Lemma for sshaus 23100 and similar theorems. If the topological property π΄ is preserved under injective preimages, then a topology finer than one with property π΄ also has property π΄. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ & β’ (π½ β π΄ β π½ β Top) & β’ ((π½ β π΄ β§ ( I βΎ π):πβ1-1βπ β§ ( I βΎ π) β (πΎ Cn π½)) β πΎ β π΄) β β’ ((π½ β π΄ β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β π΄) | ||
Theorem | sst0 23098 | A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Kol2) | ||
Theorem | sst1 23099 | A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Fre) | ||
Theorem | sshaus 23100 | A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Haus) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |