Home | Metamath
Proof Explorer Theorem List (p. 216 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | qtopres 21501 | 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 21502 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
qTop | ||
Theorem | qtoptop 21503 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
qTop | ||
Theorem | elqtop2 21504 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
qTop | ||
Theorem | qtopuni 21505 | The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
qTop | ||
Theorem | elqtop3 21506 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
TopOn qTop | ||
Theorem | qtoptopon 21507 | The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
TopOn qTop TopOn | ||
Theorem | qtopid 21508 | A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
TopOn qTop | ||
Theorem | idqtop 21509 | The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
TopOn qTop | ||
Theorem | qtopcmplem 21510 | Lemma for qtopcmp 21511 and qtopconn 21512. (Contributed by Mario Carneiro, 24-Mar-2015.) |
qTop qTop qTop qTop | ||
Theorem | qtopcmp 21511 | A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.) |
qTop | ||
Theorem | qtopconn 21512 | A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
Conn qTop Conn | ||
Theorem | qtopkgen 21513 | A quotient of a compactly generated space is compactly generated. (Contributed by Mario Carneiro, 9-Apr-2015.) |
𝑘Gen qTop 𝑘Gen | ||
Theorem | basqtop 21514 | An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.) |
qTop | ||
Theorem | tgqtop 21515 | An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015.) |
qTop qTop | ||
Theorem | qtopcld 21516 | The property of being a closed set in the quotient topology. (Contributed by Mario Carneiro, 24-Mar-2015.) |
TopOn qTop | ||
Theorem | qtopcn 21517 | Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015.) |
TopOn TopOn qTop | ||
Theorem | qtopss 21518 | 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 21508, 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.) |
TopOn qTop | ||
Theorem | qtopeu 21519* | 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 qTop | ||
Theorem | qtoprest 21520 | 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 qTop ↾t ↾t qTop | ||
Theorem | qtopomap 21521* | 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 qTop | ||
Theorem | qtopcmap 21522* | 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 qTop | ||
Theorem | imastopn 21523 | The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015.) |
s qTop | ||
Theorem | imastps 21524 | The image of a topological space under a function is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
s | ||
Theorem | qustps 21525 | A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
s | ||
Theorem | kqfval 21526* | Value of the function appearing in df-kq 21497. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | kqfeq 21527* | Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | kqffn 21528* | The topological indistinguishability map is a function on the base. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | kqval 21529* | Value of the quotient topology function. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ qTop | ||
Theorem | kqtopon 21530* | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ TopOn | ||
Theorem | kqid 21531* | The topological indistinguishability map is a continuous function into the Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ | ||
Theorem | ist0-4 21532* | The topological indistinguishability map is injective iff the space is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn | ||
Theorem | kqfvima 21533* | When the image set is open, the quotient map satisfies a partial converse to fnfvima 6496, which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn | ||
Theorem | kqsat 21534* | Any open set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 21520). (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn | ||
Theorem | kqdisj 21535* | A version of imain 5974 for the topological indistinguishability map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn | ||
Theorem | kqcldsat 21536* | Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 21520). (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn | ||
Theorem | kqopn 21537* | The topological indistinguishability map is an open map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ | ||
Theorem | kqcld 21538* | The topological indistinguishability map is a closed map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ | ||
Theorem | kqt0lem 21539* | Lemma for kqt0 21549. (Contributed by Mario Carneiro, 23-Mar-2015.) |
TopOn KQ | ||
Theorem | isr0 21540* | 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 | ||
Theorem | r0cld 21541* | 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 | ||
Theorem | regr1lem 21542* | Lemma for regr1 21553. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ KQ | ||
Theorem | regr1lem2 21543* | A Kolmogorov quotient of a regular space is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ | ||
Theorem | kqreglem1 21544* | A Kolmogorov quotient of a regular space is regular. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ | ||
Theorem | kqreglem2 21545* | If the Kolmogorov quotient of a space is regular then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ | ||
Theorem | kqnrmlem1 21546* | A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ | ||
Theorem | kqnrmlem2 21547* | If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ | ||
Theorem | kqtop 21548 | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
KQ | ||
Theorem | kqt0 21549 | The Kolmogorov quotient is T0 even if the original topology is not. (Contributed by Mario Carneiro, 25-Aug-2015.) |
KQ | ||
Theorem | kqf 21550 | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
KQ | ||
Theorem | r0sep 21551* | The separation property of an R0 space. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn KQ | ||
Theorem | nrmr0reg 21552 | A normal R0 space is also regular. These spaces are usually referred to as normal regular spaces. (Contributed by Mario Carneiro, 25-Aug-2015.) |
KQ | ||
Theorem | regr1 21553 | 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.) |
KQ | ||
Theorem | kqreg 21554 | The Kolmogorov quotient of a regular space is regular. By regr1 21553 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.) |
KQ | ||
Theorem | kqnrm 21555 | The Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.) |
KQ | ||
Syntax | chmeo 21556 | Extend class notation with the class of all homeomorphisms. |
Syntax | chmph 21557 | Extend class notation with the relation "is homeomorphic to.". |
Definition | df-hmeo 21558* | Function returning all the homeomorphisms from topology to topology . (Contributed by FL, 14-Feb-2007.) |
Definition | df-hmph 21559 | Definition of the relation is homeomorphic to . (Contributed by FL, 14-Feb-2007.) |
Theorem | hmeofn 21560 | The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015.) |
Theorem | hmeofval 21561* | The set of all the homeomorphisms between two topologies. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Theorem | ishmeo 21562 | The predicate F is a homeomorphism between topology and topology . Proposition of [BourbakiTop1] p. I.2. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Theorem | hmeocn 21563 | A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.) |
Theorem | hmeocnvcn 21564 | The converse of a homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.) |
Theorem | hmeocnv 21565 | The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Theorem | hmeof1o2 21566 | A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro, 22-Aug-2015.) |
TopOn TopOn | ||
Theorem | hmeof1o 21567 | A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 30-May-2014.) |
Theorem | hmeoima 21568 | 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.) |
Theorem | hmeoopn 21569 | Homeomorphisms preserve openness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
Theorem | hmeocld 21570 | Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
Theorem | hmeocls 21571 | Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | hmeontr 21572 | Homeomorphisms preserve interiors. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | hmeoimaf1o 21573* | The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015.) |
Theorem | hmeores 21574 | The restriction of a homeomorphism is a homeomorphism. (Contributed by Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
↾t ↾t | ||
Theorem | hmeoco 21575 | The composite of two homeomorphisms is a homeomorphism. (Contributed by FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
Theorem | idhmeo 21576 | The identity function is a homeomorphism. (Contributed by FL, 14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
TopOn | ||
Theorem | hmeocnvb 21577 | The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | hmeoqtop 21578 | A homeomorphism is a quotient map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
qTop | ||
Theorem | hmph 21579 | Express the predicate is homeomorphic to . (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Theorem | hmphi 21580 | If there is a homeomorphism between spaces, then the spaces are homeomorphic. (Contributed by Mario Carneiro, 23-Aug-2015.) |
Theorem | hmphtop 21581 | Reverse closure for the homeomorphic predicate. (Contributed by Mario Carneiro, 22-Aug-2015.) |
Theorem | hmphtop1 21582 | The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | hmphtop2 21583 | The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | hmphref 21584 | "Is homeomorphic to" is reflexive. (Contributed by FL, 25-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
Theorem | hmphsym 21585 | "Is homeomorphic to" is symmetric. (Contributed by FL, 8-Mar-2007.) (Proof shortened by Mario Carneiro, 30-May-2014.) |
Theorem | hmphtr 21586 | "Is homeomorphic to" is transitive. (Contributed by FL, 9-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | hmpher 21587 | "Is homeomorphic to" is an equivalence relation. (Contributed by FL, 22-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | hmphen 21588 | Homeomorphisms preserve the cardinality of the topologies. (Contributed by FL, 1-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
Theorem | hmphsymb 21589 | "Is homeomorphic to" is symmetric. (Contributed by FL, 22-Feb-2007.) |
Theorem | haushmphlem 21590* | Lemma for haushmph 21595 and similar theorems. If the topological property is preserved under injective preimages, then property is preserved under homeomorphisms. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | cmphmph 21591 | Compactness is a topological property-that is, for any two homeomorphic topologies, either both are compact or neither is. (Contributed by Jeff Hankins, 30-Jun-2009.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | connhmph 21592 | Connectedness is a topological property. (Contributed by Jeff Hankins, 3-Jul-2009.) |
Conn Conn | ||
Theorem | t0hmph 21593 | T0 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | t1hmph 21594 | T1 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | haushmph 21595 | Hausdorff-ness is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | reghmph 21596 | Regularity is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | nrmhmph 21597 | Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | hmph0 21598 | A topology homeomorphic to the empty set is empty. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
Theorem | hmphdis 21599 | Homeomorphisms preserve topological discretion. (Contributed by Mario Carneiro, 10-Sep-2015.) |
Theorem | hmphindis 21600 | Homeomorphisms preserve topological indiscretion. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |