Home | Metamath
Proof Explorer Theorem List (p. 228 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 | cncffvrn 22701 | Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
Theorem | cncfss 22702 | The set of continuous functions is expanded when the range is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
Theorem | climcncf 22703 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
Theorem | abscncf 22704 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
Theorem | recncf 22705 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
Theorem | imcncf 22706 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
Theorem | cjcncf 22707 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
Theorem | mulc1cncf 22708* | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
Theorem | divccncf 22709* | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
Theorem | cncfco 22710 | The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Aug-2014.) |
Theorem | cncfmet 22711 | Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
Theorem | cncfcn 22712 | Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.) |
ℂfld ↾t ↾t | ||
Theorem | cncfcn1 22713 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
ℂfld | ||
Theorem | cncfmptc 22714* | A constant function is a continuous function on . (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Sep-2015.) |
Theorem | cncfmptid 22715* | The identity function is a continuous function on . (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 17-May-2016.) |
Theorem | cncfmpt1f 22716* | Composition of continuous functions. analogue of cnmpt11f 21467. (Contributed by Mario Carneiro, 3-Sep-2014.) |
Theorem | cncfmpt2f 22717* | Composition of continuous functions. analogue of cnmpt12f 21469. (Contributed by Mario Carneiro, 3-Sep-2014.) |
ℂfld | ||
Theorem | cncfmpt2ss 22718* | Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.) |
ℂfld | ||
Theorem | addccncf 22719* | Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
Theorem | cdivcncf 22720* | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) |
Theorem | negcncf 22721* | The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) |
Theorem | negfcncf 22722* | The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
Theorem | abscncfALT 22723 | Absolute value is continuous. Alternate proof of abscncf 22704. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | cncfcnvcn 22724 | Rewrite cmphaushmeo 21603 for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015.) |
ℂfld ↾t | ||
Theorem | expcncf 22725* | The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 22675. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | cnmptre 22726* | Lemma for iirevcn 22729 and related functions. (Contributed by Mario Carneiro, 6-Jun-2014.) |
ℂfld ↾t ↾t | ||
Theorem | cnmpt2pc 22727* | Piecewise definition of a continuous function on a real interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.) |
↾t ↾t ↾t TopOn | ||
Theorem | iirev 22728 | Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iirevcn 22729 | The reversion function is a continuous map of the unit interval. (Contributed by Mario Carneiro, 6-Jun-2014.) |
Theorem | iihalf1 22730 | Map the first half of into . (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iihalf1cn 22731 | The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) |
↾t | ||
Theorem | iihalf2 22732 | Map the second half of into . (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iihalf2cn 22733 | The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) |
↾t | ||
Theorem | elii1 22734 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
Theorem | elii2 22735 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
Theorem | iimulcl 22736 | The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iimulcn 22737* | Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014.) |
Theorem | icoopnst 22738 | A half-open interval starting at is open in the closed interval from to . (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
Theorem | iocopnst 22739 | A half-open interval ending at is open in the closed interval from to . (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
Theorem | icchmeo 22740* | The natural bijection from to an arbitrary nontrivial closed interval is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) |
ℂfld ↾t | ||
Theorem | icopnfcnv 22741* | Define a bijection from to . (Contributed by Mario Carneiro, 9-Sep-2015.) |
Theorem | icopnfhmeo 22742* | The defined bijection from to is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.) |
ℂfld ↾t ↾t | ||
Theorem | iccpnfcnv 22743* | Define a bijection from to . (Contributed by Mario Carneiro, 9-Sep-2015.) |
Theorem | iccpnfhmeo 22744 | The defined bijection from to is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) |
ordTop ↾t | ||
Theorem | xrhmeo 22745* | The bijection from to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.) |
ℂfld ordTop ↾t ordTop | ||
Theorem | xrhmph 22746 | The extended reals are homeomorphic to the interval . (Contributed by Mario Carneiro, 9-Sep-2015.) |
ordTop | ||
Theorem | xrcmp 22747 | The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo 22609), this means that is a compactification of . (Contributed by Mario Carneiro, 9-Sep-2015.) |
ordTop | ||
Theorem | xrconn 22748 | The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015.) |
ordTop Conn | ||
Theorem | icccvx 22749 | A linear combination of two reals lies in the interval between them. Equivalently, a closed interval is a convex set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | oprpiece1res1 22750* | Restriction to the first part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.) |
Theorem | oprpiece1res2 22751* | Restriction to the second part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.) |
Theorem | cnrehmeo 22752* | The canonical bijection from to described in cnref1o 11827 is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if is metrized with the l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro, 25-Aug-2014.) |
ℂfld | ||
Theorem | cnheiborlem 22753* | Lemma for cnheibor 22754. (Contributed by Mario Carneiro, 14-Sep-2014.) |
ℂfld ↾t | ||
Theorem | cnheibor 22754* | Heine-Borel theorem for complex numbers. A subset of is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014.) |
ℂfld ↾t | ||
Theorem | cnllycmp 22755 | The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
ℂfld 𝑛Locally | ||
Theorem | rellycmp 22756 | The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally | ||
Theorem | bndth 22757* | The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to .) (Contributed by Mario Carneiro, 12-Aug-2014.) |
Theorem | evth 22758* | The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.) |
Theorem | evth2 22759* | The Extreme Value Theorem, minimum version. A continuous function from a nonempty compact topological space to the reals attains its minimum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.) |
Theorem | lebnumlem1 22760* | Lemma for lebnum 22763. The function measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.) |
inf | ||
Theorem | lebnumlem2 22761* | Lemma for lebnum 22763. As a finite sum of point-to-set distance functions, which are continuous by metdscn 22659, the function is also continuous. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.) |
inf | ||
Theorem | lebnumlem3 22762* | Lemma for lebnum 22763. By the previous lemmas, is continuous and positive on a compact set, so it has a positive minimum . Then setting , since for each we have iff , if for all then summing over yields , in contradiction to the assumption that is the minimum of . (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) (Revised by AV, 30-Sep-2020.) |
inf | ||
Theorem | lebnum 22763* | The Lebesgue number lemma, or Lebesgue covering lemma. If is a compact metric space and is an open cover of , then there exists a positive real number such that every ball of size (and every subset of a ball of size , including every subset of diameter less than ) is a subset of some member of the cover. (Contributed by Mario Carneiro, 14-Feb-2015.) (Proof shortened by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.) |
Theorem | xlebnum 22764* | Generalize lebnum 22763 to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015.) |
Theorem | lebnumii 22765* | Specialize the Lebesgue number lemma lebnum 22763 to the unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.) |
Syntax | chtpy 22766 | Extend class notation with the class of homotopies between two continuous functions. |
Htpy | ||
Syntax | cphtpy 22767 | Extend class notation with the class of path homotopies between two continuous functions. |
Syntax | cphtpc 22768 | Extend class notation with the path homotopy relation. |
Definition | df-htpy 22769* | Define the function which takes topological spaces and two continuous functions and returns the class of homotopies from to . (Contributed by Mario Carneiro, 22-Feb-2015.) |
Htpy | ||
Definition | df-phtpy 22770* | Define the class of path homotopies between two paths ; these are homotopies (in the sense of df-htpy 22769) which also preserve both endpoints of the paths throughout the homotopy. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Htpy | ||
Theorem | ishtpy 22771* | Membership in the class of homotopies between two continuous functions. (Contributed by Mario Carneiro, 22-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) |
TopOn Htpy | ||
Theorem | htpycn 22772 | A homotopy is a continuous function. (Contributed by Mario Carneiro, 22-Feb-2015.) |
TopOn Htpy | ||
Theorem | htpyi 22773 | A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015.) |
TopOn Htpy | ||
Theorem | ishtpyd 22774* | Deduction for membership in the class of homotopies. (Contributed by Mario Carneiro, 22-Feb-2015.) |
TopOn Htpy | ||
Theorem | htpycom 22775* | Given a homotopy from to , produce a homotopy from to . (Contributed by Mario Carneiro, 23-Feb-2015.) |
TopOn Htpy Htpy | ||
Theorem | htpyid 22776* | A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015.) |
TopOn Htpy | ||
Theorem | htpyco1 22777* | Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
TopOn Htpy Htpy | ||
Theorem | htpyco2 22778 | Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
Htpy Htpy | ||
Theorem | htpycc 22779* | Concatenate two homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
TopOn Htpy Htpy Htpy | ||
Theorem | isphtpy 22780* | Membership in the class of path homotopies between two continuous functions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
Htpy | ||
Theorem | phtpyhtpy 22781 | A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Htpy | ||
Theorem | phtpycn 22782 | A path homotopy is a continuous function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Theorem | phtpyi 22783 | Membership in the class of path homotopies between two continuous functions. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Theorem | phtpy01 22784 | Two path-homotopic paths have the same start and end point. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Theorem | isphtpyd 22785* | Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Htpy | ||
Theorem | isphtpy2d 22786* | Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Theorem | phtpycom 22787* | Given a homotopy from to , produce a homotopy from to . (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
Theorem | phtpyid 22788* | A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
Theorem | phtpyco2 22789 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
Theorem | phtpycc 22790* | Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
Definition | df-phtpc 22791* | Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.) |
Theorem | phtpcrel 22792 | The path homotopy relation is a relation. (Contributed by Mario Carneiro, 7-Jun-2014.) (Revised by Mario Carneiro, 7-Aug-2014.) |
Theorem | isphtpc 22793 | The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Sep-2015.) |
Theorem | phtpcer 22794 | Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 6-Jul-2015.) (Proof shortened by AV, 1-May-2021.) |
Theorem | phtpcerOLD 22795 | Obsolete proof of phtpcer 22794 as of 1-May-2021. Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 6-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | phtpc01 22796 | Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | reparphti 22797* | Lemma for reparpht 22798. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) |
Theorem | reparpht 22798 | Reparametrization lemma. The reparametrization of a path by any continuous map with and is path-homotopic to the original path. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Feb-2015.) |
Theorem | phtpcco2 22799 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.) |
Syntax | cpco 22800 | Extend class notation with the concatenation operation for paths in a topological space. |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |