![]() |
Metamath
Proof Explorer Theorem List (p. 247 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | addcnlem 24601* | Lemma for addcn 24602, subcn 24603, and mulcn 24604. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (TopOpenββfld) & β’ + :(β Γ β)βΆβ & β’ ((π β β+ β§ π β β β§ π β β) β βπ¦ β β+ βπ§ β β+ βπ’ β β βπ£ β β (((absβ(π’ β π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π)) β β’ + β ((π½ Γt π½) Cn π½) | ||
Theorem | addcn 24602 | Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ + β ((π½ Γt π½) Cn π½) | ||
Theorem | subcn 24603 | Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ β β ((π½ Γt π½) Cn π½) | ||
Theorem | mulcn 24604 | Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ Β· β ((π½ Γt π½) Cn π½) | ||
Theorem | divcnOLD 24605 | Obsolete version of divcn 24607 as of 6-Apr-2025. (Contributed by Mario Carneiro, 12-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt (β β {0})) β β’ / β ((π½ Γt πΎ) Cn π½) | ||
Theorem | mpomulcn 24606* | Complex number multiplication is a continuous function. Version of mulcn 24604 using maps-to notation, which does not require ax-mulf 11193. (Contributed by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) β β’ (π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) β ((π½ Γt π½) Cn π½) | ||
Theorem | divcn 24607 | Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt (β β {0})) β β’ / β ((π½ Γt πΎ) Cn π½) | ||
Theorem | cnfldtgp 24608 | The complex numbers form a topological group under addition, with the standard topology induced by the absolute value metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ βfld β TopGrp | ||
Theorem | fsumcn 24609* | A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for π΅ normally contains free variables π and π₯ to index it. (Contributed by NM, 8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (π½ Cn πΎ)) | ||
Theorem | fsum2cn 24610* | Version of fsumcn 24609 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.) |
β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ (π β πΏ β (TopOnβπ)) & β’ ((π β§ π β π΄) β (π₯ β π, π¦ β π β¦ π΅) β ((π½ Γt πΏ) Cn πΎ)) β β’ (π β (π₯ β π, π¦ β π β¦ Ξ£π β π΄ π΅) β ((π½ Γt πΏ) Cn πΎ)) | ||
Theorem | expcn 24611* | The power function on complex numbers, for fixed exponent π, is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) β β’ (π β β0 β (π₯ β β β¦ (π₯βπ)) β (π½ Cn π½)) | ||
Theorem | divccn 24612* | Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) β β’ ((π΄ β β β§ π΄ β 0) β (π₯ β β β¦ (π₯ / π΄)) β (π½ Cn π½)) | ||
Theorem | expcnOLD 24613* | Obsolete version of expcn 24611 as of 6-Apr-2025. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π½ = (TopOpenββfld) β β’ (π β β0 β (π₯ β β β¦ (π₯βπ)) β (π½ Cn π½)) | ||
Theorem | divccnOLD 24614* | Obsolete version of divccn 24612 as of 6-Apr-2025. (Contributed by Mario Carneiro, 5-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π½ = (TopOpenββfld) β β’ ((π΄ β β β§ π΄ β 0) β (π₯ β β β¦ (π₯ / π΄)) β (π½ Cn π½)) | ||
Theorem | sqcn 24615* | The square function on complex numbers is continuous. (Contributed by NM, 13-Jun-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ (π₯ β β β¦ (π₯β2)) β (π½ Cn π½) | ||
Syntax | cii 24616 | Extend class notation with the unit interval. |
class II | ||
Syntax | ccncf 24617 | Extend class notation to include the operation which returns a class of continuous complex functions. |
class βcnβ | ||
Definition | df-ii 24618 | Define the unit interval with the Euclidean topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ II = (MetOpenβ((abs β β ) βΎ ((0[,]1) Γ (0[,]1)))) | ||
Definition | df-cncf 24619* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
β’ βcnβ = (π β π« β, π β π« β β¦ {π β (π βm π) β£ βπ₯ β π βπ β β+ βπ β β+ βπ¦ β π ((absβ(π₯ β π¦)) < π β (absβ((πβπ₯) β (πβπ¦))) < π)}) | ||
Theorem | iitopon 24620 | The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ II β (TopOnβ(0[,]1)) | ||
Theorem | iitop 24621 | The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ II β Top | ||
Theorem | iiuni 24622 | The base set of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Jan-2014.) |
β’ (0[,]1) = βͺ II | ||
Theorem | dfii2 24623 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ II = ((topGenβran (,)) βΎt (0[,]1)) | ||
Theorem | dfii3 24624 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ II = (π½ βΎt (0[,]1)) | ||
Theorem | dfii4 24625 | Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ πΌ = (βfld βΎs (0[,]1)) β β’ II = (TopOpenβπΌ) | ||
Theorem | dfii5 24626 | The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ II = (ordTopβ( β€ β© ((0[,]1) Γ (0[,]1)))) | ||
Theorem | iicmp 24627 | The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.) |
β’ II β Comp | ||
Theorem | iiconn 24628 | The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ II β Conn | ||
Theorem | cncfval 24629* | The value of the continuous complex function operation is the set of continuous functions from π΄ to π΅. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+ βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦)}) | ||
Theorem | elcncf 24630* | Membership in the set of continuous complex functions from π΄ to π΅. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.) |
β’ ((π΄ β β β§ π΅ β β) β (πΉ β (π΄βcnβπ΅) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+ βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πΉβπ₯) β (πΉβπ€))) < π¦)))) | ||
Theorem | elcncf2 24631* | Version of elcncf 24630 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (πΉ β (π΄βcnβπ΅) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+ βπ€ β π΄ ((absβ(π€ β π₯)) < π§ β (absβ((πΉβπ€) β (πΉβπ₯))) < π¦)))) | ||
Theorem | cncfrss 24632 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ (πΉ β (π΄βcnβπ΅) β π΄ β β) | ||
Theorem | cncfrss2 24633 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ (πΉ β (π΄βcnβπ΅) β π΅ β β) | ||
Theorem | cncff 24634 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
β’ (πΉ β (π΄βcnβπ΅) β πΉ:π΄βΆπ΅) | ||
Theorem | cncfi 24635* | Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.) |
β’ ((πΉ β (π΄βcnβπ΅) β§ πΆ β π΄ β§ π β β+) β βπ§ β β+ βπ€ β π΄ ((absβ(π€ β πΆ)) < π§ β (absβ((πΉβπ€) β (πΉβπΆ))) < π )) | ||
Theorem | elcncf1di 24636* | Membership in the set of continuous complex functions from π΄ to π΅. (Contributed by Paul Chapman, 26-Nov-2007.) |
β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ((π₯ β π΄ β§ π¦ β β+) β π β β+)) & β’ (π β (((π₯ β π΄ β§ π€ β π΄) β§ π¦ β β+) β ((absβ(π₯ β π€)) < π β (absβ((πΉβπ₯) β (πΉβπ€))) < π¦))) β β’ (π β ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnβπ΅))) | ||
Theorem | elcncf1ii 24637* | Membership in the set of continuous complex functions from π΄ to π΅. (Contributed by Paul Chapman, 26-Nov-2007.) |
β’ πΉ:π΄βΆπ΅ & β’ ((π₯ β π΄ β§ π¦ β β+) β π β β+) & β’ (((π₯ β π΄ β§ π€ β π΄) β§ π¦ β β+) β ((absβ(π₯ β π€)) < π β (absβ((πΉβπ₯) β (πΉβπ€))) < π¦)) β β’ ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnβπ΅)) | ||
Theorem | rescncf 24638 | A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 25-Aug-2014.) |
β’ (πΆ β π΄ β (πΉ β (π΄βcnβπ΅) β (πΉ βΎ πΆ) β (πΆβcnβπ΅))) | ||
Theorem | cncfcdm 24639 | Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
β’ ((πΆ β β β§ πΉ β (π΄βcnβπ΅)) β (πΉ β (π΄βcnβπΆ) β πΉ:π΄βΆπΆ)) | ||
Theorem | cncfss 24640 | The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ ((π΅ β πΆ β§ πΆ β β) β (π΄βcnβπ΅) β (π΄βcnβπΆ)) | ||
Theorem | climcncf 24641 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΊ:πβΆπ΄) & β’ (π β πΊ β π·) & β’ (π β π· β π΄) β β’ (π β (πΉ β πΊ) β (πΉβπ·)) | ||
Theorem | abscncf 24642 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ abs β (ββcnββ) | ||
Theorem | recncf 24643 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ β β (ββcnββ) | ||
Theorem | imcncf 24644 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ β β (ββcnββ) | ||
Theorem | cjcncf 24645 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ β β (ββcnββ) | ||
Theorem | mulc1cncf 24646* | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β β β¦ (π΄ Β· π₯)) β β’ (π΄ β β β πΉ β (ββcnββ)) | ||
Theorem | divccncf 24647* | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
β’ πΉ = (π₯ β β β¦ (π₯ / π΄)) β β’ ((π΄ β β β§ π΄ β 0) β πΉ β (ββcnββ)) | ||
Theorem | cncfco 24648 | 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.) |
β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΊ β (π΅βcnβπΆ)) β β’ (π β (πΊ β πΉ) β (π΄βcnβπΆ)) | ||
Theorem | cncfcompt2 24649* | Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ (π β (π₯ β π΄ β¦ π ) β (π΄βcnβπ΅)) & β’ (π β (π¦ β πΆ β¦ π) β (πΆβcnβπΈ)) & β’ (π β π΅ β πΆ) & β’ (π¦ = π β π = π) β β’ (π β (π₯ β π΄ β¦ π) β (π΄βcnβπΈ)) | ||
Theorem | cncfmet 24650 | Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
β’ πΆ = ((abs β β ) βΎ (π΄ Γ π΄)) & β’ π· = ((abs β β ) βΎ (π΅ Γ π΅)) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = (π½ Cn πΎ)) | ||
Theorem | cncfcn 24651 | Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π΄) & β’ πΏ = (π½ βΎt π΅) β β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = (πΎ Cn πΏ)) | ||
Theorem | cncfcn1 24652 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ (ββcnββ) = (π½ Cn π½) | ||
Theorem | cncfmptc 24653* | A constant function is a continuous function on β. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Sep-2015.) |
β’ ((π΄ β π β§ π β β β§ π β β) β (π₯ β π β¦ π΄) β (πβcnβπ)) | ||
Theorem | cncfmptid 24654* | The identity function is a continuous function on β. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 17-May-2016.) |
β’ ((π β π β§ π β β) β (π₯ β π β¦ π₯) β (πβcnβπ)) | ||
Theorem | cncfmpt1f 24655* | Composition of continuous functions. βcnβ analogue of cnmpt11f 23389. (Contributed by Mario Carneiro, 3-Sep-2014.) |
β’ (π β πΉ β (ββcnββ)) & β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (πΉβπ΄)) β (πβcnββ)) | ||
Theorem | cncfmpt2f 24656* | Composition of continuous functions. βcnβ analogue of cnmpt12f 23391. (Contributed by Mario Carneiro, 3-Sep-2014.) |
β’ π½ = (TopOpenββfld) & β’ (π β πΉ β ((π½ Γt π½) Cn π½)) & β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄πΉπ΅)) β (πβcnββ)) | ||
Theorem | cncfmpt2ss 24657* | Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.) |
β’ π½ = (TopOpenββfld) & β’ πΉ β ((π½ Γt π½) Cn π½) & β’ (π β (π₯ β π β¦ π΄) β (πβcnβπ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnβπ)) & β’ π β β & β’ ((π΄ β π β§ π΅ β π) β (π΄πΉπ΅) β π) β β’ (π β (π₯ β π β¦ (π΄πΉπ΅)) β (πβcnβπ)) | ||
Theorem | addccncf 24658* | Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ πΉ = (π₯ β β β¦ (π₯ + π΄)) β β’ (π΄ β β β πΉ β (ββcnββ)) | ||
Theorem | idcncf 24659 | The identity function is a continuous function on β. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 24654 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
β’ πΉ = (π₯ β β β¦ π₯) β β’ πΉ β (ββcnββ) | ||
Theorem | sub1cncf 24660* | Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ πΉ = (π₯ β β β¦ (π₯ β π΄)) β β’ (π΄ β β β πΉ β (ββcnββ)) | ||
Theorem | sub2cncf 24661* | Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ πΉ = (π₯ β β β¦ (π΄ β π₯)) β β’ (π΄ β β β πΉ β (ββcnββ)) | ||
Theorem | cdivcncf 24662* | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) |
β’ πΉ = (π₯ β (β β {0}) β¦ (π΄ / π₯)) β β’ (π΄ β β β πΉ β ((β β {0})βcnββ)) | ||
Theorem | negcncf 24663* | The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ πΉ = (π₯ β π΄ β¦ -π₯) β β’ (π΄ β β β πΉ β (π΄βcnββ)) | ||
Theorem | negcncfOLD 24664* | Obsolete version of negcncf 24663 as of 9-Apr-2025. (Contributed by Mario Carneiro, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΉ = (π₯ β π΄ β¦ -π₯) β β’ (π΄ β β β πΉ β (π΄βcnββ)) | ||
Theorem | negfcncf 24665* | The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
β’ πΊ = (π₯ β π΄ β¦ -(πΉβπ₯)) β β’ (πΉ β (π΄βcnββ) β πΊ β (π΄βcnββ)) | ||
Theorem | abscncfALT 24666 | Absolute value is continuous. Alternate proof of abscncf 24642. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ abs β (ββcnββ) | ||
Theorem | cncfcnvcn 24667 | Rewrite cmphaushmeo 23525 for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π) β β’ ((πΎ β Comp β§ πΉ β (πβcnβπ)) β (πΉ:πβ1-1-ontoβπ β β‘πΉ β (πβcnβπ))) | ||
Theorem | expcncf 24668* | The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 24611. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ (π β β0 β (π₯ β β β¦ (π₯βπ)) β (ββcnββ)) | ||
Theorem | cnmptre 24669* | Lemma for iirevcn 24672 and related functions. (Contributed by Mario Carneiro, 6-Jun-2014.) |
β’ π = (TopOpenββfld) & β’ π½ = ((topGenβran (,)) βΎt π΄) & β’ πΎ = ((topGenβran (,)) βΎt π΅) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΉ β π΅) & β’ (π β (π₯ β β β¦ πΉ) β (π Cn π )) β β’ (π β (π₯ β π΄ β¦ πΉ) β (π½ Cn πΎ)) | ||
Theorem | cnmpopc 24670* | Piecewise definition of a continuous function on a real interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.) |
β’ π = (topGenβran (,)) & β’ π = (π βΎt (π΄[,]π΅)) & β’ π = (π βΎt (π΅[,]πΆ)) & β’ π = (π βΎt (π΄[,]πΆ)) & β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β (π΄[,]πΆ)) & β’ (π β π½ β (TopOnβπ)) & β’ ((π β§ (π₯ = π΅ β§ π¦ β π)) β π· = πΈ) & β’ (π β (π₯ β (π΄[,]π΅), π¦ β π β¦ π·) β ((π Γt π½) Cn πΎ)) & β’ (π β (π₯ β (π΅[,]πΆ), π¦ β π β¦ πΈ) β ((π Γt π½) Cn πΎ)) β β’ (π β (π₯ β (π΄[,]πΆ), π¦ β π β¦ if(π₯ β€ π΅, π·, πΈ)) β ((π Γt π½) Cn πΎ)) | ||
Theorem | iirev 24671 | Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β (0[,]1) β (1 β π) β (0[,]1)) | ||
Theorem | iirevcn 24672 | The reversion function is a continuous map of the unit interval. (Contributed by Mario Carneiro, 6-Jun-2014.) |
β’ (π₯ β (0[,]1) β¦ (1 β π₯)) β (II Cn II) | ||
Theorem | iihalf1 24673 | Map the first half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β (0[,](1 / 2)) β (2 Β· π) β (0[,]1)) | ||
Theorem | iihalf1cn 24674 | The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ π½ = ((topGenβran (,)) βΎt (0[,](1 / 2))) β β’ (π₯ β (0[,](1 / 2)) β¦ (2 Β· π₯)) β (π½ Cn II) | ||
Theorem | iihalf1cnOLD 24675 | Obsolete version of iihalf1cn 24674 as of 9-Apr-2025. (Contributed by Mario Carneiro, 6-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π½ = ((topGenβran (,)) βΎt (0[,](1 / 2))) β β’ (π₯ β (0[,](1 / 2)) β¦ (2 Β· π₯)) β (π½ Cn II) | ||
Theorem | iihalf2 24676 | Map the second half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β ((1 / 2)[,]1) β ((2 Β· π) β 1) β (0[,]1)) | ||
Theorem | iihalf2cn 24677 | The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ π½ = ((topGenβran (,)) βΎt ((1 / 2)[,]1)) β β’ (π₯ β ((1 / 2)[,]1) β¦ ((2 Β· π₯) β 1)) β (π½ Cn II) | ||
Theorem | iihalf2cnOLD 24678 | Obsolete version of iihalf2cn 24677 as of 9-Apr-2025. (Contributed by Mario Carneiro, 6-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π½ = ((topGenβran (,)) βΎt ((1 / 2)[,]1)) β β’ (π₯ β ((1 / 2)[,]1) β¦ ((2 Β· π₯) β 1)) β (π½ Cn II) | ||
Theorem | elii1 24679 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
β’ (π β (0[,](1 / 2)) β (π β (0[,]1) β§ π β€ (1 / 2))) | ||
Theorem | elii2 24680 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
β’ ((π β (0[,]1) β§ Β¬ π β€ (1 / 2)) β π β ((1 / 2)[,]1)) | ||
Theorem | iimulcl 24681 | The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π΄ β (0[,]1) β§ π΅ β (0[,]1)) β (π΄ Β· π΅) β (0[,]1)) | ||
Theorem | iimulcn 24682* | Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (π₯ Β· π¦)) β ((II Γt II) Cn II) | ||
Theorem | iimulcnOLD 24683* | Obsolete version of iimulcn 24682 as of 9-Apr-2025. (Contributed by Mario Carneiro, 8-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (π₯ Β· π¦)) β ((II Γt II) Cn II) | ||
Theorem | icoopnst 24684 | 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.) |
β’ π½ = (MetOpenβ((abs β β ) βΎ ((π΄[,]π΅) Γ (π΄[,]π΅)))) β β’ ((π΄ β β β§ π΅ β β) β (πΆ β (π΄(,]π΅) β (π΄[,)πΆ) β π½)) | ||
Theorem | iocopnst 24685 | 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.) |
β’ π½ = (MetOpenβ((abs β β ) βΎ ((π΄[,]π΅) Γ (π΄[,]π΅)))) β β’ ((π΄ β β β§ π΅ β β) β (πΆ β (π΄[,)π΅) β (πΆ(,]π΅) β π½)) | ||
Theorem | icchmeo 24686* | The natural bijection from [0, 1] to an arbitrary nontrivial closed interval [π΄, π΅] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ π½ = (TopOpenββfld) & β’ πΉ = (π₯ β (0[,]1) β¦ ((π₯ Β· π΅) + ((1 β π₯) Β· π΄))) β β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β πΉ β (IIHomeo(π½ βΎt (π΄[,]π΅)))) | ||
Theorem | icchmeoOLD 24687* | Obsolete version of icchmeo 24686 as of 9-Apr-2025. (Contributed by Mario Carneiro, 8-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π½ = (TopOpenββfld) & β’ πΉ = (π₯ β (0[,]1) β¦ ((π₯ Β· π΅) + ((1 β π₯) Β· π΄))) β β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β πΉ β (IIHomeo(π½ βΎt (π΄[,]π΅)))) | ||
Theorem | icopnfcnv 24688* | Define a bijection from [0, 1) to [0, +β). (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ πΉ = (π₯ β (0[,)1) β¦ (π₯ / (1 β π₯))) β β’ (πΉ:(0[,)1)β1-1-ontoβ(0[,)+β) β§ β‘πΉ = (π¦ β (0[,)+β) β¦ (π¦ / (1 + π¦)))) | ||
Theorem | icopnfhmeo 24689* | The defined bijection from [0, 1) to [0, +β) is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ πΉ = (π₯ β (0[,)1) β¦ (π₯ / (1 β π₯))) & β’ π½ = (TopOpenββfld) β β’ (πΉ Isom < , < ((0[,)1), (0[,)+β)) β§ πΉ β ((π½ βΎt (0[,)1))Homeo(π½ βΎt (0[,)+β)))) | ||
Theorem | iccpnfcnv 24690* | Define a bijection from [0, 1] to [0, +β]. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ πΉ = (π₯ β (0[,]1) β¦ if(π₯ = 1, +β, (π₯ / (1 β π₯)))) β β’ (πΉ:(0[,]1)β1-1-ontoβ(0[,]+β) β§ β‘πΉ = (π¦ β (0[,]+β) β¦ if(π¦ = +β, 1, (π¦ / (1 + π¦))))) | ||
Theorem | iccpnfhmeo 24691 | The defined bijection from [0, 1] to [0, +β] is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ πΉ = (π₯ β (0[,]1) β¦ if(π₯ = 1, +β, (π₯ / (1 β π₯)))) & β’ πΎ = ((ordTopβ β€ ) βΎt (0[,]+β)) β β’ (πΉ Isom < , < ((0[,]1), (0[,]+β)) β§ πΉ β (IIHomeoπΎ)) | ||
Theorem | xrhmeo 24692* | The bijection from [-1, 1] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ πΉ = (π₯ β (0[,]1) β¦ if(π₯ = 1, +β, (π₯ / (1 β π₯)))) & β’ πΊ = (π¦ β (-1[,]1) β¦ if(0 β€ π¦, (πΉβπ¦), -π(πΉβ-π¦))) & β’ π½ = (TopOpenββfld) β β’ (πΊ Isom < , < ((-1[,]1), β*) β§ πΊ β ((π½ βΎt (-1[,]1))Homeo(ordTopβ β€ ))) | ||
Theorem | xrhmph 24693 | The extended reals are homeomorphic to the interval [0, 1]. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ II β (ordTopβ β€ ) | ||
Theorem | xrcmp 24694 | The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo 24543), this means that β* is a compactification of β. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ (ordTopβ β€ ) β Comp | ||
Theorem | xrconn 24695 | The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ (ordTopβ β€ ) β Conn | ||
Theorem | icccvx 24696 | 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.) |
β’ ((π΄ β β β§ π΅ β β) β ((πΆ β (π΄[,]π΅) β§ π· β (π΄[,]π΅) β§ π β (0[,]1)) β (((1 β π) Β· πΆ) + (π Β· π·)) β (π΄[,]π΅))) | ||
Theorem | oprpiece1res1 24697* | 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.) |
β’ π΄ β β & β’ π΅ β β & β’ π΄ β€ π΅ & β’ π β V & β’ π β V & β’ πΎ β (π΄[,]π΅) & β’ πΉ = (π₯ β (π΄[,]π΅), π¦ β πΆ β¦ if(π₯ β€ πΎ, π , π)) & β’ πΊ = (π₯ β (π΄[,]πΎ), π¦ β πΆ β¦ π ) β β’ (πΉ βΎ ((π΄[,]πΎ) Γ πΆ)) = πΊ | ||
Theorem | oprpiece1res2 24698* | 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.) |
β’ π΄ β β & β’ π΅ β β & β’ π΄ β€ π΅ & β’ π β V & β’ π β V & β’ πΎ β (π΄[,]π΅) & β’ πΉ = (π₯ β (π΄[,]π΅), π¦ β πΆ β¦ if(π₯ β€ πΎ, π , π)) & β’ (π₯ = πΎ β π = π) & β’ (π₯ = πΎ β π = π) & β’ (π¦ β πΆ β π = π) & β’ πΊ = (π₯ β (πΎ[,]π΅), π¦ β πΆ β¦ π) β β’ (πΉ βΎ ((πΎ[,]π΅) Γ πΆ)) = πΊ | ||
Theorem | cnrehmeo 24699* | The canonical bijection from (β Γ β) to β described in cnref1o 12974 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.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ πΉ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) & β’ π½ = (topGenβran (,)) & β’ πΎ = (TopOpenββfld) β β’ πΉ β ((π½ Γt π½)HomeoπΎ) | ||
Theorem | cnrehmeoOLD 24700* | Obsolete version of cnrehmeo 24699 as of 9-Apr-2025. (Contributed by Mario Carneiro, 25-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΉ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) & β’ π½ = (topGenβran (,)) & β’ πΎ = (TopOpenββfld) β β’ πΉ β ((π½ Γt π½)HomeoπΎ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |