![]() |
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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnss2 23001 | 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 23002 | 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 23003 | 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 23004* | 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 23005* | 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 23006* | Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (πΉ β (π½ Cn πΎ) β βπ β π βπ€ β ((neiβπΎ)β{(πΉβπ)})βπ£ β ((neiβπ½)β{π})(πΉ β π£) β π€)) | ||
Theorem | cnconst2 23007 | A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β (π Γ {π΅}) β (π½ Cn πΎ)) | ||
Theorem | cnconst 23008 | A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π΅ β π β§ πΉ:πβΆ{π΅})) β πΉ β (π½ Cn πΎ)) | ||
Theorem | cnrest 23009 | 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 23010 | 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 23011 | 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 23012 | One direction of cnprest 23013 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 23013 | 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 23014 | 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 23015 | 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 23016 | 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 23017 | 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 23018 | 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 23019 | If πΉ converges, then πΉ is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β πΉ β (π βpm β)) | ||
Theorem | lmfss 23020 | 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 23021 | Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β π β π) | ||
Theorem | lmss 23022 | Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ πΎ = (π½ βΎt π) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β π½ β Top) & β’ (π β π β π) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ(βπ‘βπ½)π β πΉ(βπ‘βπΎ)π)) | ||
Theorem | sslm 23023 | 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 23024 | A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ βΎ (β€β₯βπ))(βπ‘βπ½)π)) | ||
Theorem | lmff 23025* | 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 23026* | 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 23027* | 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 23028 | 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 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.) |
β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β πΊ β (π½ Cn πΎ)) β β’ (π β (πΊ β πΉ)(βπ‘βπΎ)(πΊβπ)) | ||
Syntax | ct0 23030 | Extend class notation with the class of all T0 spaces. |
class Kol2 | ||
Syntax | ct1 23031 | Extend class notation to include T1 spaces (also called FrΓ©chet spaces). |
class Fre | ||
Syntax | cha 23032 | Extend class notation with the class of all Hausdorff spaces. |
class Haus | ||
Syntax | creg 23033 | Extend class notation with the class of all regular topologies. |
class Reg | ||
Syntax | cnrm 23034 | Extend class notation with the class of all normal topologies. |
class Nrm | ||
Syntax | ccnrm 23035 | Extend class notation with the class of all completely normal topologies. |
class CNrm | ||
Syntax | cpnrm 23036 | Extend class notation with the class of all perfectly normal topologies. |
class PNrm | ||
Definition | df-t0 23037* | Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2701): 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 23071) 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 23038* | 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 23039* | 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 23040* | 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 23041* | 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 23042* | 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 23043* | 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 23044* | 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 23069. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ (π½ β Kol2 β (π½ β Top β§ βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | ist1 23045* | The predicate "is a T1 space". (Contributed by FL, 18-Jun-2007.) |
β’ π = βͺ π½ β β’ (π½ β Fre β (π½ β Top β§ βπ β π {π} β (Clsdβπ½))) | ||
Theorem | ishaus 23046* | The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007.) |
β’ π = βͺ π½ β β’ (π½ β Haus β (π½ β Top β§ βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β )))) | ||
Theorem | iscnrm 23047* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β CNrm β (π½ β Top β§ βπ₯ β π« π(π½ βΎt π₯) β Nrm)) | ||
Theorem | t0sep 23048* | Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ (π΄ β π β§ π΅ β π)) β (βπ₯ β π½ (π΄ β π₯ β π΅ β π₯) β π΄ = π΅)) | ||
Theorem | t0dist 23049* | Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅)) β βπ β π½ Β¬ (π΄ β π β π΅ β π)) | ||
Theorem | t1sncld 23050 | In a T1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π) β {π΄} β (Clsdβπ½)) | ||
Theorem | t1ficld 23051 | In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π β§ π΄ β Fin) β π΄ β (Clsdβπ½)) | ||
Theorem | hausnei 23052* | Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ (π β π β§ π β π β§ π β π)) β βπ β π½ βπ β π½ (π β π β§ π β π β§ (π β© π) = β )) | ||
Theorem | t0top 23053 | A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Kol2 β π½ β Top) | ||
Theorem | t1top 23054 | A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Top) | ||
Theorem | haustop 23055 | A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
β’ (π½ β Haus β π½ β Top) | ||
Theorem | isreg 23056* | 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 23057 | A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Reg β π½ β Top) | ||
Theorem | regsep 23058* | In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Reg β§ π β π½ β§ π΄ β π) β βπ₯ β π½ (π΄ β π₯ β§ ((clsβπ½)βπ₯) β π)) | ||
Theorem | isnrm 23059* | 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 23060 | A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Nrm β π½ β Top) | ||
Theorem | cnrmtop 23061 | A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Top) | ||
Theorem | iscnrm2 23062* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β CNrm β βπ₯ β π« π(π½ βΎt π₯) β Nrm)) | ||
Theorem | ispnrm 23063* | The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β (π½ β Nrm β§ (Clsdβπ½) β ran (π β (π½ βm β) β¦ β© ran π))) | ||
Theorem | pnrmnrm 23064 | A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Nrm) | ||
Theorem | pnrmtop 23065 | A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Top) | ||
Theorem | pnrmcld 23066* | 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 23067* | 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 23068* | The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | ist0-3 23069* | The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ ((π₯ β π β§ Β¬ π¦ β π) β¨ (Β¬ π₯ β π β§ π¦ β π))))) | ||
Theorem | cnt0 23070 | 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 23071* | 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 23072 | A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Kol2) | ||
Theorem | ist1-3 23073* | 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 23074 | 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 23075* | Express the predicate "π½ is a Hausdorff space." (Contributed by NM, 8-Mar-2007.) |
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β )))) | ||
Theorem | haust1 23076 | 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 23077* | 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 23078 | 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 23079* | 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 23080* | 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 23081* | In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ ((π½ β Nrm β§ (πΆ β (Clsdβπ½) β§ π· β (Clsdβπ½) β§ (πΆ β© π·) = β )) β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π· β π¦ β§ (π₯ β© π¦) = β )) | ||
Theorem | isnrm2 23082* | 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 23083* | 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 23084 | A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β Nrm) | ||
Theorem | cnrmnrm 23085 | A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Nrm) | ||
Theorem | restcnrm 23086 | A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β CNrm) | ||
Theorem | resthauslem 23087 | Lemma for resthaus 23092 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 23088 | 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 23089 | 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 23090 | A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Kol2 β§ π΄ β π) β (π½ βΎt π΄) β Kol2) | ||
Theorem | restt1 23091 | A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Fre β§ π΄ β π) β (π½ βΎt π΄) β Fre) | ||
Theorem | resthaus 23092 | 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 23093* | Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π β§ π΅ β π) β (βπ β π½ (π΄ β π β π΅ β π) β π΄ = π΅)) | ||
Theorem | t1sep 23094* | Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅)) β βπ β π½ (π΄ β π β§ Β¬ π΅ β π)) | ||
Theorem | sncld 23095 | 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 23096 | Lemma for sshaus 23099 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 23097 | A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Kol2) | ||
Theorem | sst1 23098 | A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Fre) | ||
Theorem | sshaus 23099 | A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Haus) | ||
Theorem | regsep2 23100* | In a regular space, a closed set is separated by open sets from a point not in it. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Reg β§ (πΆ β (Clsdβπ½) β§ π΄ β π β§ Β¬ π΄ β πΆ)) β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π΄ β π¦ β§ (π₯ β© π¦) = β )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |