![]() |
Metamath
Proof Explorer Theorem List (p. 446 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | liminfvaluz2 44501* | Alternate definition of lim inf for a real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β (lim infβ(π β π β¦ π΅)) = -π(lim supβ(π β π β¦ -π΅))) | ||
Theorem | liminfvaluz3 44502* | Alternate definition of lim inf for an extended real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (lim infβπΉ) = -π(lim supβ(π β π β¦ -π(πΉβπ)))) | ||
Theorem | liminflelimsupcex 44503 | A counterexample for liminflelimsup 44482, showing that the second hypothesis is needed. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (lim supββ ) < (lim infββ ) | ||
Theorem | limsupvaluz3 44504* | Alternate definition of lim inf for an extended real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β*) β β’ (π β (lim supβ(π β π β¦ π΅)) = -π(lim infβ(π β π β¦ -ππ΅))) | ||
Theorem | liminfvaluz4 44505* | Alternate definition of lim inf for a real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (lim infβπΉ) = -π(lim supβ(π β π β¦ -(πΉβπ)))) | ||
Theorem | limsupvaluz4 44506* | Alternate definition of lim inf for a real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β (lim supβ(π β π β¦ π΅)) = -π(lim infβ(π β π β¦ -π΅))) | ||
Theorem | climliminflimsupd 44507 | If a sequence of real numbers converges, its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β dom β ) β β’ (π β (lim infβπΉ) = (lim supβπΉ)) | ||
Theorem | liminfreuzlem 44508* | Given a function on the reals, its inferior limit is real if and only if two condition holds: 1. there is a real number that is greater than or equal to the function, infinitely often; 2. there is a real number that is smaller than or equal to the function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β ((lim infβπΉ) β β β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β§ βπ₯ β β βπ β π π₯ β€ (πΉβπ)))) | ||
Theorem | liminfreuz 44509* | Given a function on the reals, its inferior limit is real if and only if two condition holds: 1. there is a real number that is greater than or equal to the function, infinitely often; 2. there is a real number that is smaller than or equal to the function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β ((lim infβπΉ) β β β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β§ βπ₯ β β βπ β π π₯ β€ (πΉβπ)))) | ||
Theorem | liminfltlem 44510* | Given a sequence of real numbers, there exists an upper part of the sequence that's approximated from above by the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim infβπΉ) β β) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)(lim infβπΉ) < ((πΉβπ) + π)) | ||
Theorem | liminflt 44511* | Given a sequence of real numbers, there exists an upper part of the sequence that's approximated from above by the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim infβπΉ) β β) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)(lim infβπΉ) < ((πΉβπ) + π)) | ||
Theorem | climliminf 44512 | A sequence of real numbers converges if and only if it converges to its inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β πΉ β (lim infβπΉ))) | ||
Theorem | liminflimsupclim 44513 | A sequence of real numbers converges if its inferior limit is real, and it is greater than or equal to the superior limit (in such a case, they are actually equal, see liminflelimsupuz 44491). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim infβπΉ) β β) & β’ (π β (lim supβπΉ) β€ (lim infβπΉ)) β β’ (π β πΉ β dom β ) | ||
Theorem | climliminflimsup 44514 | A sequence of real numbers converges if and only if its inferior limit is real and it is greater than or equal to its superior limit (in such a case, they are actually equal, see liminfgelimsupuz 44494). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim infβπΉ) β β β§ (lim supβπΉ) β€ (lim infβπΉ)))) | ||
Theorem | climliminflimsup2 44515 | A sequence of real numbers converges if and only if its superior limit is real and it is less than or equal to its inferior limit (in such a case, they are actually equal, see liminfgelimsupuz 44494). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim supβπΉ) β β β§ (lim supβπΉ) β€ (lim infβπΉ)))) | ||
Theorem | climliminflimsup3 44516 | A sequence of real numbers converges if and only if its inferior limit is real and equal to its superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim infβπΉ) β β β§ (lim infβπΉ) = (lim supβπΉ)))) | ||
Theorem | climliminflimsup4 44517 | A sequence of real numbers converges if and only if its superior limit is real and equal to its inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim supβπΉ) β β β§ (lim infβπΉ) = (lim supβπΉ)))) | ||
Theorem | limsupub2 44518* | A extended real valued function, with limsup that is not +β, is eventually less than +β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β (lim supβπΉ) β +β) β β’ (π β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < +β)) | ||
Theorem | limsupubuz2 44519* | A sequence with values in the extended reals, and with limsup that is not +β, is eventually less than +β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β (lim supβπΉ) β +β) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) < +β) | ||
Theorem | xlimpnfxnegmnf 44520* | A sequence converges to +β if and only if its negation converges to -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) | ||
Theorem | liminflbuz2 44521* | A sequence with values in the extended reals, and with liminf that is not -β, is eventually greater than -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β (lim infβπΉ) β -β) β β’ (π β βπ β π βπ β (β€β₯βπ)-β < (πΉβπ)) | ||
Theorem | liminfpnfuz 44522* | The inferior limit of a function is +β if and only if every real number is the lower bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β ((lim infβπΉ) = +β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) | ||
Theorem | liminflimsupxrre 44523* | A sequence with values in the extended reals, and with real liminf and limsup, is eventually real. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β (lim supβπΉ) β +β) & β’ (π β (lim infβπΉ) β -β) β β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) | ||
Textbooks generally use a single symbol to denote the limit of a sequence of real numbers. But then, three distinct definitions are usually given: one for the case of convergence to a real number, one for the case of limit to +β and one for the case of limit to -β. It turns out that these three definitions can be expressed as the limit w.r.t. to the standard topology on the extended reals. In this section, a relation ~~>* is defined that captures all three definitions (and can be applied to sequences of extended reals, also), see dfxlim2 44554. | ||
Syntax | clsxlim 44524 | Extend class notation with convergence relation for limits in the extended real numbers. |
class ~~>* | ||
Definition | df-xlim 44525 | Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ ~~>* = (βπ‘β(ordTopβ β€ )) | ||
Theorem | xlimrel 44526 | The limit on extended reals is a relation. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ Rel ~~>* | ||
Theorem | xlimres 44527 | A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β πΉ β (β* βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ~~>*π΄ β (πΉ βΎ (β€β₯βπ))~~>*π΄)) | ||
Theorem | xlimcl 44528 | The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (πΉ~~>*π΄ β π΄ β β*) | ||
Theorem | rexlimddv2 44529* | Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β βπ₯ β π΄ π) & β’ (((π β§ π₯ β π΄) β§ π) β π) β β’ (π β π) | ||
Theorem | xlimclim 44530 | Given a sequence of reals, it converges to a real number π΄ w.r.t. the standard topology on the reals, if and only if it converges to π΄ w.r.t. to the standard topology on the extended reals (see climreeq 44319). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimconst 44531* | A constant sequence converges to its value, w.r.t. the standard topology on the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ Fn π) & β’ (π β π΄ β β*) & β’ ((π β§ π β π) β (πΉβπ) = π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | climxlim 44532 | A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | xlimbr 44533* | Express the binary relation "sequence πΉ converges to point π " w.r.t. the standard topology on the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ π½ = (ordTopβ β€ ) β β’ (π β (πΉ~~>*π β (π β β* β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) | ||
Theorem | fuzxrpmcn 44534 | A function mapping from an upper set of integers to the extended reals is a partial map on the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β πΉ β (β* βpm β)) | ||
Theorem | cnrefiisplem 44535* | Lemma for cnrefiisp 44536 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β) & β’ (π β Β¬ π΄ β β) & β’ (π β π΅ β Fin) & β’ πΆ = (β βͺ π΅) & β’ π· = ({(absβ(ββπ΄))} βͺ βͺ π¦ β ((π΅ β© β) β {π΄}){(absβ(π¦ β π΄))}) & β’ π = inf(π·, β*, < ) β β’ (π β βπ₯ β β+ βπ¦ β πΆ ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) | ||
Theorem | cnrefiisp 44536* | A non-real, complex number is an isolated point w.r.t. the union of the reals with any finite set (the extended reals is an example of such a union). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β) & β’ (π β Β¬ π΄ β β) & β’ (π β π΅ β Fin) & β’ πΆ = (β βͺ π΅) β β’ (π β βπ₯ β β+ βπ¦ β πΆ ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) | ||
Theorem | xlimxrre 44537* | If a sequence ranging over the extended reals converges w.r.t. the standard topology on the complex numbers, then there exists an upper set of the integers over which the function is real-valued (the weaker hypothesis πΉ β dom β is probably not enough, since in principle we could have +β β β and -β β β). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β π΄ β β) & β’ (π β πΉ~~>*π΄) β β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) | ||
Theorem | xlimmnfvlem1 44538* | Lemma for xlimmnfv 44540: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*-β) & β’ (π β π β β) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π) | ||
Theorem | xlimmnfvlem2 44539* | Lemma for xlimmnf 44547: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) < π₯) β β’ (π β πΉ~~>*-β) | ||
Theorem | xlimmnfv 44540* | A function converges to minus infinity if it eventually becomes (and stays) smaller than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) | ||
Theorem | xlimconst2 44541* | A sequence that eventually becomes constant, converges to its constant value (w.r.t. the standard topology on the extended reals). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β π β π) & β’ (π β π΄ β β*) & β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | xlimpnfvlem1 44542* | Lemma for xlimpnfv 44544: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*+β) & β’ (π β π β β) β β’ (π β βπ β π βπ β (β€β₯βπ)π β€ (πΉβπ)) | ||
Theorem | xlimpnfvlem2 44543* | Lemma for xlimpnfv 44544: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ < (πΉβπ)) β β’ (π β πΉ~~>*+β) | ||
Theorem | xlimpnfv 44544* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) | ||
Theorem | xlimclim2lem 44545* | Lemma for xlimclim2 44546. Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β π΄ β β) & β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimclim2 44546 | Given a sequence of extended reals, it converges to a real number π΄ w.r.t. the standard topology on the reals (see climreeq 44319), if and only if it converges to π΄ w.r.t. to the standard topology on the extended reals. In order for the first part of the statement to even make sense, the sequence will of course eventually become (and stay) real: showing this, is the key step of the proof. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β π΄ β β) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimmnf 44547* | A function converges to minus infinity if it eventually becomes (and stays) smaller than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) | ||
Theorem | xlimpnf 44548* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) | ||
Theorem | xlimmnfmpt 44549* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β*) & β’ πΉ = (π β π β¦ π΅) β β’ (π β (πΉ~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π΅ β€ π₯)) | ||
Theorem | xlimpnfmpt 44550* | A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β*) & β’ πΉ = (π β π β¦ π΅) β β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅)) | ||
Theorem | climxlim2lem 44551 | In this lemma for climxlim2 44552 there is the additional assumption that the converging function is complex-valued on the whole domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | climxlim2 44552 | A sequence of extended reals, converging w.r.t. the standard topology on the complex numbers is a converging sequence w.r.t. the standard topology on the extended reals. This is non-trivial, because +β and -β could, in principle, be complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ β π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | dfxlim2v 44553* | An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*π΄ β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))))) | ||
Theorem | dfxlim2 44554* | An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*π΄ β (πΉ β π΄ β¨ (π΄ = -β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β¨ (π΄ = +β β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))))) | ||
Theorem | climresd 44555 | A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ (π β πΉ β π) β β’ (π β ((πΉ βΎ (β€β₯βπ)) β π΄ β πΉ β π΄)) | ||
Theorem | climresdm 44556 | A real function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ (π β πΉ β π) β β’ (π β (πΉ β dom β β (πΉ βΎ (β€β₯βπ)) β dom β )) | ||
Theorem | dmclimxlim 44557 | A real valued sequence that converges w.r.t. the topology on the complex numbers, converges w.r.t. the topology on the extended reals (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β dom β ) β β’ (π β πΉ β dom ~~>*) | ||
Theorem | xlimmnflimsup2 44558 | A sequence of extended reals converges to -β if and only if its superior limit is also -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*-β β (lim supβπΉ) = -β)) | ||
Theorem | xlimuni 44559 | An infinite sequence converges to at most one limit (w.r.t. to the standard topology on the extended reals). (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β πΉ~~>*π΄) & β’ (π β πΉ~~>*π΅) β β’ (π β π΄ = π΅) | ||
Theorem | xlimclimdm 44560 | A sequence of extended reals that converges to a real w.r.t. the standard topology on the extended reals, also converges w.r.t. to the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*π΄) & β’ (π β π΄ β β) β β’ (π β πΉ β dom β ) | ||
Theorem | xlimfun 44561 | The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ Fun ~~>* | ||
Theorem | xlimmnflimsup 44562 | If a sequence of extended reals converges to -β then its superior limit is also -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*-β) β β’ (π β (lim supβπΉ) = -β) | ||
Theorem | xlimdm 44563 | Two ways to express that a function has a limit. (The expression (~~>*βπΉ) is sometimes useful as a shorthand for "the unique limit of the function πΉ"). (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (πΉ β dom ~~>* β πΉ~~>*(~~>*βπΉ)) | ||
Theorem | xlimpnfxnegmnf2 44564* | A sequence converges to +β if and only if its negation converges to -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β (π β π β¦ -π(πΉβπ))~~>*-β)) | ||
Theorem | xlimresdm 44565 | A function converges in the extended reals iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β πΉ β (β* βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ β dom ~~>* β (πΉ βΎ (β€β₯βπ)) β dom ~~>*)) | ||
Theorem | xlimpnfliminf 44566 | If a sequence of extended reals converges to +β then its superior limit is also +β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*+β) β β’ (π β (lim infβπΉ) = +β) | ||
Theorem | xlimpnfliminf2 44567 | A sequence of extended reals converges to +β if and only if its superior limit is also +β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β (lim infβπΉ) = +β)) | ||
Theorem | xlimliminflimsup 44568 | A sequence of extended reals converges if and only if its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ β dom ~~>* β (lim infβπΉ) = (lim supβπΉ))) | ||
Theorem | xlimlimsupleliminf 44569 | A sequence of extended reals converges if and only if its superior limit is smaller than or equal to its inferior limit. (Contributed by Glauco Siliprandi, 2-Dec-2023.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ β dom ~~>* β (lim supβπΉ) β€ (lim infβπΉ))) | ||
Theorem | coseq0 44570 | A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β ((cosβπ΄) = 0 β ((π΄ / Ο) + (1 / 2)) β β€)) | ||
Theorem | sinmulcos 44571 | Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) Β· (cosβπ΅)) = (((sinβ(π΄ + π΅)) + (sinβ(π΄ β π΅))) / 2)) | ||
Theorem | coskpi2 44572 | The cosine of an integer multiple of negative Ο is either 1 or negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (πΎ β β€ β (cosβ(πΎ Β· Ο)) = if(2 β₯ πΎ, 1, -1)) | ||
Theorem | cosnegpi 44573 | The cosine of negative Ο is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (cosβ-Ο) = -1 | ||
Theorem | sinaover2ne0 44574 | If π΄ in (0, 2Ο) then sin(π΄ / 2) is not 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β (0(,)(2 Β· Ο)) β (sinβ(π΄ / 2)) β 0) | ||
Theorem | cosknegpi 44575 | The cosine of an integer multiple of negative Ο is either 1 or negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (πΎ β β€ β (cosβ(πΎ Β· -Ο)) = if(2 β₯ πΎ, 1, -1)) | ||
Theorem | mulcncff 44576 | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf Β· πΊ) β (πβcnββ)) | ||
Theorem | cncfmptssg 44577* | A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss 44293 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ πΈ) & β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΆ β π΄) & β’ (π β π· β π΅) & β’ ((π β§ π₯ β πΆ) β πΈ β π·) β β’ (π β (π₯ β πΆ β¦ πΈ) β (πΆβcnβπ·)) | ||
Theorem | constcncfg 44578* | A constant function is a continuous function on β. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β β) β β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnβπΆ)) | ||
Theorem | idcncfg 44579* | The identity function is a continuous function on β. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β π΅) & β’ (π β π΅ β β) β β’ (π β (π₯ β π΄ β¦ π₯) β (π΄βcnβπ΅)) | ||
Theorem | cncfshift 44580* | A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π β β) & β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} & β’ (π β πΉ β (π΄βcnββ)) & β’ πΊ = (π₯ β π΅ β¦ (πΉβ(π₯ β π))) β β’ (π β πΊ β (π΅βcnββ)) | ||
Theorem | resincncf 44581 | sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (sin βΎ β) β (ββcnββ) | ||
Theorem | addccncf2 44582* | Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ (π΅ + π₯)) β β’ ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnββ)) | ||
Theorem | 0cnf 44583 | The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β ({β } Cn {β }) | ||
Theorem | fsumcncf 44584* | The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (πβcnββ)) | ||
Theorem | cncfperiod 44585* | A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π β β) & β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} & β’ (π β πΉ:dom πΉβΆβ) & β’ (π β π΅ β dom πΉ) & β’ ((π β§ π₯ β π΄) β (πΉβ(π₯ + π)) = (πΉβπ₯)) & β’ (π β (πΉ βΎ π΄) β (π΄βcnββ)) β β’ (π β (πΉ βΎ π΅) β (π΅βcnββ)) | ||
Theorem | subcncff 44586 | The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf β πΊ) β (πβcnββ)) | ||
Theorem | negcncfg 44587* | The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnββ)) β β’ (π β (π₯ β π΄ β¦ -π΅) β (π΄βcnββ)) | ||
Theorem | cnfdmsn 44588* | A function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β π β§ π΅ β π) β (π₯ β {π΄} β¦ π΅) β (π« {π΄} Cn π« {π΅})) | ||
Theorem | cncfcompt 44589* | Composition of continuous functions. A generalization of cncfmpt1f 24429 to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnβπΆ)) & β’ (π β πΉ β (πΆβcnβπ·)) β β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β (π΄βcnβπ·)) | ||
Theorem | addcncff 44590 | The sum of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf + πΊ) β (πβcnββ)) | ||
Theorem | ioccncflimc 44591 | Limit at the upper bound of a continuous function defined on a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,]π΅)βcnββ)) β β’ (π β (πΉβπ΅) β ((πΉ βΎ (π΄(,)π΅)) limβ π΅)) | ||
Theorem | cncfuni 44592* | A complex function on a subset of the complex numbers is continuous if its domain is the union of relatively open subsets over which the function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β βͺ π΅) & β’ ((π β§ π β π΅) β (π΄ β© π) β ((TopOpenββfld) βΎt π΄)) & β’ ((π β§ π β π΅) β (πΉ βΎ π) β ((π΄ β© π)βcnββ)) β β’ (π β πΉ β (π΄βcnββ)) | ||
Theorem | icccncfext 44593* | A continuous function on a closed interval can be extended to a continuous function on the whole real line. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯πΉ & β’ π½ = (topGenβran (,)) & β’ π = βͺ πΎ & β’ πΊ = (π₯ β β β¦ if(π₯ β (π΄[,]π΅), (πΉβπ₯), if(π₯ < π΄, (πΉβπ΄), (πΉβπ΅)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΎ β Top) & β’ (π β πΉ β ((π½ βΎt (π΄[,]π΅)) Cn πΎ)) β β’ (π β (πΊ β (π½ Cn (πΎ βΎt ran πΉ)) β§ (πΊ βΎ (π΄[,]π΅)) = πΉ)) | ||
Theorem | cncficcgt0 44594* | A the absolute value of a continuous function on a closed interval, that is never 0, has a strictly positive lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β (π΄[,]π΅) β¦ πΆ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnβ(β β {0}))) β β’ (π β βπ¦ β β+ βπ₯ β (π΄[,]π΅)π¦ β€ (absβπΆ)) | ||
Theorem | icocncflimc 44595 | Limit at the lower bound, of a continuous function defined on a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄[,)π΅)βcnββ)) β β’ (π β (πΉβπ΄) β ((πΉ βΎ (π΄(,)π΅)) limβ π΄)) | ||
Theorem | cncfdmsn 44596* | A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β {π΄} β¦ π΅) β ({π΄}βcnβ{π΅})) | ||
Theorem | divcncff 44597 | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnβ(β β {0}))) β β’ (π β (πΉ βf / πΊ) β (πβcnββ)) | ||
Theorem | cncfshiftioo 44598* | A periodic continuous function stays continuous if the domain is an open interval that is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ πΆ = (π΄(,)π΅) & β’ (π β π β β) & β’ π· = ((π΄ + π)(,)(π΅ + π)) & β’ (π β πΉ β (πΆβcnββ)) & β’ πΊ = (π₯ β π· β¦ (πΉβ(π₯ β π))) β β’ (π β πΊ β (π·βcnββ)) | ||
Theorem | cncfiooicclem1 44599* | A continuous function πΉ on an open interval (π΄(,)π΅) can be extended to a continuous function πΊ on the corresponding closed interval, if it has a finite right limit π in π΄ and a finite left limit πΏ in π΅. πΉ can be complex-valued. This lemma assumes π΄ < π΅, the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) | ||
Theorem | cncfiooicc 44600* | A continuous function πΉ on an open interval (π΄(,)π΅) can be extended to a continuous function πΊ on the corresponding closed interval, if it has a finite right limit π in π΄ and a finite left limit πΏ in π΅. πΉ can be complex-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |