Home | Metamath
Proof Explorer Theorem List (p. 300 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 | txomap 29901* | Given two open maps and , mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019.) |
TopOn TopOn TopOn TopOn | ||
Theorem | qtopt1 29902* | If every equivalence class is closed, then the quotient space is T1 . (Contributed by Thierry Arnoux, 5-Jan-2020.) |
qTop | ||
Theorem | qtophaus 29903* | If an open map's graph in the product space is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
qTop qTop | ||
Theorem | circtopn 29904* | The topology of the unit circle is generated by open intervals of the polar coordinate. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
qTop s RRfld | ||
Theorem | circcn 29905* | The function gluing the real line into the unit circle is continuous. (Contributed by Thierry Arnoux, 5-Jan-2020.) |
qTop | ||
Theorem | reff 29906* | For any cover refinement, there exists a function associating with each set in the refinement a set in the original cover containing it. This is sometimes used as a defintion of refinement. Note that this definition uses the axiom of choice through ac6sg 9310. (Contributed by Thierry Arnoux, 12-Jan-2020.) |
Theorem | locfinreflem 29907* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function from the original cover , which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.) |
Theorem | locfinref 29908* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function from the original cover , which is taken as the index set. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
Syntax | ccref 29909 | The "every open cover has an refinement" predicate. |
CovHasRef | ||
Definition | df-cref 29910* | Define a statement "every open cover has an refinement" , where is a property for refinements like "finite", "countable", "point finite" or "locally finite". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
CovHasRef | ||
Theorem | iscref 29911* | The property that every open cover has an refinement for the topological space . (Contributed by Thierry Arnoux, 7-Jan-2020.) |
CovHasRef | ||
Theorem | crefeq 29912 | Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
CovHasRef CovHasRef | ||
Theorem | creftop 29913 | A space where every open cover has an refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
CovHasRef | ||
Theorem | crefi 29914* | The property that every open cover has an refinement for the topological space . (Contributed by Thierry Arnoux, 7-Jan-2020.) |
CovHasRef | ||
Theorem | crefdf 29915* | A formulation of crefi 29914 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
CovHasRef | ||
Theorem | crefss 29916 | The "every open cover has an refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
CovHasRef CovHasRef | ||
Theorem | cmpcref 29917 | Equivalent definition of compact space in terms of open cover refinements. Compact spaces are topologies with finite open cover refinements. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
CovHasRef | ||
Theorem | cmpfiref 29918* | Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
Syntax | cldlf 29919 | Extend class notation with the class of all Lindelöf spaces. |
Ldlf | ||
Definition | df-ldlf 29920 | Definition of a Lindelöf space. A Lindelöf space is a topological space in which every open cover has a countable subcover. Definition 1 of [BourbakiTop2] p. 195. (Contributed by Thierry Arnoux, 30-Jan-2020.) |
Ldlf CovHasRef | ||
Theorem | ldlfcntref 29921* | Every open cover of a Lindelöf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
Ldlf | ||
Syntax | cpcmp 29922 | Extend class notation with the class of all paracompact topologies. |
Paracomp | ||
Definition | df-pcmp 29923 | Definition of a paracompact topology. A topology is said to be paracompact iff every open cover has an open refinement that is locally finite. The definition 6 of [BourbakiTop1] p. I.69. also requires the topology to be Hausdorff, but this is dropped here. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
Paracomp CovHasRef | ||
Theorem | ispcmp 29924 | The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
Paracomp CovHasRef | ||
Theorem | cmppcmp 29925 | Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
Paracomp | ||
Theorem | dispcmp 29926 | Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
Paracomp | ||
Theorem | pcmplfin 29927* | Given a paracompact topology and an open cover , there exists an open refinement that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
Paracomp | ||
Theorem | pcmplfinf 29928* | Given a paracompact topology and an open cover , there exists an open refinement that is locally finite, using the same index as the original cover . (Contributed by Thierry Arnoux, 31-Jan-2020.) |
Paracomp | ||
Syntax | cmetid 29929 | Extend class notation with the class of metric identifications. |
~Met | ||
Syntax | cpstm 29930 | Extend class notation with the metric induced by a pseudometric. |
pstoMet | ||
Definition | df-metid 29931* | Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
~Met PsMet | ||
Definition | df-pstm 29932* | Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
pstoMet PsMet ~Met ~Met | ||
Theorem | metidval 29933* | Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet ~Met | ||
Theorem | metidss 29934 | As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet ~Met | ||
Theorem | metidv 29935 | and identify by the metric if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet ~Met | ||
Theorem | metideq 29936 | Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
PsMet ~Met ~Met | ||
Theorem | metider 29937 | The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
PsMet ~Met | ||
Theorem | pstmval 29938* | Value of the metric induced by a pseudometric . (Contributed by Thierry Arnoux, 7-Feb-2018.) |
~Met PsMet pstoMet | ||
Theorem | pstmfval 29939 | Function value of the metric induced by a pseudometric (Contributed by Thierry Arnoux, 11-Feb-2018.) |
~Met PsMet pstoMet | ||
Theorem | pstmxmet 29940 | The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
~Met PsMet pstoMet | ||
Theorem | hauseqcn 29941 | In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28-Dec-2017.) |
Theorem | unitsscn 29942 | The closed unit is a subset of the set of the complex numbers Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
Theorem | elunitrn 29943 | The closed unit is a subset of the set of the real numbers Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 21-Dec-2016.) |
Theorem | elunitcn 29944 | The closed unit is a subset of the set of the complext numbers Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 21-Dec-2016.) |
Theorem | elunitge0 29945 | An element of the closed unit is positive Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 20-Dec-2016.) |
Theorem | unitssxrge0 29946 | The closed unit is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
Theorem | unitdivcld 29947 | Necessary conditions for a quotient to be in the closed unit. (somewhat too strong, it would be sufficient that A and B are in RR+) (Contributed by Thierry Arnoux, 20-Dec-2016.) |
Theorem | iistmd 29948 | The closed unit forms a topological monoid. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
mulGrpℂfld ↾s TopMnd | ||
Theorem | unicls 29949 | The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
Theorem | tpr2tp 29950 | The usual topology on is the product topology of the usual topology on . (Contributed by Thierry Arnoux, 21-Sep-2017.) |
TopOn | ||
Theorem | tpr2uni 29951 | The usual topology on is the product topology of the usual topology on . (Contributed by Thierry Arnoux, 21-Sep-2017.) |
Theorem | xpinpreima 29952 | Rewrite the cartesian product of two sets as the intersection of their preimage by and , the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
Theorem | xpinpreima2 29953 | Rewrite the cartesian product of two sets as the intersection of their preimage by and , the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
Theorem | sqsscirc1 29954 | The complex square of side is a subset of the complex circle of radius . (Contributed by Thierry Arnoux, 25-Sep-2017.) |
Theorem | sqsscirc2 29955 | The complex square of side is a subset of the complex disc of radius . (Contributed by Thierry Arnoux, 25-Sep-2017.) |
Theorem | cnre2csqlem 29956* | Lemma for cnre2csqima 29957. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
Theorem | cnre2csqima 29957* | Image of a centered square by the canonical bijection from to . (Contributed by Thierry Arnoux, 27-Sep-2017.) |
Theorem | tpr2rico 29958* | For any point of an open set of the usual topology on there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the norm . (Contributed by Thierry Arnoux, 21-Sep-2017.) |
Theorem | cnvordtrestixx 29959* | The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
ordTop ↾t ordTop | ||
Theorem | prsdm 29960 | Domain of the relation of a preset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
Theorem | prsrn 29961 | Range of the relation of a preset. (Contributed by Thierry Arnoux, 11-Sep-2018.) |
Theorem | prsss 29962 | Relation of a subpreset. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
Theorem | prsssdm 29963 | Domain of a subpreset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
Theorem | ordtprsval 29964* | Value of the order topology for a preset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
ordTop | ||
Theorem | ordtprsuni 29965* | Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
Theorem | ordtcnvNEW 29966 | The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) (Revised by Thierry Arnoux, 13-Sep-2018.) |
ordTop ordTop | ||
Theorem | ordtrestNEW 29967 | The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
ordTop ordTop ↾t | ||
Theorem | ordtrest2NEWlem 29968* | Lemma for ordtrest2NEW 29969. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
Toset ordTop | ||
Theorem | ordtrest2NEW 29969* | An interval-closed set in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in , but in other sets like there are interval-closed sets like that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
Toset ordTop ordTop ↾t | ||
Theorem | ordtconnlem1 29970* | Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 29971. See also reconnlem1 22629. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
ordTop Toset ↾t Conn | ||
Theorem | ordtconn 29971 | Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
ordTop | ||
Theorem | mndpluscn 29972* | A mapping that is both a homeomorphism and a monoid homomorphism preserves the "continuousness" of the operation. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
TopOn TopOn | ||
Theorem | mhmhmeotmd 29973 | Deduce a Topological Monoid using mapping that is both a homeomorphism and a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017.) |
MndHom TopMnd TopMnd | ||
Theorem | rmulccn 29974* | Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) |
Theorem | raddcn 29975* | Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) |
Theorem | xrmulc1cn 29976* | The operation multiplying an extended real number by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
ordTop | ||
Theorem | fmcncfil 29977 | The image of a Cauchy filter by a continuous filter map is a Cauchy filter. (Contributed by Thierry Arnoux, 12-Nov-2017.) |
CauFil CauFil | ||
Theorem | xrge0hmph 29978 | The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
ordTop ↾t | ||
Theorem | xrge0iifcnv 29979* | Define a bijection from to . (Contributed by Thierry Arnoux, 29-Mar-2017.) |
Theorem | xrge0iifcv 29980* | The defined function's value in the real. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
Theorem | xrge0iifiso 29981* | The defined bijection from the closed unit interval and the extended nonnegative reals is an order isomorphism. (Contributed by Thierry Arnoux, 31-Mar-2017.) |
Theorem | xrge0iifhmeo 29982* | Expose a homeomorphism from the closed unit interval and the extended nonnegative reals. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
ordTop ↾t | ||
Theorem | xrge0iifhom 29983* | The defined function from the closed unit interval and the extended nonnegative reals is also a monoid homomorphism. (Contributed by Thierry Arnoux, 5-Apr-2017.) |
ordTop ↾t | ||
Theorem | xrge0iif1 29984* | Condition for the defined function, to be a monoid homomorphism. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
ordTop ↾t | ||
Theorem | xrge0iifmhm 29985* | The defined function from the closed unit interval and the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017.) |
ordTop ↾t mulGrpℂfld ↾s MndHom ↾s | ||
Theorem | xrge0pluscn 29986* | The addition operation of the extended nonnegative real numbers monoid is continuous. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
ordTop ↾t | ||
Theorem | xrge0mulc1cn 29987* | The operation multiplying a nonnegative real numbers by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
ordTop ↾t | ||
Theorem | xrge0tps 29988 | The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
↾s | ||
Theorem | xrge0topn 29989 | The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
↾s ordTop ↾t | ||
Theorem | xrge0haus 29990 | The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.) |
↾s | ||
Theorem | xrge0tmdOLD 29991 | The extended nonnegative real numbers monoid is a topological monoid. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
↾s TopMnd | ||
Theorem | xrge0tmd 29992 | The extended nonnegative real numbers monoid is a topological monoid. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof Shortened by Thierry Arnoux, 21-Jun-2017.) |
↾s TopMnd | ||
Theorem | lmlim 29993 | Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017.) |
TopOn ↾t ℂfld ↾t | ||
Theorem | lmlimxrge0 29994 | Relate a limit in the nonnegative extended reals to a complex limit, provided the considered function is a real function. (Contributed by Thierry Arnoux, 11-Jul-2017.) |
↾s | ||
Theorem | rge0scvg 29995 | Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 15625. (Contributed by Thierry Arnoux, 28-Jul-2017.) |
Theorem | fsumcvg4 29996 | A serie with finite support is a finite sum, and therefore converges. (Contributed by Thierry Arnoux, 6-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
Theorem | pnfneige0 29997* | A neighborhood of contains an unbounded interval based at a real number. See pnfnei 21024. (Contributed by Thierry Arnoux, 31-Jul-2017.) |
↾s | ||
Theorem | lmxrge0 29998* | Express "sequence converges to plus infinity" (i.e. diverges), for a sequence of nonnegative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017.) |
↾s | ||
Theorem | lmdvg 29999* | If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
Theorem | lmdvglim 30000* | If a monotonic real number sequence diverges, it converges in the extended real numbers and its limit is plus infinity. (Contributed by Thierry Arnoux, 3-Aug-2017.) |
↾s |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |