![]() |
Metamath
Proof Explorer Theorem List (p. 233 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnconst 23201 | A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π΅ β π β§ πΉ:πβΆ{π΅})) β πΉ β (π½ Cn πΎ)) | ||
Theorem | cnrest 23202 | 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 23203 | 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 23204 | 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 23205 | One direction of cnprest 23206 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 23206 | 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 23207 | 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 23208 | 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 23209 | 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 23210 | 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 23211 | 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 23212 | If πΉ converges, then πΉ is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β πΉ β (π βpm β)) | ||
Theorem | lmfss 23213 | 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 23214 | Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β π β π) | ||
Theorem | lmss 23215 | Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ πΎ = (π½ βΎt π) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β π½ β Top) & β’ (π β π β π) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ(βπ‘βπ½)π β πΉ(βπ‘βπΎ)π)) | ||
Theorem | sslm 23216 | 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 23217 | A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ βΎ (β€β₯βπ))(βπ‘βπ½)π)) | ||
Theorem | lmff 23218* | 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 23219* | 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 23220* | 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 23221 | 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 23222 | 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 23223 | Extend class notation with the class of all T0 spaces. |
class Kol2 | ||
Syntax | ct1 23224 | Extend class notation to include T1 spaces (also called FrΓ©chet spaces). |
class Fre | ||
Syntax | cha 23225 | Extend class notation with the class of all Hausdorff spaces. |
class Haus | ||
Syntax | creg 23226 | Extend class notation with the class of all regular topologies. |
class Reg | ||
Syntax | cnrm 23227 | Extend class notation with the class of all normal topologies. |
class Nrm | ||
Syntax | ccnrm 23228 | Extend class notation with the class of all completely normal topologies. |
class CNrm | ||
Syntax | cpnrm 23229 | Extend class notation with the class of all perfectly normal topologies. |
class PNrm | ||
Definition | df-t0 23230* | Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2696): 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 23264) 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 23231* | 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 23232* | 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 23233* | 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 23234* | 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 23235* | 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 23236* | 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 23237* | 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 23262. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ (π½ β Kol2 β (π½ β Top β§ βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | ist1 23238* | The predicate "is a T1 space". (Contributed by FL, 18-Jun-2007.) |
β’ π = βͺ π½ β β’ (π½ β Fre β (π½ β Top β§ βπ β π {π} β (Clsdβπ½))) | ||
Theorem | ishaus 23239* | The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007.) |
β’ π = βͺ π½ β β’ (π½ β Haus β (π½ β Top β§ βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β )))) | ||
Theorem | iscnrm 23240* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β CNrm β (π½ β Top β§ βπ₯ β π« π(π½ βΎt π₯) β Nrm)) | ||
Theorem | t0sep 23241* | Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ (π΄ β π β§ π΅ β π)) β (βπ₯ β π½ (π΄ β π₯ β π΅ β π₯) β π΄ = π΅)) | ||
Theorem | t0dist 23242* | Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅)) β βπ β π½ Β¬ (π΄ β π β π΅ β π)) | ||
Theorem | t1sncld 23243 | In a T1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π) β {π΄} β (Clsdβπ½)) | ||
Theorem | t1ficld 23244 | In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π β§ π΄ β Fin) β π΄ β (Clsdβπ½)) | ||
Theorem | hausnei 23245* | Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ (π β π β§ π β π β§ π β π)) β βπ β π½ βπ β π½ (π β π β§ π β π β§ (π β© π) = β )) | ||
Theorem | t0top 23246 | A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Kol2 β π½ β Top) | ||
Theorem | t1top 23247 | A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Top) | ||
Theorem | haustop 23248 | A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
β’ (π½ β Haus β π½ β Top) | ||
Theorem | isreg 23249* | 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 23250 | A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Reg β π½ β Top) | ||
Theorem | regsep 23251* | In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Reg β§ π β π½ β§ π΄ β π) β βπ₯ β π½ (π΄ β π₯ β§ ((clsβπ½)βπ₯) β π)) | ||
Theorem | isnrm 23252* | 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 23253 | A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Nrm β π½ β Top) | ||
Theorem | cnrmtop 23254 | A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Top) | ||
Theorem | iscnrm2 23255* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β CNrm β βπ₯ β π« π(π½ βΎt π₯) β Nrm)) | ||
Theorem | ispnrm 23256* | The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β (π½ β Nrm β§ (Clsdβπ½) β ran (π β (π½ βm β) β¦ β© ran π))) | ||
Theorem | pnrmnrm 23257 | A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Nrm) | ||
Theorem | pnrmtop 23258 | A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Top) | ||
Theorem | pnrmcld 23259* | 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 23260* | 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 23261* | The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | ist0-3 23262* | The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ ((π₯ β π β§ Β¬ π¦ β π) β¨ (Β¬ π₯ β π β§ π¦ β π))))) | ||
Theorem | cnt0 23263 | 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 23264* | 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 23265 | A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Kol2) | ||
Theorem | ist1-3 23266* | 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 23267 | 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 23268* | Express the predicate "π½ is a Hausdorff space." (Contributed by NM, 8-Mar-2007.) |
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β )))) | ||
Theorem | haust1 23269 | 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 23270* | 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 23271 | 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 23272* | 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 23273* | 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 23274* | In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ ((π½ β Nrm β§ (πΆ β (Clsdβπ½) β§ π· β (Clsdβπ½) β§ (πΆ β© π·) = β )) β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π· β π¦ β§ (π₯ β© π¦) = β )) | ||
Theorem | isnrm2 23275* | 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 23276* | 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 23277 | A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β Nrm) | ||
Theorem | cnrmnrm 23278 | A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Nrm) | ||
Theorem | restcnrm 23279 | A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β CNrm) | ||
Theorem | resthauslem 23280 | Lemma for resthaus 23285 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 23281 | 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 23282 | 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 23283 | A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Kol2 β§ π΄ β π) β (π½ βΎt π΄) β Kol2) | ||
Theorem | restt1 23284 | A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Fre β§ π΄ β π) β (π½ βΎt π΄) β Fre) | ||
Theorem | resthaus 23285 | 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 23286* | Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π β§ π΅ β π) β (βπ β π½ (π΄ β π β π΅ β π) β π΄ = π΅)) | ||
Theorem | t1sep 23287* | Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅)) β βπ β π½ (π΄ β π β§ Β¬ π΅ β π)) | ||
Theorem | sncld 23288 | 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 23289 | Lemma for sshaus 23292 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 23290 | A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Kol2) | ||
Theorem | sst1 23291 | A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Fre) | ||
Theorem | sshaus 23292 | A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Haus) | ||
Theorem | regsep2 23293* | 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βπ½) β§ π΄ β π β§ Β¬ π΄ β πΆ)) β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π΄ β π¦ β§ (π₯ β© π¦) = β )) | ||
Theorem | isreg2 23294* | A topological space is regular if any closed set is separated from any point not in it by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Reg β βπ β (Clsdβπ½)βπ₯ β π (Β¬ π₯ β π β βπ β π½ βπ β π½ (π β π β§ π₯ β π β§ (π β© π) = β )))) | ||
Theorem | dnsconst 23295 | If a continuous mapping to a T1 space is constant on a dense subset, it is constant on the entire space. Note that ((clsβπ½)βπ΄) = π means "π΄ is dense in π " and π΄ β (β‘πΉ β {π}) means "πΉ is constant on π΄ " (see funconstss 7058). (Contributed by NM, 15-Mar-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((πΎ β Fre β§ πΉ β (π½ Cn πΎ)) β§ (π β π β§ π΄ β (β‘πΉ β {π}) β§ ((clsβπ½)βπ΄) = π)) β πΉ:πβΆ{π}) | ||
Theorem | ordtt1 23296 | The order topology is T1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π β PosetRel β (ordTopβπ ) β Fre) | ||
Theorem | lmmo 23297 | A sequence in a Hausdorff space converges to at most one limit. Part of Lemma 1.4-2(a) of [Kreyszig] p. 26. (Contributed by NM, 31-Jan-2008.) (Proof shortened by Mario Carneiro, 1-May-2014.) |
β’ (π β π½ β Haus) & β’ (π β πΉ(βπ‘βπ½)π΄) & β’ (π β πΉ(βπ‘βπ½)π΅) β β’ (π β π΄ = π΅) | ||
Theorem | lmfun 23298 | The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013.) |
β’ (π½ β Haus β Fun (βπ‘βπ½)) | ||
Theorem | dishaus 23299 | A discrete topology is Hausdorff. Morris, Topology without tears, p.72, ex. 13. (Contributed by FL, 24-Jun-2007.) (Proof shortened by Mario Carneiro, 8-Apr-2015.) |
β’ (π΄ β π β π« π΄ β Haus) | ||
Theorem | ordthauslem 23300* | Lemma for ordthaus 23301. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ π = dom π β β’ ((π β TosetRel β§ π΄ β π β§ π΅ β π) β (π΄π π΅ β (π΄ β π΅ β βπ β (ordTopβπ )βπ β (ordTopβπ )(π΄ β π β§ π΅ β π β§ (π β© π) = β )))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |