![]() |
Metamath
Proof Explorer Theorem List (p. 445 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | limsupref 44401* | If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β βπ β β βπ β β βπ β π΄ (π β€ π β (absβ(πΉβπ)) β€ π)) β β’ (π β (lim supβπΉ) β β) | ||
Theorem | limsupbnd1f 44402* | If a sequence is eventually at most π΄, then the limsup is also at most π΄. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) & β’ (π β βπ β β βπ β π΅ (π β€ π β (πΉβπ) β€ π΄)) β β’ (π β (lim supβπΉ) β€ π΄) | ||
Theorem | climbddf 44403* | A converging sequence of complex numbers is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ β dom β β§ βπ β π (πΉβπ) β β) β βπ₯ β β βπ β π (absβ(πΉβπ)) β€ π₯) | ||
Theorem | climeqf 44404* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) = (πΊβπ)) β β’ (π β (πΉ β π΄ β πΊ β π΄)) | ||
Theorem | climeldmeqmpt3 44405* | Two functions that are eventually equal, either both are convergent or both are divergent. TODO: this is more general than climeldmeqmpt 44384 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β π β π΄) & β’ (π β π β πΆ) & β’ ((π β§ π β π) β π΅ β π) & β’ ((π β§ π β π) β π΅ = π·) β β’ (π β ((π β π΄ β¦ π΅) β dom β β (π β πΆ β¦ π·) β dom β )) | ||
Theorem | limsupcld 44406 | Closure of the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ β π) β β’ (π β (lim supβπΉ) β β*) | ||
Theorem | climfv 44407 | The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (πΉ β π΄ β π΄ = ( β βπΉ)) | ||
Theorem | limsupval3 44408* | The superior limit of an infinite sequence πΉ of extended real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆβ*) & β’ πΊ = (π β β β¦ sup((πΉ β (π[,)+β)), β*, < )) β β’ (π β (lim supβπΉ) = inf(ran πΊ, β*, < )) | ||
Theorem | climfveqmpt2 44409* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π β π) β πΆ β π) β β’ (π β ( β β(π β π΄ β¦ πΆ)) = ( β β(π β π΅ β¦ πΆ))) | ||
Theorem | limsup0 44410 | The superior limit of the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (lim supββ ) = -β | ||
Theorem | climeldmeqmpt2 44411* | Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π β π) β πΆ β π) β β’ (π β ((π β π΄ β¦ πΆ) β dom β β (π β π΅ β¦ πΆ) β dom β )) | ||
Theorem | limsupresre 44412 | The supremum limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ β π) β β’ (π β (lim supβ(πΉ βΎ β)) = (lim supβπΉ)) | ||
Theorem | climeqmpt 44413* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π₯ β π) β πΆ β π) β β’ (π β ((π₯ β π΄ β¦ πΆ) β π· β (π₯ β π΅ β¦ πΆ) β π·)) | ||
Theorem | climfvd 44414 | The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ β π΄) β β’ (π β π΄ = ( β βπΉ)) | ||
Theorem | limsuplesup 44415 | An upper bound for the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ β π) & β’ (π β πΎ β β) β β’ (π β (lim supβπΉ) β€ sup(((πΉ β (πΎ[,)+β)) β© β*), β*, < )) | ||
Theorem | limsupresico 44416 | The superior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β) & β’ π = (π[,)+β) & β’ (π β πΉ β π) β β’ (π β (lim supβ(πΉ βΎ π)) = (lim supβπΉ)) | ||
Theorem | limsuppnfdlem 44417* | If the restriction of a function to every upper interval is unbounded above, its lim sup is +β. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) & β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β (lim supβπΉ) = +β) | ||
Theorem | limsuppnfd 44418* | If the restriction of a function to every upper interval is unbounded above, its lim sup is +β. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ))) β β’ (π β (lim supβπΉ) = +β) | ||
Theorem | limsupresuz 44419 | If the real part of the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ β π) & β’ (π β dom (πΉ βΎ β) β β€) β β’ (π β (lim supβ(πΉ βΎ π)) = (lim supβπΉ)) | ||
Theorem | limsupub 44420* | If the limsup is not +β, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β (lim supβπΉ) β +β) β β’ (π β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) | ||
Theorem | limsupres 44421 | The superior limit of a restriction is less than or equal to the original superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ β π) β β’ (π β (lim supβ(πΉ βΎ πΆ)) β€ (lim supβπΉ)) | ||
Theorem | climinf2lem 44422* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ (π β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) β β’ (π β πΉ β inf(ran πΉ, β*, < )) | ||
Theorem | climinf2 44423* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ (π β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) β β’ (π β πΉ β inf(ran πΉ, β*, < )) | ||
Theorem | limsupvaluz 44424* | The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -β and the r.h.s. would be +β). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β (lim supβπΉ) = inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )), β*, < )) | ||
Theorem | limsupresuz2 44425 | If the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ β π) & β’ (π β dom πΉ β β€) β β’ (π β (lim supβ(πΉ βΎ π)) = (lim supβπΉ)) | ||
Theorem | limsuppnflem 44426* | If the restriction of a function to every upper interval is unbounded above, its lim sup is +β. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) β β’ (π β ((lim supβπΉ) = +β β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) | ||
Theorem | limsuppnf 44427* | If the restriction of a function to every upper interval is unbounded above, its lim sup is +β. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) β β’ (π β ((lim supβπΉ) = +β β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) | ||
Theorem | limsupubuzlem 44428* | If the limsup is not +β, then the function is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β βπ β π (πΎ β€ π β (πΉβπ) β€ π)) & β’ π = if((ββπΎ) β€ π, π, (ββπΎ)) & β’ π = sup(ran (π β (π...π) β¦ (πΉβπ)), β, < ) & β’ π = if(π β€ π, π, π) β β’ (π β βπ₯ β β βπ β π (πΉβπ) β€ π₯) | ||
Theorem | limsupubuz 44429* | For a real-valued function on a set of upper integers, if the superior limit is not +β, then the function is bounded above. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β (lim supβπΉ) β +β) β β’ (π β βπ₯ β β βπ β π (πΉβπ) β€ π₯) | ||
Theorem | climinf2mpt 44430* | A bounded below, monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β) & β’ (π = π β π΅ = πΆ) & β’ ((π β§ π β π β§ π = (π + 1)) β πΆ β€ π΅) & β’ (π β (π β π β¦ π΅) β dom β ) β β’ (π β (π β π β¦ π΅) β inf(ran (π β π β¦ π΅), β*, < )) | ||
Theorem | climinfmpt 44431* | A bounded below, monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β) & β’ (π = π β π΅ = πΆ) & β’ ((π β§ π β π β§ π = (π + 1)) β πΆ β€ π΅) & β’ (π β βπ₯ β β βπ β π π₯ β€ π΅) β β’ (π β (π β π β¦ π΅) β inf(ran (π β π β¦ π΅), β*, < )) | ||
Theorem | climinf3 44432* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ (π β πΉ β dom β ) β β’ (π β πΉ β inf(ran πΉ, β*, < )) | ||
Theorem | limsupvaluzmpt 44433* | The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -β and the r.h.s. would be +β). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β*) β β’ (π β (lim supβ(π β π β¦ π΅)) = inf(ran (π β π β¦ sup(ran (π β (β€β₯βπ) β¦ π΅), β*, < )), β*, < )) | ||
Theorem | limsupequzmpt2 44434* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππ΄ & β’ β²ππ΅ & β’ π΄ = (β€β₯βπ) & β’ π΅ = (β€β₯βπ) & β’ (π β πΎ β π΄) & β’ (π β πΎ β π΅) & β’ ((π β§ π β (β€β₯βπΎ)) β πΆ β π) β β’ (π β (lim supβ(π β π΄ β¦ πΆ)) = (lim supβ(π β π΅ β¦ πΆ))) | ||
Theorem | limsupubuzmpt 44435* | If the limsup is not +β, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β) & β’ (π β (lim supβ(π β π β¦ π΅)) β +β) β β’ (π β βπ₯ β β βπ β π π΅ β€ π₯) | ||
Theorem | limsupmnflem 44436* | The superior limit of a function is -β if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ πΊ = (π β β β¦ sup((πΉ β (π[,)+β)), β*, < )) β β’ (π β ((lim supβπΉ) = -β β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) | ||
Theorem | limsupmnf 44437* | The superior limit of a function is -β if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) β β’ (π β ((lim supβπΉ) = -β β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) | ||
Theorem | limsupequzlem 44438* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ (π β πΉ Fn (β€β₯βπ)) & β’ (π β π β β€) & β’ (π β πΊ Fn (β€β₯βπ)) & β’ (π β πΎ β β€) & β’ ((π β§ π β (β€β₯βπΎ)) β (πΉβπ) = (πΊβπ)) β β’ (π β (lim supβπΉ) = (lim supβπΊ)) | ||
Theorem | limsupequz 44439* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ (π β π β β€) & β’ (π β πΉ Fn (β€β₯βπ)) & β’ (π β π β β€) & β’ (π β πΊ Fn (β€β₯βπ)) & β’ (π β πΎ β β€) & β’ ((π β§ π β (β€β₯βπΎ)) β (πΉβπ) = (πΊβπ)) β β’ (π β (lim supβπΉ) = (lim supβπΊ)) | ||
Theorem | limsupre2lem 44440* | Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) β β’ (π β ((lim supβπΉ) β β β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯)))) | ||
Theorem | limsupre2 44441* | Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) β β’ (π β ((lim supβπΉ) β β β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ < (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) < π₯)))) | ||
Theorem | limsupmnfuzlem 44442* | The superior limit of a function is -β if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β ((lim supβπΉ) = -β β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) | ||
Theorem | limsupmnfuz 44443* | The superior limit of a function is -β if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β ((lim supβπΉ) = -β β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) | ||
Theorem | limsupequzmptlem 44444* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ (π β π β β€) & β’ π΄ = (β€β₯βπ) & β’ π΅ = (β€β₯βπ) & β’ ((π β§ π β π΄) β πΆ β π) & β’ ((π β§ π β π΅) β πΆ β π) & β’ πΎ = if(π β€ π, π, π) β β’ (π β (lim supβ(π β π΄ β¦ πΆ)) = (lim supβ(π β π΅ β¦ πΆ))) | ||
Theorem | limsupequzmpt 44445* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ (π β π β β€) & β’ π΄ = (β€β₯βπ) & β’ π΅ = (β€β₯βπ) & β’ ((π β§ π β π΄) β πΆ β π) & β’ ((π β§ π β π΅) β πΆ β π) β β’ (π β (lim supβ(π β π΄ β¦ πΆ)) = (lim supβ(π β π΅ β¦ πΆ))) | ||
Theorem | limsupre2mpt 44446* | Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β*) β β’ (π β ((lim supβ(π₯ β π΄ β¦ π΅)) β β β (βπ¦ β β βπ β β βπ₯ β π΄ (π β€ π₯ β§ π¦ < π΅) β§ βπ¦ β β βπ β β βπ₯ β π΄ (π β€ π₯ β π΅ < π¦)))) | ||
Theorem | limsupequzmptf 44447* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππ΄ & β’ β²ππ΅ & β’ (π β π β β€) & β’ (π β π β β€) & β’ π΄ = (β€β₯βπ) & β’ π΅ = (β€β₯βπ) & β’ ((π β§ π β π΄) β πΆ β π) & β’ ((π β§ π β π΅) β πΆ β π) β β’ (π β (lim supβ(π β π΄ β¦ πΆ)) = (lim supβ(π β π΅ β¦ πΆ))) | ||
Theorem | limsupre3lem 44448* | Given a function on the extended reals, 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, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) β β’ (π β ((lim supβπΉ) β β β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)))) | ||
Theorem | limsupre3 44449* | Given a function on the extended reals, 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, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) β β’ (π β ((lim supβπΉ) β β β (βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)) β§ βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)))) | ||
Theorem | limsupre3mpt 44450* | Given a function on the extended reals, 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, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β*) β β’ (π β ((lim supβ(π₯ β π΄ β¦ π΅)) β β β (βπ¦ β β βπ β β βπ₯ β π΄ (π β€ π₯ β§ π¦ β€ π΅) β§ βπ¦ β β βπ β β βπ₯ β π΄ (π β€ π₯ β π΅ β€ π¦)))) | ||
Theorem | limsupre3uzlem 44451* | Given a function on the extended reals, 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 eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β ((lim supβπΉ) β β β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯))) | ||
Theorem | limsupre3uz 44452* | Given a function on the extended reals, 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 eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ*) β β’ (π β ((lim supβπΉ) β β β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯))) | ||
Theorem | limsupreuz 44453* | Given a function on the reals, 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 | limsupvaluz2 44454* | 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 44455* | 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 44456* | 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 44457* | 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 44458 | If β is a complex number, then it converges to itself. See 0ncn 11128 and its comment; see also the comment in climlimsupcex 44485. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (β β β β β β β ) | ||
Theorem | climuzlem 44459* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) | ||
Theorem | climuz 44460* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) | ||
Theorem | lmbr3v 44461* | 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 44462* | 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 44463* | 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 44464* | 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 44465* | 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 44466* | 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 44467 | 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 44468* | 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 44469* | The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) β β’ (π β ((lim supβπΉ) < π΄ β βπ β β sup(((πΉ β (π[,)+β)) β© β*), β*, < ) < π΄)) | ||
Theorem | liminfgord 44470 | Ordering property of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β inf(((πΉ β (π΄[,)+β)) β© β*), β*, < ) β€ inf(((πΉ β (π΅[,)+β)) β© β*), β*, < )) | ||
Theorem | limsupvald 44471* | 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 44472* | 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 44473 | Closure of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ β π β β’ (lim supβπΉ) β β* | ||
Theorem | liminfgf 44474 | Closure of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ πΊ:ββΆβ* | ||
Theorem | liminfval 44475* | The inferior limit of a set πΉ. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (πΉ β π β (lim infβπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | climlimsup 44476 | A sequence of real numbers converges if and only if it converges to its superior limit. The first hypothesis is needed (see climlimsupcex 44485 for a counterexample). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β πΉ β (lim supβπΉ))) | ||
Theorem | limsupge 44477* | The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) β β’ (π β (π΄ β€ (lim supβπΉ) β βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*), β*, < ))) | ||
Theorem | liminfgval 44478* | Value of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β β β (πΊβπ) = inf(((πΉ β (π[,)+β)) β© β*), β*, < )) | ||
Theorem | liminfcl 44479 | Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (πΉ β π β (lim infβπΉ) β β*) | ||
Theorem | liminfvald 44480* | The inferior limit of a set πΉ. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β (lim infβπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | liminfval5 44481* | 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 44482 | 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 44483 | 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 44484* | The superior limit, relativized to an unbounded set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) & β’ (π β πΉ β π) & β’ (π β π΄ β β) & β’ (π β sup(π΄, β*, < ) = +β) β β’ (π β (lim infβπΉ) = sup((πΊ β π΄), β*, < )) | ||
Theorem | climlimsupcex 44485 | Counterexample for climlimsup 44476, showing that the first hypothesis is needed, if the empty set is a complex number (see 0ncn 11128 and its comment). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ Β¬ π β β€ & β’ π = (β€β₯βπ) & β’ πΉ = β β β’ ((β β β β§ Β¬ -β β β) β (πΉ:πβΆβ β§ πΉ β dom β β§ Β¬ πΉ β (lim supβπΉ))) | ||
Theorem | liminfcld 44486 | Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) β β’ (π β (lim infβπΉ) β β*) | ||
Theorem | liminfresico 44487 | 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 44488* | The range of the given function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ = (π β β β¦ if(2 β₯ π, 0, 1)) & β’ (π β πΎ β β) β β’ (π β (πΉ β (πΎ[,)+β)) = {0, 1}) | ||
Theorem | limsup10ex 44489 | 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 44490 | 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 44491* | 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 44492* | The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex 44513 for a counterexample). The inequality can be strict, see liminfltlimsupex 44497. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ (π β βπ β β βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β β ) β β’ (π β (lim infβπΉ) β€ (lim supβπΉ)) | ||
Theorem | limsupgtlem 44493* | 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 44494* | 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 44495 | 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 44496* | 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 44497 | 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 44498* | 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 44499* | 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 44500 | 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βπΉ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |