Home | Metamath
Proof Explorer Theorem List (p. 438 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | limsupvaluz2 43701* | The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim supβπΉ) β β) β β’ (π β (lim supβπΉ) = inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )), β, < )) | ||
Theorem | limsupreuzmpt 43702* | Given a function on the reals, defined on a set of upper integers, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, infinitely often; 2. there is a real number that is greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β ((lim supβ(π β π β¦ π΅)) β β β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ π΅ β§ βπ₯ β β βπ β π π΅ β€ π₯))) | ||
Theorem | supcnvlimsup 43703* | If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim supβπΉ) β β) β β’ (π β (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )) β (lim supβπΉ)) | ||
Theorem | supcnvlimsupmpt 43704* | If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β) & β’ (π β (lim supβ(π β π β¦ π΅)) β β) β β’ (π β (π β π β¦ sup(ran (π β (β€β₯βπ) β¦ π΅), β*, < )) β (lim supβ(π β π β¦ π΅))) | ||
Theorem | 0cnv 43705 | If β is a complex number, then it converges to itself. See 0ncn 11003 and its comment; see also the comment in climlimsupcex 43732. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (β β β β β β β ) | ||
Theorem | climuzlem 43706* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) | ||
Theorem | climuz 43707* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) | ||
Theorem | lmbr3v 43708* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π½ β (TopOnβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) | ||
Theorem | climisp 43709* | If a sequence converges to an isolated point (w.r.t. the standard topology on the complex numbers) then the sequence eventually becomes that point. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) & β’ (π β π β β+) & β’ ((π β§ π β π β§ (πΉβπ) β π΄) β π β€ (absβ((πΉβπ) β π΄))) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) = π΄) | ||
Theorem | lmbr3 43710* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππΉ & β’ (π β π½ β (TopOnβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) | ||
Theorem | climrescn 43711* | A sequence converging w.r.t. the standard topology on the complex numbers, eventually becomes a sequence of complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ Fn π) & β’ (π β πΉ β dom β ) β β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) | ||
Theorem | climxrrelem 43712* | 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. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ β π΄) & β’ (π β π· β β+) & β’ ((π β§ +β β β) β π· β€ (absβ(+β β π΄))) & β’ ((π β§ -β β β) β π· β€ (absβ(-β β π΄))) β β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) | ||
Theorem | climxrre 43713* | 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.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β π΄ β β) & β’ (π β πΉ β π΄) β β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) | ||
Syntax | clsi 43714 | Extend class notation to include the liminf function. (actually, it makes sense for any extended real function defined on a subset of RR which is not upper-bounded) |
class lim inf | ||
Definition | df-liminf 43715* | Define the inferior limit of a sequence of extended real numbers. (Contributed by GS, 2-Jan-2022.) |
β’ lim inf = (π₯ β V β¦ sup(ran (π β β β¦ inf(((π₯ β (π[,)+β)) β© β*), β*, < )), β*, < )) | ||
Theorem | limsuplt2 43716* | The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) β β’ (π β ((lim supβπΉ) < π΄ β βπ β β sup(((πΉ β (π[,)+β)) β© β*), β*, < ) < π΄)) | ||
Theorem | liminfgord 43717 | Ordering property of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β inf(((πΉ β (π΄[,)+β)) β© β*), β*, < ) β€ inf(((πΉ β (π΅[,)+β)) β© β*), β*, < )) | ||
Theorem | limsupvald 43718* | The superior limit of a sequence πΉ of extended real numbers is the infimum of the set of suprema of all restrictions of πΉ to an upperset of reals . (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β (lim supβπΉ) = inf(ran πΊ, β*, < )) | ||
Theorem | limsupresicompt 43719* | The superior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β π) & β’ (π β π β β) & β’ π = (π[,)+β) β β’ (π β (lim supβ(π₯ β π΄ β¦ π΅)) = (lim supβ(π₯ β (π΄ β© π) β¦ π΅))) | ||
Theorem | limsupcli 43720 | Closure of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ β π β β’ (lim supβπΉ) β β* | ||
Theorem | liminfgf 43721 | Closure of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ πΊ:ββΆβ* | ||
Theorem | liminfval 43722* | The inferior limit of a set πΉ. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (πΉ β π β (lim infβπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | climlimsup 43723 | A sequence of real numbers converges if and only if it converges to its superior limit. The first hypothesis is needed (see climlimsupcex 43732 for a counterexample). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β πΉ β (lim supβπΉ))) | ||
Theorem | limsupge 43724* | The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) β β’ (π β (π΄ β€ (lim supβπΉ) β βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*), β*, < ))) | ||
Theorem | liminfgval 43725* | Value of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β β β (πΊβπ) = inf(((πΉ β (π[,)+β)) β© β*), β*, < )) | ||
Theorem | liminfcl 43726 | Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (πΉ β π β (lim infβπΉ) β β*) | ||
Theorem | liminfvald 43727* | The inferior limit of a set πΉ. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β (lim infβπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | liminfval5 43728* | The inferior limit of an infinite sequence πΉ of extended real numbers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆβ*) & β’ πΊ = (π β β β¦ inf((πΉ β (π[,)+β)), β*, < )) β β’ (π β (lim infβπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | limsupresxr 43729 | The superior limit of a function only depends on the restriction of that function to the preimage of the set of extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ (π β Fun πΉ) & β’ π΄ = (β‘πΉ β β*) β β’ (π β (lim supβ(πΉ βΎ π΄)) = (lim supβπΉ)) | ||
Theorem | liminfresxr 43730 | The inferior limit of a function only depends on the preimage of the extended real part. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ (π β Fun πΉ) & β’ π΄ = (β‘πΉ β β*) β β’ (π β (lim infβ(πΉ βΎ π΄)) = (lim infβπΉ)) | ||
Theorem | liminfval2 43731* | The superior limit, relativized to an unbounded set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) & β’ (π β πΉ β π) & β’ (π β π΄ β β) & β’ (π β sup(π΄, β*, < ) = +β) β β’ (π β (lim infβπΉ) = sup((πΊ β π΄), β*, < )) | ||
Theorem | climlimsupcex 43732 | Counterexample for climlimsup 43723, showing that the first hypothesis is needed, if the empty set is a complex number (see 0ncn 11003 and its comment). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ Β¬ π β β€ & β’ π = (β€β₯βπ) & β’ πΉ = β β β’ ((β β β β§ Β¬ -β β β) β (πΉ:πβΆβ β§ πΉ β dom β β§ Β¬ πΉ β (lim supβπΉ))) | ||
Theorem | liminfcld 43733 | Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) β β’ (π β (lim infβπΉ) β β*) | ||
Theorem | liminfresico 43734 | The inferior limit doesn't change when a function is restricted to an upperset of reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β) & β’ π = (π[,)+β) & β’ (π β πΉ β π) β β’ (π β (lim infβ(πΉ βΎ π)) = (lim infβπΉ)) | ||
Theorem | limsup10exlem 43735* | The range of the given function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ = (π β β β¦ if(2 β₯ π, 0, 1)) & β’ (π β πΎ β β) β β’ (π β (πΉ β (πΎ[,)+β)) = {0, 1}) | ||
Theorem | limsup10ex 43736 | The superior limit of a function that alternates between two values. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ = (π β β β¦ if(2 β₯ π, 0, 1)) β β’ (lim supβπΉ) = 1 | ||
Theorem | liminf10ex 43737 | The inferior limit of a function that alternates between two values. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ = (π β β β¦ if(2 β₯ π, 0, 1)) β β’ (lim infβπΉ) = 0 | ||
Theorem | liminflelimsuplem 43738* | The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ (π β βπ β β βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β β ) β β’ (π β (lim infβπΉ) β€ (lim supβπΉ)) | ||
Theorem | liminflelimsup 43739* | The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex 43760 for a counterexample). The inequality can be strict, see liminfltlimsupex 43744. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ (π β βπ β β βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β β ) β β’ (π β (lim infβπΉ) β€ (lim supβπΉ)) | ||
Theorem | limsupgtlem 43740* | For any positive real, the superior limit of F is larger than any of its values at large enough arguments, up to that positive real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim supβπΉ) β β) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ) β π) < (lim supβπΉ)) | ||
Theorem | limsupgt 43741* | Given a sequence of real numbers, there exists an upper part of the sequence that's appxoximated from below by the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim supβπΉ) β β) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ) β π) < (lim supβπΉ)) | ||
Theorem | liminfresre 43742 | The inferior limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) β β’ (π β (lim infβ(πΉ βΎ β)) = (lim infβπΉ)) | ||
Theorem | liminfresicompt 43743* | The inferior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β) & β’ π = (π[,)+β) & β’ (π β π΄ β π) β β’ (π β (lim infβ(π₯ β (π΄ β© π) β¦ π΅)) = (lim infβ(π₯ β π΄ β¦ π΅))) | ||
Theorem | liminfltlimsupex 43744 | An example where the lim inf is strictly smaller than the lim sup. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ = (π β β β¦ if(2 β₯ π, 0, 1)) β β’ (lim infβπΉ) < (lim supβπΉ) | ||
Theorem | liminfgelimsup 43745* | The inferior limit is greater than or equal to the superior limit if and only if they are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ (π β βπ β β βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β β ) β β’ (π β ((lim supβπΉ) β€ (lim infβπΉ) β (lim infβπΉ) = (lim supβπΉ))) | ||
Theorem | liminfvalxr 43746* | Alternate definition of lim inf when πΉ is an extended real-valued function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯πΉ & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆβ*) β β’ (π β (lim infβπΉ) = -π(lim supβ(π₯ β π΄ β¦ -π(πΉβπ₯)))) | ||
Theorem | liminfresuz 43747 | If the real part of the domain of a function is a subset of the integers, the inferior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ β π) & β’ (π β dom (πΉ βΎ β) β β€) β β’ (π β (lim infβ(πΉ βΎ π)) = (lim infβπΉ)) | ||
Theorem | liminflelimsupuz 43748 | The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (lim infβπΉ) β€ (lim supβπΉ)) | ||
Theorem | liminfvalxrmpt 43749* | Alternate definition of lim inf when πΉ is an extended real-valued function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β β*) β β’ (π β (lim infβ(π₯ β π΄ β¦ π΅)) = -π(lim supβ(π₯ β π΄ β¦ -ππ΅))) | ||
Theorem | liminfresuz2 43750 | If the domain of a function is a subset of the integers, the inferior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ β π) & β’ (π β dom πΉ β β€) β β’ (π β (lim infβ(πΉ βΎ π)) = (lim infβπΉ)) | ||
Theorem | liminfgelimsupuz 43751 | The inferior limit is greater than or equal to the superior limit if and only if they are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β ((lim supβπΉ) β€ (lim infβπΉ) β (lim infβπΉ) = (lim supβπΉ))) | ||
Theorem | liminfval4 43752* | Alternate definition of lim inf when the given function is eventually real-valued. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π β β) & β’ ((π β§ π₯ β (π΄ β© (π[,)+β))) β π΅ β β) β β’ (π β (lim infβ(π₯ β π΄ β¦ π΅)) = -π(lim supβ(π₯ β π΄ β¦ -π΅))) | ||
Theorem | liminfval3 43753* | Alternate definition of lim inf when the given function is eventually extended real-valued. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π β β) & β’ ((π β§ π₯ β (π΄ β© (π[,)+β))) β π΅ β β*) β β’ (π β (lim infβ(π₯ β π΄ β¦ π΅)) = -π(lim supβ(π₯ β π΄ β¦ -ππ΅))) | ||
Theorem | liminfequzmpt2 43754* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππ & β’ β²ππ΄ & β’ β²ππ΅ & β’ π΄ = (β€β₯βπ) & β’ π΅ = (β€β₯βπ) & β’ (π β πΎ β π΄) & β’ (π β πΎ β π΅) & β’ ((π β§ π β (β€β₯βπΎ)) β πΆ β π) β β’ (π β (lim infβ(π β π΄ β¦ πΆ)) = (lim infβ(π β π΅ β¦ πΆ))) | ||
Theorem | liminfvaluz 43755* | 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 | liminf0 43756 | The inferior limit of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (lim infββ ) = +β | ||
Theorem | limsupval4 43757* | Alternate definition of lim inf when the given a function is eventually extended real-valued. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π β β) & β’ ((π β§ π₯ β (π΄ β© (π[,)+β))) β π΅ β β*) β β’ (π β (lim supβ(π₯ β π΄ β¦ π΅)) = -π(lim infβ(π₯ β π΄ β¦ -ππ΅))) | ||
Theorem | liminfvaluz2 43758* | 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 43759* | 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 43760 | A counterexample for liminflelimsup 43739, showing that the second hypothesis is needed. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (lim supββ ) < (lim infββ ) | ||
Theorem | limsupvaluz3 43761* | 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 43762* | 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 43763* | 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 43764 | 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 43765* | 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 43766* | 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 43767* | 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 43768* | 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 43769 | 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 43770 | 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 43748). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim infβπΉ) β β) & β’ (π β (lim supβπΉ) β€ (lim infβπΉ)) β β’ (π β πΉ β dom β ) | ||
Theorem | climliminflimsup 43771 | 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 43751). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim infβπΉ) β β β§ (lim supβπΉ) β€ (lim infβπΉ)))) | ||
Theorem | climliminflimsup2 43772 | 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 43751). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim supβπΉ) β β β§ (lim supβπΉ) β€ (lim infβπΉ)))) | ||
Theorem | climliminflimsup3 43773 | 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 43774 | 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 43775* | 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 43776* | 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 43777* | A sequence converges to +β if and only if its negation converges to -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) | ||
Theorem | liminflbuz2 43778* | 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 43779* | 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 43780* | 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 43811. | ||
Syntax | clsxlim 43781 | Extend class notation with convergence relation for limits in the extended real numbers. |
class ~~>* | ||
Definition | df-xlim 43782 | Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ ~~>* = (βπ‘β(ordTopβ β€ )) | ||
Theorem | xlimrel 43783 | The limit on extended reals is a relation. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ Rel ~~>* | ||
Theorem | xlimres 43784 | A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β πΉ β (β* βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ~~>*π΄ β (πΉ βΎ (β€β₯βπ))~~>*π΄)) | ||
Theorem | xlimcl 43785 | The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (πΉ~~>*π΄ β π΄ β β*) | ||
Theorem | rexlimddv2 43786* | Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β βπ₯ β π΄ π) & β’ (((π β§ π₯ β π΄) β§ π) β π) β β’ (π β π) | ||
Theorem | xlimclim 43787 | 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 43576). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimconst 43788* | 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 43789 | A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | xlimbr 43790* | 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 43791 | 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 43792* | Lemma for cnrefiisp 43793 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β) & β’ (π β Β¬ π΄ β β) & β’ (π β π΅ β Fin) & β’ πΆ = (β βͺ π΅) & β’ π· = ({(absβ(ββπ΄))} βͺ βͺ π¦ β ((π΅ β© β) β {π΄}){(absβ(π¦ β π΄))}) & β’ π = inf(π·, β*, < ) β β’ (π β βπ₯ β β+ βπ¦ β πΆ ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) | ||
Theorem | cnrefiisp 43793* | 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 43794* | 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 43795* | Lemma for xlimmnfv 43797: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*-β) & β’ (π β π β β) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π) | ||
Theorem | xlimmnfvlem2 43796* | Lemma for xlimmnf 43804: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) < π₯) β β’ (π β πΉ~~>*-β) | ||
Theorem | xlimmnfv 43797* | 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 43798* | 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 43799* | Lemma for xlimpnfv 43801: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*+β) & β’ (π β π β β) β β’ (π β βπ β π βπ β (β€β₯βπ)π β€ (πΉβπ)) | ||
Theorem | xlimpnfvlem2 43800* | Lemma for xlimpnfv 43801: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ < (πΉβπ)) β β’ (π β πΉ~~>*+β) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |