![]() |
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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | climeldmeqmpt2 44401* | 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 44402 | 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 44403* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π₯ β π) β πΆ β π) β β’ (π β ((π₯ β π΄ β¦ πΆ) β π· β (π₯ β π΅ β¦ πΆ) β π·)) | ||
Theorem | climfvd 44404 | The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ β π΄) β β’ (π β π΄ = ( β βπΉ)) | ||
Theorem | limsuplesup 44405 | An upper bound for the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ β π) & β’ (π β πΎ β β) β β’ (π β (lim supβπΉ) β€ sup(((πΉ β (πΎ[,)+β)) β© β*), β*, < )) | ||
Theorem | limsupresico 44406 | 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 44407* | 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 44408* | 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 44409 | 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 44410* | If the limsup is not +β, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) & β’ (π β (lim supβπΉ) β +β) β β’ (π β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) | ||
Theorem | limsupres 44411 | 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 44412* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ (π β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) β β’ (π β πΉ β inf(ran πΉ, β*, < )) | ||
Theorem | climinf2 44413* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ (π β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) β β’ (π β πΉ β inf(ran πΉ, β*, < )) | ||
Theorem | limsupvaluz 44414* | 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 44415 | 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 44416* | 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 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.) |
β’ β²ππΉ & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ*) β β’ (π β ((lim supβπΉ) = +β β βπ₯ β β βπ β β βπ β π΄ (π β€ π β§ π₯ β€ (πΉβπ)))) | ||
Theorem | limsupubuzlem 44418* | If the limsup is not +β, then the function is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ (π β πΎ β β) & β’ (π β βπ β π (πΎ β€ π β (πΉβπ) β€ π)) & β’ π = if((ββπΎ) β€ π, π, (ββπΎ)) & β’ π = sup(ran (π β (π...π) β¦ (πΉβπ)), β, < ) & β’ π = if(π β€ π, π, π) β β’ (π β βπ₯ β β βπ β π (πΉβπ) β€ π₯) | ||
Theorem | limsupubuz 44419* | 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 44420* | 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 44421* | 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 44422* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ (π β πΉ β dom β ) β β’ (π β πΉ β inf(ran πΉ, β*, < )) | ||
Theorem | limsupvaluzmpt 44423* | 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 44424* | 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 44425* | If the limsup is not +β, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ β²ππ & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β β) & β’ (π β (lim supβ(π β π β¦ π΅)) β +β) β β’ (π β βπ₯ β β βπ β π π΅ β€ π₯) | ||
Theorem | limsupmnflem 44426* | 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 44427* | 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 44428* | 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 44429* | 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 44430* | 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 44431* | 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 44432* | 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 44433* | 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 44434* | 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 44435* | 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 44436* | 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 44437* | 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 44438* | 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 44439* | 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 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 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 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 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 44442* | 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 44443* | 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 44444* | 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 44445* | 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 44446* | 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 44447* | 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 44448 | If β is a complex number, then it converges to itself. See 0ncn 11127 and its comment; see also the comment in climlimsupcex 44475. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (β β β β β β β ) | ||
Theorem | climuzlem 44449* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) | ||
Theorem | climuz 44450* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²ππΉ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) | ||
Theorem | lmbr3v 44451* | 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 44452* | 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 44453* | 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 44454* | 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 44455* | 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 44456* | 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 44457 | 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 44458* | 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 44459* | The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) β β’ (π β ((lim supβπΉ) < π΄ β βπ β β sup(((πΉ β (π[,)+β)) β© β*), β*, < ) < π΄)) | ||
Theorem | liminfgord 44460 | Ordering property of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β inf(((πΉ β (π΄[,)+β)) β© β*), β*, < ) β€ inf(((πΉ β (π΅[,)+β)) β© β*), β*, < )) | ||
Theorem | limsupvald 44461* | 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 44462* | 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 44463 | Closure of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ β π β β’ (lim supβπΉ) β β* | ||
Theorem | liminfgf 44464 | Closure of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ πΊ:ββΆβ* | ||
Theorem | liminfval 44465* | The inferior limit of a set πΉ. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (πΉ β π β (lim infβπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | climlimsup 44466 | A sequence of real numbers converges if and only if it converges to its superior limit. The first hypothesis is needed (see climlimsupcex 44475 for a counterexample). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉ β dom β β πΉ β (lim supβπΉ))) | ||
Theorem | limsupge 44467* | The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) β β’ (π β (π΄ β€ (lim supβπΉ) β βπ β β π΄ β€ sup(((πΉ β (π[,)+β)) β© β*), β*, < ))) | ||
Theorem | liminfgval 44468* | Value of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β β β (πΊβπ) = inf(((πΉ β (π[,)+β)) β© β*), β*, < )) | ||
Theorem | liminfcl 44469 | Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (πΉ β π β (lim infβπΉ) β β*) | ||
Theorem | liminfvald 44470* | The inferior limit of a set πΉ. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β (lim infβπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | liminfval5 44471* | 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 44472 | 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 44473 | 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 44474* | The superior limit, relativized to an unbounded set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΊ = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*), β*, < )) & β’ (π β πΉ β π) & β’ (π β π΄ β β) & β’ (π β sup(π΄, β*, < ) = +β) β β’ (π β (lim infβπΉ) = sup((πΊ β π΄), β*, < )) | ||
Theorem | climlimsupcex 44475 | Counterexample for climlimsup 44466, showing that the first hypothesis is needed, if the empty set is a complex number (see 0ncn 11127 and its comment). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ Β¬ π β β€ & β’ π = (β€β₯βπ) & β’ πΉ = β β β’ ((β β β β§ Β¬ -β β β) β (πΉ:πβΆβ β§ πΉ β dom β β§ Β¬ πΉ β (lim supβπΉ))) | ||
Theorem | liminfcld 44476 | Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) β β’ (π β (lim infβπΉ) β β*) | ||
Theorem | liminfresico 44477 | 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 44478* | The range of the given function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ πΉ = (π β β β¦ if(2 β₯ π, 0, 1)) & β’ (π β πΎ β β) β β’ (π β (πΉ β (πΎ[,)+β)) = {0, 1}) | ||
Theorem | limsup10ex 44479 | 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 44480 | 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 44481* | 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 44482* | The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex 44503 for a counterexample). The inequality can be strict, see liminfltlimsupex 44487. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β πΉ β π) & β’ (π β βπ β β βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β β ) β β’ (π β (lim infβπΉ) β€ (lim supβπΉ)) | ||
Theorem | limsupgtlem 44483* | 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 44484* | 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 44485 | 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 44486* | 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 44487 | 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 44488* | 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 44489* | 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 44490 | 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 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 | liminfvalxrmpt 44492* | 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 44493 | 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 44494 | 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 44495* | 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 44496* | 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 44497* | 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 44498* | 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 44499 | The inferior limit of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (lim infββ ) = +β | ||
Theorem | limsupval4 44500* | 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β(π₯ β π΄ β¦ -ππ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |