Home | Metamath
Proof Explorer Theorem List (p. 439 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | liminflimsupclim 43801 | 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 43779). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim infβπΉ) β β) & β’ (π β (lim supβπΉ) β€ (lim infβπΉ)) β β’ (π β πΉ β dom β ) | ||
Theorem | climliminflimsup 43802 | 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 43782). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim infβπΉ) β β β§ (lim supβπΉ) β€ (lim infβπΉ)))) | ||
Theorem | climliminflimsup2 43803 | 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 43782). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim supβπΉ) β β β§ (lim supβπΉ) β€ (lim infβπΉ)))) | ||
Theorem | climliminflimsup3 43804 | 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 43805 | 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 43806* | 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 43807* | 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 43808* | A sequence converges to +β if and only if its negation converges to -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) | ||
Theorem | liminflbuz2 43809* | 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 43810* | 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 43811* | 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 43842. | ||
Syntax | clsxlim 43812 | Extend class notation with convergence relation for limits in the extended real numbers. |
class ~~>* | ||
Definition | df-xlim 43813 | Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ ~~>* = (βπ‘β(ordTopβ β€ )) | ||
Theorem | xlimrel 43814 | The limit on extended reals is a relation. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ Rel ~~>* | ||
Theorem | xlimres 43815 | A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β πΉ β (β* βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ~~>*π΄ β (πΉ βΎ (β€β₯βπ))~~>*π΄)) | ||
Theorem | xlimcl 43816 | The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (πΉ~~>*π΄ β π΄ β β*) | ||
Theorem | rexlimddv2 43817* | Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β βπ₯ β π΄ π) & β’ (((π β§ π₯ β π΄) β§ π) β π) β β’ (π β π) | ||
Theorem | xlimclim 43818 | 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 43607). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimconst 43819* | 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 43820 | A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | xlimbr 43821* | 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 43822 | 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 43823* | Lemma for cnrefiisp 43824 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β) & β’ (π β Β¬ π΄ β β) & β’ (π β π΅ β Fin) & β’ πΆ = (β βͺ π΅) & β’ π· = ({(absβ(ββπ΄))} βͺ βͺ π¦ β ((π΅ β© β) β {π΄}){(absβ(π¦ β π΄))}) & β’ π = inf(π·, β*, < ) β β’ (π β βπ₯ β β+ βπ¦ β πΆ ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) | ||
Theorem | cnrefiisp 43824* | 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 43825* | 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 43826* | Lemma for xlimmnfv 43828: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*-β) & β’ (π β π β β) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π) | ||
Theorem | xlimmnfvlem2 43827* | Lemma for xlimmnf 43835: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) < π₯) β β’ (π β πΉ~~>*-β) | ||
Theorem | xlimmnfv 43828* | 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 43829* | 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 43830* | Lemma for xlimpnfv 43832: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*+β) & β’ (π β π β β) β β’ (π β βπ β π βπ β (β€β₯βπ)π β€ (πΉβπ)) | ||
Theorem | xlimpnfvlem2 43831* | Lemma for xlimpnfv 43832: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ < (πΉβπ)) β β’ (π β πΉ~~>*+β) | ||
Theorem | xlimpnfv 43832* | 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 43833* | Lemma for xlimclim2 43834. Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β π΄ β β) & β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimclim2 43834 | Given a sequence of extended reals, it converges to a real number π΄ w.r.t. the standard topology on the reals (see climreeq 43607), 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 43835* | 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 43836* | 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 43837* | 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 43838* | 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 43839 | In this lemma for climxlim2 43840 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 43840 | 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 43841* | 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 43842* | 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 43843 | A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ (π β πΉ β π) β β’ (π β ((πΉ βΎ (β€β₯βπ)) β π΄ β πΉ β π΄)) | ||
Theorem | climresdm 43844 | A real function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ (π β πΉ β π) β β’ (π β (πΉ β dom β β (πΉ βΎ (β€β₯βπ)) β dom β )) | ||
Theorem | dmclimxlim 43845 | 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 43846 | 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 43847 | 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 43848 | 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 43849 | The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ Fun ~~>* | ||
Theorem | xlimmnflimsup 43850 | 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 43851 | 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 43852* | A sequence converges to +β if and only if its negation converges to -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (πΉ~~>*+β β (π β π β¦ -π(πΉβπ))~~>*-β)) | ||
Theorem | xlimresdm 43853 | 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 43854 | 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 43855 | 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 43856 | 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 43857 | 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 43858 | A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β ((cosβπ΄) = 0 β ((π΄ / Ο) + (1 / 2)) β β€)) | ||
Theorem | sinmulcos 43859 | Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) Β· (cosβπ΅)) = (((sinβ(π΄ + π΅)) + (sinβ(π΄ β π΅))) / 2)) | ||
Theorem | coskpi2 43860 | 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 43861 | The cosine of negative Ο is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (cosβ-Ο) = -1 | ||
Theorem | sinaover2ne0 43862 | If π΄ in (0, 2Ο) then sin(π΄ / 2) is not 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β (0(,)(2 Β· Ο)) β (sinβ(π΄ / 2)) β 0) | ||
Theorem | cosknegpi 43863 | 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 43864 | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf Β· πΊ) β (πβcnββ)) | ||
Theorem | cncfmptssg 43865* | A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss 43581 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ πΈ) & β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΆ β π΄) & β’ (π β π· β π΅) & β’ ((π β§ π₯ β πΆ) β πΈ β π·) β β’ (π β (π₯ β πΆ β¦ πΈ) β (πΆβcnβπ·)) | ||
Theorem | constcncfg 43866* | A constant function is a continuous function on β. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β β) β β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnβπΆ)) | ||
Theorem | idcncfg 43867* | The identity function is a continuous function on β. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β π΅) & β’ (π β π΅ β β) β β’ (π β (π₯ β π΄ β¦ π₯) β (π΄βcnβπ΅)) | ||
Theorem | cncfshift 43868* | A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π β β) & β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} & β’ (π β πΉ β (π΄βcnββ)) & β’ πΊ = (π₯ β π΅ β¦ (πΉβ(π₯ β π))) β β’ (π β πΊ β (π΅βcnββ)) | ||
Theorem | resincncf 43869 | sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (sin βΎ β) β (ββcnββ) | ||
Theorem | addccncf2 43870* | Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ (π΅ + π₯)) β β’ ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnββ)) | ||
Theorem | 0cnf 43871 | The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β ({β } Cn {β }) | ||
Theorem | fsumcncf 43872* | The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (πβcnββ)) | ||
Theorem | cncfperiod 43873* | 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 43874 | The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf β πΊ) β (πβcnββ)) | ||
Theorem | negcncfg 43875* | The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnββ)) β β’ (π β (π₯ β π΄ β¦ -π΅) β (π΄βcnββ)) | ||
Theorem | cnfdmsn 43876* | A function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β π β§ π΅ β π) β (π₯ β {π΄} β¦ π΅) β (π« {π΄} Cn π« {π΅})) | ||
Theorem | cncfcompt 43877* | Composition of continuous functions. A generalization of cncfmpt1f 24199 to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π΄ β¦ π΅) β (π΄βcnβπΆ)) & β’ (π β πΉ β (πΆβcnβπ·)) β β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β (π΄βcnβπ·)) | ||
Theorem | addcncff 43878 | The sum of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnββ)) β β’ (π β (πΉ βf + πΊ) β (πβcnββ)) | ||
Theorem | ioccncflimc 43879 | 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 43880* | 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 43881* | 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 43882* | 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 43883 | 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 43884* | A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β {π΄} β¦ π΅) β ({π΄}βcnβ{π΅})) | ||
Theorem | divcncff 43885 | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ β (πβcnββ)) & β’ (π β πΊ β (πβcnβ(β β {0}))) β β’ (π β (πΉ βf / πΊ) β (πβcnββ)) | ||
Theorem | cncfshiftioo 43886* | 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 43887* | 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 43888* | 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ββ)) | ||
Theorem | cncfiooiccre 43889* | 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 π΅. πΉ is assumed to be real-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) | ||
Theorem | cncfioobdlem 43890* | πΊ actually extends πΉ. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄(,)π΅)βΆπ) & β’ πΊ = (π₯ β (π΄[,]π΅) β¦ if(π₯ = π΄, π , if(π₯ = π΅, πΏ, (πΉβπ₯)))) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β (πΊβπΆ) = (πΉβπΆ)) | ||
Theorem | cncfioobd 43891* | A continuous function πΉ on an open interval (π΄(,)π΅) with a finite right limit π in π΄ and a finite left limit πΏ in π΅ is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΏ β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΄)) β β’ (π β βπ₯ β β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ π₯) | ||
Theorem | jumpncnp 43892 | Jump discontinuity or discontinuity of the first kind: if the left and the right limit don't match, the function is discontinuous at the point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (TopOpenββfld) & β’ (π β π΄ β β) & β’ π½ = (topGenβran (,)) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β) & β’ (π β π΅ β ((limPtβπ½)β(π΄ β© (-β(,)π΅)))) & β’ (π β π΅ β ((limPtβπ½)β(π΄ β© (π΅(,)+β)))) & β’ (π β πΏ β ((πΉ βΎ (-β(,)π΅)) limβ π΅)) & β’ (π β π β ((πΉ βΎ (π΅(,)+β)) limβ π΅)) & β’ (π β πΏ β π ) β β’ (π β Β¬ πΉ β ((π½ CnP (TopOpenββfld))βπ΅)) | ||
Theorem | cxpcncf2 43893* | The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π΄ β (β β (-β(,]0)) β (π₯ β β β¦ (π΄βππ₯)) β (ββcnββ)) | ||
Theorem | fprodcncf 43894* | The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β β) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ πΆ) β (π΄βcnββ)) β β’ (π β (π₯ β π΄ β¦ βπ β π΅ πΆ) β (π΄βcnββ)) | ||
Theorem | add1cncf 43895* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ + π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | add2cncf 43896* | Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ + π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub1cncfd 43897* | Subtracting a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π₯ β π΄)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | sub2cncfd 43898* | Subtraction from a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β β β¦ (π΄ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodsub2cncf 43899* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ β π₯)) β β’ (π β πΉ β (ββcnββ)) | ||
Theorem | fprodadd2cncf 43900* | πΉ is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ = (π₯ β β β¦ βπ β π΄ (π΅ + π₯)) β β’ (π β πΉ β (ββcnββ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |