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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | climxrre 43701* | 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 43702 | 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 43703* | 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 43704* | The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) β β’ (π β ((lim supβπΉ) < π΄ β βπ β β sup(((πΉ β (π[,)+β)) β© β*), β*, < ) < π΄)) | ||
Theorem | liminfgord 43705 | Ordering property of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β inf(((πΉ β (π΄[,)+β)) β© β*), β*, < ) β€ inf(((πΉ β (π΅[,)+β)) β© β*), β*, < )) | ||
Theorem | limsupvald 43706* | 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 43707* | 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 43708 | Closure of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ β π β β’ (lim supβπΉ) β β* | ||
Theorem | liminfgf 43709 | Closure of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ πΊ:ββΆβ* | ||
Theorem | liminfval 43710* | The inferior limit of a set πΉ. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (πΉ β π β (lim infβπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | climlimsup 43711 | A sequence of real numbers converges if and only if it converges to its superior limit. The first hypothesis is needed (see climlimsupcex 43720 for a counterexample). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β πΉ β (lim supβπΉ))) | ||
Theorem | limsupge 43712* | The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) β β’ (π β (π΄ β€ (lim supβπΉ) β βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*), β*, < ))) | ||
Theorem | liminfgval 43713* | Value of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β β β (πΊβπ) = inf(((πΉ β (π[,)+β)) β© β*), β*, < )) | ||
Theorem | liminfcl 43714 | Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (πΉ β π β (lim infβπΉ) β β*) | ||
Theorem | liminfvald 43715* | The inferior limit of a set πΉ. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β (lim infβπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | liminfval5 43716* | 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 43717 | 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 43718 | 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 43719* | The superior limit, relativized to an unbounded set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) & β’ (π β πΉ β π) & β’ (π β π΄ β β) & β’ (π β sup(π΄, β*, < ) = +β) β β’ (π β (lim infβπΉ) = sup((πΊ β π΄), β*, < )) | ||
Theorem | climlimsupcex 43720 | Counterexample for climlimsup 43711, 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 43721 | Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) β β’ (π β (lim infβπΉ) β β*) | ||
Theorem | liminfresico 43722 | 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 43723* | The range of the given function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ = (π β β β¦ if(2 β₯ π, 0, 1)) & β’ (π β πΎ β β) β β’ (π β (πΉ β (πΎ[,)+β)) = {0, 1}) | ||
Theorem | limsup10ex 43724 | 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 43725 | 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 43726* | 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 43727* | The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex 43748 for a counterexample). The inequality can be strict, see liminfltlimsupex 43732. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ (π β βπ β β βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β β ) β β’ (π β (lim infβπΉ) β€ (lim supβπΉ)) | ||
Theorem | limsupgtlem 43728* | 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 43729* | 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 43730 | 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 43731* | 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 43732 | 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 43733* | 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 43734* | 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 43735 | 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 43736 | 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 43737* | 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 43738 | 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 43739 | 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 43740* | 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 43741* | 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 43742* | 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 43743* | 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 43744 | The inferior limit of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (lim infββ ) = +β | ||
Theorem | limsupval4 43745* | 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 43746* | 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 43747* | 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 43748 | A counterexample for liminflelimsup 43727, showing that the second hypothesis is needed. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (lim supββ ) < (lim infββ ) | ||
Theorem | limsupvaluz3 43749* | 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 43750* | 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 43751* | 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 43752 | 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 43753* | 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 43754* | 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 43755* | 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 43756* | 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 43757 | 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 43758 | 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 43736). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim infβπΉ) β β) & β’ (π β (lim supβπΉ) β€ (lim infβπΉ)) β β’ (π β πΉ β dom β ) | ||
Theorem | climliminflimsup 43759 | 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 43739). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim infβπΉ) β β β§ (lim supβπΉ) β€ (lim infβπΉ)))) | ||
Theorem | climliminflimsup2 43760 | 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 43739). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β ((lim supβπΉ) β β β§ (lim supβπΉ) β€ (lim infβπΉ)))) | ||
Theorem | climliminflimsup3 43761 | 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 43762 | 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 43763* | 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 43764* | 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 43765* | A sequence converges to +β if and only if its negation converges to -β. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) | ||
Theorem | liminflbuz2 43766* | 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 43767* | 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 43768* | 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 43799. | ||
Syntax | clsxlim 43769 | Extend class notation with convergence relation for limits in the extended real numbers. |
class ~~>* | ||
Definition | df-xlim 43770 | Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ ~~>* = (βπ‘β(ordTopβ β€ )) | ||
Theorem | xlimrel 43771 | The limit on extended reals is a relation. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ Rel ~~>* | ||
Theorem | xlimres 43772 | A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β πΉ β (β* βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ~~>*π΄ β (πΉ βΎ (β€β₯βπ))~~>*π΄)) | ||
Theorem | xlimcl 43773 | The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (πΉ~~>*π΄ β π΄ β β*) | ||
Theorem | rexlimddv2 43774* | Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β βπ₯ β π΄ π) & β’ (((π β§ π₯ β π΄) β§ π) β π) β β’ (π β π) | ||
Theorem | xlimclim 43775 | 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 43564). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimconst 43776* | 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 43777 | A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) β β’ (π β πΉ~~>*π΄) | ||
Theorem | xlimbr 43778* | 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 43779 | 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 43780* | Lemma for cnrefiisp 43781 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β) & β’ (π β Β¬ π΄ β β) & β’ (π β π΅ β Fin) & β’ πΆ = (β βͺ π΅) & β’ π· = ({(absβ(ββπ΄))} βͺ βͺ π¦ β ((π΅ β© β) β {π΄}){(absβ(π¦ β π΄))}) & β’ π = inf(π·, β*, < ) β β’ (π β βπ₯ β β+ βπ¦ β πΆ ((π¦ β β β§ π¦ β π΄) β π₯ β€ (absβ(π¦ β π΄)))) | ||
Theorem | cnrefiisp 43781* | 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 43782* | 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 43783* | Lemma for xlimmnfv 43785: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*-β) & β’ (π β π β β) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π) | ||
Theorem | xlimmnfvlem2 43784* | Lemma for xlimmnf 43792: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) < π₯) β β’ (π β πΉ~~>*-β) | ||
Theorem | xlimmnfv 43785* | 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 43786* | 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 43787* | Lemma for xlimpnfv 43789: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β πΉ~~>*+β) & β’ (π β π β β) β β’ (π β βπ β π βπ β (β€β₯βπ)π β€ (πΉβπ)) | ||
Theorem | xlimpnfvlem2 43788* | Lemma for xlimpnfv 43789: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ < (πΉβπ)) β β’ (π β πΉ~~>*+β) | ||
Theorem | xlimpnfv 43789* | 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 43790* | Lemma for xlimclim2 43791. Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) & β’ (π β π΄ β β) & β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β β’ (π β (πΉ~~>*π΄ β πΉ β π΄)) | ||
Theorem | xlimclim2 43791 | Given a sequence of extended reals, it converges to a real number π΄ w.r.t. the standard topology on the reals (see climreeq 43564), 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 43792* | 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 43793* | 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 43794* | 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 43795* | 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 43796 | In this lemma for climxlim2 43797 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 43797 | 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 43798* | 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 43799* | 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 43800 | A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ (π β π β β€) & β’ (π β πΉ β π) β β’ (π β ((πΉ βΎ (β€β₯βπ)) β π΄ β πΉ β π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |