![]() |
Metamath
Proof Explorer Theorem List (p. 235 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 | cnmpt1res 23401* | The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.) |
β’ πΎ = (π½ βΎt π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΏ)) β β’ (π β (π₯ β π β¦ π΄) β (πΎ Cn πΏ)) | ||
Theorem | cnmpt2res 23402* | The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.) |
β’ πΎ = (π½ βΎt π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π βΎt π) & β’ (π β π β (TopOnβπ)) & β’ (π β π β π) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt π) Cn πΏ)) β β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΎ Γt π) Cn πΏ)) | ||
Theorem | cnmptcom 23403* | The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) β β’ (π β (π¦ β π, π₯ β π β¦ π΄) β ((πΎ Γt π½) Cn πΏ)) | ||
Theorem | cnmptkc 23404* | The curried first projection function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) β β’ (π β (π₯ β π β¦ (π¦ β π β¦ π₯)) β (π½ Cn (π½ βko πΎ))) | ||
Theorem | cnmptkp 23405* | The evaluation of the inner function in a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) & β’ (π β π΅ β π) & β’ (π¦ = π΅ β π΄ = πΆ) β β’ (π β (π₯ β π β¦ πΆ) β (π½ Cn πΏ)) | ||
Theorem | cnmptk1 23406* | The composition of a curried function with a one-arg function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) & β’ (π β (π§ β π β¦ π΅) β (πΏ Cn π)) & β’ (π§ = π΄ β π΅ = πΆ) β β’ (π β (π₯ β π β¦ (π¦ β π β¦ πΆ)) β (π½ Cn (π βko πΎ))) | ||
Theorem | cnmpt1k 23407* | The composition of a one-arg function with a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΏ)) & β’ (π β (π¦ β π β¦ (π§ β π β¦ π΅)) β (πΎ Cn (π βko πΏ))) & β’ (π§ = π΄ β π΅ = πΆ) β β’ (π β (π¦ β π β¦ (π₯ β π β¦ πΆ)) β (πΎ Cn (π βko π½))) | ||
Theorem | cnmptkk 23408* | The composition of two curried functions is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ (π β πΏ β π-Locally Comp) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) & β’ (π β (π₯ β π β¦ (π§ β π β¦ π΅)) β (π½ Cn (π βko πΏ))) & β’ (π§ = π΄ β π΅ = πΆ) β β’ (π β (π₯ β π β¦ (π¦ β π β¦ πΆ)) β (π½ Cn (π βko πΎ))) | ||
Theorem | xkofvcn 23409* | Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn 23381.) (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π & β’ πΉ = (π β (π Cn π), π₯ β π β¦ (πβπ₯)) β β’ ((π β π-Locally Comp β§ π β Top) β πΉ β (((π βko π ) Γt π ) Cn π)) | ||
Theorem | cnmptk1p 23410* | The evaluation of a curried function by a one-arg function is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β πΎ β π-Locally Comp) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) & β’ (π β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) & β’ (π¦ = π΅ β π΄ = πΆ) β β’ (π β (π₯ β π β¦ πΆ) β (π½ Cn πΏ)) | ||
Theorem | cnmptk2 23411* | The uncurrying of a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β πΎ β π-Locally Comp) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) β β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) | ||
Theorem | xkoinjcn 23412* | Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ πΉ = (π₯ β π β¦ (π¦ β π β¦ β¨π¦, π₯β©)) β β’ ((π β (TopOnβπ) β§ π β (TopOnβπ)) β πΉ β (π Cn ((π Γt π ) βko π))) | ||
Theorem | cnmpt2k 23413* | The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) β β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) | ||
Theorem | txconn 23414 | The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.) |
β’ ((π β Conn β§ π β Conn) β (π Γt π) β Conn) | ||
Theorem | imasnopn 23415 | If a relation graph is open, then an image set of a singleton is also open. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ πΎ β Top) β§ (π β (π½ Γt πΎ) β§ π΄ β π)) β (π β {π΄}) β πΎ) | ||
Theorem | imasncld 23416 | If a relation graph is closed, then an image set of a singleton is also closed. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ πΎ β Top) β§ (π β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π β {π΄}) β (ClsdβπΎ)) | ||
Theorem | imasncls 23417 | If a relation graph is closed, then an image set of a singleton is also closed. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (π β (π Γ π) β§ π΄ β π)) β ((clsβπΎ)β(π β {π΄})) β (((clsβ(π½ Γt πΎ))βπ ) β {π΄})) | ||
Syntax | ckq 23418 | Extend class notation with the Kolmogorov quotient function. |
class KQ | ||
Definition | df-kq 23419* | Define the Kolmogorov quotient. This is a function on topologies which maps a topology to its quotient under the topological distinguishability map, which takes a point to the set of open sets that contain it. Two points are mapped to the same image under this function iff they are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ KQ = (π β Top β¦ (π qTop (π₯ β βͺ π β¦ {π¦ β π β£ π₯ β π¦}))) | ||
Theorem | qtopval 23420* | Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ β π) β (π½ qTop πΉ) = {π β π« (πΉ β π) β£ ((β‘πΉ β π ) β© π) β π½}) | ||
Theorem | qtopval2 23421* | Value of the quotient topology function when πΉ is a function on the base set. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ:πβontoβπ β§ π β π) β (π½ qTop πΉ) = {π β π« π β£ (β‘πΉ β π ) β π½}) | ||
Theorem | elqtop 23422 | Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ:πβontoβπ β§ π β π) β (π΄ β (π½ qTop πΉ) β (π΄ β π β§ (β‘πΉ β π΄) β π½))) | ||
Theorem | qtopres 23423 | The quotient topology is unaffected by restriction to the base set. This property makes it slightly more convenient to use, since we don't have to require that πΉ be a function with domain π. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ (πΉ β π β (π½ qTop πΉ) = (π½ qTop (πΉ βΎ π))) | ||
Theorem | qtoptop2 23424 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π½ qTop πΉ) β Top) | ||
Theorem | qtoptop 23425 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΉ Fn π) β (π½ qTop πΉ) β Top) | ||
Theorem | elqtop2 23426 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ:πβontoβπ) β (π΄ β (π½ qTop πΉ) β (π΄ β π β§ (β‘πΉ β π΄) β π½))) | ||
Theorem | qtopuni 23427 | The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΉ:πβontoβπ) β π = βͺ (π½ qTop πΉ)) | ||
Theorem | elqtop3 23428 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π΄ β (π½ qTop πΉ) β (π΄ β π β§ (β‘πΉ β π΄) β π½))) | ||
Theorem | qtoptopon 23429 | The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π½ qTop πΉ) β (TopOnβπ)) | ||
Theorem | qtopid 23430 | A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ Fn π) β πΉ β (π½ Cn (π½ qTop πΉ))) | ||
Theorem | idqtop 23431 | The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ qTop ( I βΎ π)) = π½) | ||
Theorem | qtopcmplem 23432 | Lemma for qtopcmp 23433 and qtopconn 23434. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ & β’ (π½ β π΄ β π½ β Top) & β’ ((π½ β π΄ β§ πΉ:πβontoββͺ (π½ qTop πΉ) β§ πΉ β (π½ Cn (π½ qTop πΉ))) β (π½ qTop πΉ) β π΄) β β’ ((π½ β π΄ β§ πΉ Fn π) β (π½ qTop πΉ) β π΄) | ||
Theorem | qtopcmp 23433 | A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ πΉ Fn π) β (π½ qTop πΉ) β Comp) | ||
Theorem | qtopconn 23434 | A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Conn β§ πΉ Fn π) β (π½ qTop πΉ) β Conn) | ||
Theorem | qtopkgen 23435 | A quotient of a compactly generated space is compactly generated. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ β β’ ((π½ β ran πGen β§ πΉ Fn π) β (π½ qTop πΉ) β ran πGen) | ||
Theorem | basqtop 23436 | An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β TopBases β§ πΉ:πβ1-1-ontoβπ) β (π½ qTop πΉ) β TopBases) | ||
Theorem | tgqtop 23437 | An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β TopBases β§ πΉ:πβ1-1-ontoβπ) β ((topGenβπ½) qTop πΉ) = (topGenβ(π½ qTop πΉ))) | ||
Theorem | qtopcld 23438 | The property of being a closed set in the quotient topology. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π΄ β (Clsdβ(π½ qTop πΉ)) β (π΄ β π β§ (β‘πΉ β π΄) β (Clsdβπ½)))) | ||
Theorem | qtopcn 23439 | Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β (πΊ β ((π½ qTop πΉ) Cn πΎ) β (πΊ β πΉ) β (π½ Cn πΎ))) | ||
Theorem | qtopss 23440 | A surjective continuous function from π½ to πΎ induces a topology π½ qTop πΉ on the base set of πΎ. This topology is in general finer than πΎ. Together with qtopid 23430, this implies that π½ qTop πΉ is the finest topology making πΉ continuous, i.e. the final topology with respect to the family {πΉ}. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ ((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β πΎ β (π½ qTop πΉ)) | ||
Theorem | qtopeu 23441* | Universal property of the quotient topology. If πΊ is a function from π½ to πΎ which is equal on all equivalent elements under πΉ, then there is a unique continuous map π:(π½ / πΉ)βΆπΎ such that πΊ = π β πΉ, and we say that πΊ "passes to the quotient". (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ:πβontoβπ) & β’ (π β πΊ β (π½ Cn πΎ)) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ (πΉβπ₯) = (πΉβπ¦))) β (πΊβπ₯) = (πΊβπ¦)) β β’ (π β β!π β ((π½ qTop πΉ) Cn πΎ)πΊ = (π β πΉ)) | ||
Theorem | qtoprest 23442 | If π΄ is a saturated open or closed set (where saturated means that π΄ = (β‘πΉ β π) for some π), then the restriction of the quotient map πΉ to π΄ is a quotient map. (Contributed by Mario Carneiro, 24-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ:πβontoβπ) & β’ (π β π β π) & β’ (π β π΄ = (β‘πΉ β π)) & β’ (π β (π΄ β π½ β¨ π΄ β (Clsdβπ½))) β β’ (π β ((π½ qTop πΉ) βΎt π) = ((π½ βΎt π΄) qTop (πΉ βΎ π΄))) | ||
Theorem | qtopomap 23443* | If πΉ is a surjective continuous open map, then it is a quotient map. (An open map is a function that maps open sets to open sets.) (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β ran πΉ = π) & β’ ((π β§ π₯ β π½) β (πΉ β π₯) β πΎ) β β’ (π β πΎ = (π½ qTop πΉ)) | ||
Theorem | qtopcmap 23444* | If πΉ is a surjective continuous closed map, then it is a quotient map. (A closed map is a function that maps closed sets to closed sets.) (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β ran πΉ = π) & β’ ((π β§ π₯ β (Clsdβπ½)) β (πΉ β π₯) β (ClsdβπΎ)) β β’ (π β πΎ = (π½ qTop πΉ)) | ||
Theorem | imastopn 23445 | The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ π½ = (TopOpenβπ ) & β’ π = (TopOpenβπ) β β’ (π β π = (π½ qTop πΉ)) | ||
Theorem | imastps 23446 | The image of a topological space under a function is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β TopSp) β β’ (π β π β TopSp) | ||
Theorem | qustps 23447 | A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ (π β π = (π /s πΈ)) & β’ (π β π = (Baseβπ )) & β’ (π β πΈ β π) & β’ (π β π β TopSp) β β’ (π β π β TopSp) | ||
Theorem | kqfval 23448* | Value of the function appearing in df-kq 23419. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β π β§ π΄ β π) β (πΉβπ΄) = {π¦ β π½ β£ π΄ β π¦}) | ||
Theorem | kqfeq 23449* | Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β π β§ π΄ β π β§ π΅ β π) β ((πΉβπ΄) = (πΉβπ΅) β βπ¦ β π½ (π΄ β π¦ β π΅ β π¦))) | ||
Theorem | kqffn 23450* | The topological indistinguishability map is a function on the base. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β π β πΉ Fn π) | ||
Theorem | kqval 23451* | Value of the quotient topology function. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β (TopOnβπ) β (KQβπ½) = (π½ qTop πΉ)) | ||
Theorem | kqtopon 23452* | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β (TopOnβπ) β (KQβπ½) β (TopOnβran πΉ)) | ||
Theorem | kqid 23453* | The topological indistinguishability map is a continuous function into the Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β (TopOnβπ) β πΉ β (π½ Cn (KQβπ½))) | ||
Theorem | ist0-4 23454* | The topological indistinguishability map is injective iff the space is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β (TopOnβπ) β (π½ β Kol2 β πΉ:πβ1-1βV)) | ||
Theorem | kqfvima 23455* | When the image set is open, the quotient map satisfies a partial converse to fnfvima 7237, which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β (π΄ β π β (πΉβπ΄) β (πΉ β π))) | ||
Theorem | kqsat 23456* | Any open set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 23442). (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ π β π½) β (β‘πΉ β (πΉ β π)) = π) | ||
Theorem | kqdisj 23457* | A version of imain 6633 for the topological indistinguishability map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ π β π½) β ((πΉ β π) β© (πΉ β (π΄ β π))) = β ) | ||
Theorem | kqcldsat 23458* | Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 23442). (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (β‘πΉ β (πΉ β π)) = π) | ||
Theorem | kqopn 23459* | The topological indistinguishability map is an open map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ π β π½) β (πΉ β π) β (KQβπ½)) | ||
Theorem | kqcld 23460* | The topological indistinguishability map is a closed map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (πΉ β π) β (Clsdβ(KQβπ½))) | ||
Theorem | kqt0lem 23461* | Lemma for kqt0 23471. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β (TopOnβπ) β (KQβπ½) β Kol2) | ||
Theorem | isr0 23462* | The property "π½ is an R0 space". A space is R0 if any two topologically distinguishable points are separated (there is an open set containing each one and disjoint from the other). Or in contraposition, if every open set which contains π₯ also contains π¦, so there is no separation, then π₯ and π¦ are members of the same open sets. We have chosen not to give this definition a name, because it turns out that a space is R0 if and only if its Kolmogorov quotient is T1, so that is what we prove here. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β (TopOnβπ) β ((KQβπ½) β Fre β βπ§ β π βπ€ β π (βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π)))) | ||
Theorem | r0cld 23463* | The analogue of the T1 axiom (singletons are closed) for an R0 space. In an R0 space the set of all points topologically indistinguishable from π΄ is closed. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β {π§ β π β£ βπ β π½ (π§ β π β π΄ β π)} β (Clsdβπ½)) | ||
Theorem | regr1lem 23464* | Lemma for regr1 23475. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π½ β Reg) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β π½) & β’ (π β Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β )) β β’ (π β (π΄ β π β π΅ β π)) | ||
Theorem | regr1lem2 23465* | A Kolmogorov quotient of a regular space is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (KQβπ½) β Haus) | ||
Theorem | kqreglem1 23466* | A Kolmogorov quotient of a regular space is regular. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (KQβπ½) β Reg) | ||
Theorem | kqreglem2 23467* | If the Kolmogorov quotient of a space is regular then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Reg) β π½ β Reg) | ||
Theorem | kqnrmlem1 23468* | A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ π½ β Nrm) β (KQβπ½) β Nrm) | ||
Theorem | kqnrmlem2 23469* | If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Nrm) β π½ β Nrm) | ||
Theorem | kqtop 23470 | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β Top β (KQβπ½) β Top) | ||
Theorem | kqt0 23471 | The Kolmogorov quotient is T0 even if the original topology is not. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β Top β (KQβπ½) β Kol2) | ||
Theorem | kqf 23472 | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ KQ:TopβΆKol2 | ||
Theorem | r0sep 23473* | The separation property of an R0 space. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π΄ β π β§ π΅ β π)) β (βπ β π½ (π΄ β π β π΅ β π) β βπ β π½ (π΄ β π β π΅ β π))) | ||
Theorem | nrmr0reg 23474 | A normal R0 space is also regular. These spaces are usually referred to as normal regular spaces. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Nrm β§ (KQβπ½) β Fre) β π½ β Reg) | ||
Theorem | regr1 23475 | A regular space is R1, which means that any two topologically distinct points can be separated by neighborhoods. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β Reg β (KQβπ½) β Haus) | ||
Theorem | kqreg 23476 | The Kolmogorov quotient of a regular space is regular. By regr1 23475 it is also Hausdorff, so we can also say that a space is regular iff the Kolmogorov quotient is regular Hausdorff (T3). (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β Reg β (KQβπ½) β Reg) | ||
Theorem | kqnrm 23477 | The Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β Nrm β (KQβπ½) β Nrm) | ||
Syntax | chmeo 23478 | Extend class notation with the class of all homeomorphisms. |
class Homeo | ||
Syntax | chmph 23479 | Extend class notation with the relation "is homeomorphic to.". |
class β | ||
Definition | df-hmeo 23480* | Function returning all the homeomorphisms from topology π to topology π. (Contributed by FL, 14-Feb-2007.) |
β’ Homeo = (π β Top, π β Top β¦ {π β (π Cn π) β£ β‘π β (π Cn π)}) | ||
Definition | df-hmph 23481 | Definition of the relation π₯ is homeomorphic to π¦. (Contributed by FL, 14-Feb-2007.) |
β’ β = (β‘Homeo β (V β 1o)) | ||
Theorem | hmeofn 23482 | The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ Homeo Fn (Top Γ Top) | ||
Theorem | hmeofval 23483* | The set of all the homeomorphisms between two topologies. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π½HomeoπΎ) = {π β (π½ Cn πΎ) β£ β‘π β (πΎ Cn π½)} | ||
Theorem | ishmeo 23484 | The predicate F is a homeomorphism between topology π½ and topology πΎ. Criterion of [BourbakiTop1] p. I.2. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (πΉ β (π½HomeoπΎ) β (πΉ β (π½ Cn πΎ) β§ β‘πΉ β (πΎ Cn π½))) | ||
Theorem | hmeocn 23485 | A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ (πΉ β (π½HomeoπΎ) β πΉ β (π½ Cn πΎ)) | ||
Theorem | hmeocnvcn 23486 | The converse of a homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ (πΉ β (π½HomeoπΎ) β β‘πΉ β (πΎ Cn π½)) | ||
Theorem | hmeocnv 23487 | The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (πΉ β (π½HomeoπΎ) β β‘πΉ β (πΎHomeoπ½)) | ||
Theorem | hmeof1o2 23488 | A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β (π½HomeoπΎ)) β πΉ:πβ1-1-ontoβπ) | ||
Theorem | hmeof1o 23489 | A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 30-May-2014.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (πΉ β (π½HomeoπΎ) β πΉ:πβ1-1-ontoβπ) | ||
Theorem | hmeoima 23490 | The image of an open set by a homeomorphism is an open set. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ ((πΉ β (π½HomeoπΎ) β§ π΄ β π½) β (πΉ β π΄) β πΎ) | ||
Theorem | hmeoopn 23491 | Homeomorphisms preserve openness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½HomeoπΎ) β§ π΄ β π) β (π΄ β π½ β (πΉ β π΄) β πΎ)) | ||
Theorem | hmeocld 23492 | Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½HomeoπΎ) β§ π΄ β π) β (π΄ β (Clsdβπ½) β (πΉ β π΄) β (ClsdβπΎ))) | ||
Theorem | hmeocls 23493 | Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½HomeoπΎ) β§ π΄ β π) β ((clsβπΎ)β(πΉ β π΄)) = (πΉ β ((clsβπ½)βπ΄))) | ||
Theorem | hmeontr 23494 | Homeomorphisms preserve interiors. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½HomeoπΎ) β§ π΄ β π) β ((intβπΎ)β(πΉ β π΄)) = (πΉ β ((intβπ½)βπ΄))) | ||
Theorem | hmeoimaf1o 23495* | The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015.) |
β’ πΊ = (π₯ β π½ β¦ (πΉ β π₯)) β β’ (πΉ β (π½HomeoπΎ) β πΊ:π½β1-1-ontoβπΎ) | ||
Theorem | hmeores 23496 | The restriction of a homeomorphism is a homeomorphism. (Contributed by Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½HomeoπΎ) β§ π β π) β (πΉ βΎ π) β ((π½ βΎt π)Homeo(πΎ βΎt (πΉ β π)))) | ||
Theorem | hmeoco 23497 | The composite of two homeomorphisms is a homeomorphism. (Contributed by FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
β’ ((πΉ β (π½HomeoπΎ) β§ πΊ β (πΎHomeoπΏ)) β (πΊ β πΉ) β (π½HomeoπΏ)) | ||
Theorem | idhmeo 23498 | The identity function is a homeomorphism. (Contributed by FL, 14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
β’ (π½ β (TopOnβπ) β ( I βΎ π) β (π½Homeoπ½)) | ||
Theorem | hmeocnvb 23499 | The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
β’ (Rel πΉ β (β‘πΉ β (π½HomeoπΎ) β πΉ β (πΎHomeoπ½))) | ||
Theorem | hmeoqtop 23500 | A homeomorphism is a quotient map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ (πΉ β (π½HomeoπΎ) β πΎ = (π½ qTop πΉ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |