P. 410 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40901-41000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	limsupge 40901*	The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐵⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 ≤ (lim sup‘𝐹) ↔ ∀𝑘 ∈ ℝ 𝐴 ≤ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )))
Theorem	liminfgval 40902*	Value of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    ⇒   ⊢ (𝑀 ∈ ℝ → (𝐺‘𝑀) = inf(((𝐹 “ (𝑀[,)+∞)) ∩ ℝ*), ℝ*, < ))
Theorem	liminfcl 40903	Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐹 ∈ 𝑉 → (lim inf‘𝐹) ∈ ℝ*)
Theorem	liminfvald 40904*	The inferior limit of a set 𝐹. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) = sup(ran 𝐺, ℝ*, < ))
Theorem	liminfval5 40905*	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 40906	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 40907	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 40908*	The superior limit, relativized to an unbounded set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) = sup((𝐺 “ 𝐴), ℝ*, < ))
Theorem	climlimsupcex 40909	Counterexample for climlimsup 40900, showing that the first hypothesis is needed, if the empty set is a complex number (see 0ncn 10290 and its comment) (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ¬ 𝑀 ∈ ℤ    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐹 = ∅    ⇒   ⊢ ((∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ) → (𝐹:𝑍⟶ℝ ∧ 𝐹 ∈ dom ⇝ ∧ ¬ 𝐹 ⇝ (lim sup‘𝐹)))
Theorem	liminfcld 40910	Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) ∈ ℝ*)
Theorem	liminfresico 40911	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 40912*	The range of the given function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 1))    &   ⊢ (𝜑 → 𝐾 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹 “ (𝐾[,)+∞)) = {0, 1})
Theorem	limsup10ex 40913	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 40914	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 40915*	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 40916*	The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex 40937 for a counterexample). The inequality can be strict, see liminfltlimsupex 40921. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))
Theorem	limsupgtlem 40917*	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 40918*	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 40919	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 40920*	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 40921	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 40922*	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 40923*	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 40924	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 40925	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 40926*	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 40927	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 40928	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 40929*	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 40930*	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 40931*	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 40932*	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 40933	The inferior limit of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (lim inf‘∅) = +∞
Theorem	limsupval4 40934*	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 40935*	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 40936*	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 40937	A counterexample for liminflelimsup 40916, showing that the second hypothesis is needed. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (lim sup‘∅) < (lim inf‘∅)
Theorem	limsupvaluz3 40938*	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 40939*	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 40940*	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 40941	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 40942*	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 40943*	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 40944*	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 40945*	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 40946	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 40947	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 40925). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → (lim inf‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → (lim sup‘𝐹) ≤ (lim inf‘𝐹))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	climliminflimsup 40948	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 40928). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ ((lim inf‘𝐹) ∈ ℝ ∧ (lim sup‘𝐹) ≤ (lim inf‘𝐹))))
Theorem	climliminflimsup2 40949	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 40928). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ ((lim sup‘𝐹) ∈ ℝ ∧ (lim sup‘𝐹) ≤ (lim inf‘𝐹))))
Theorem	climliminflimsup3 40950	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 40951	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 40952*	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 40953*	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 40954*	A sequence converges to +∞ if and only if its negation converges to -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗) ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≤ 𝑥))
Theorem	liminflbuz2 40955*	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 40956*	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 40957*	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‘𝐹) ≠ -∞)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶ℝ)
20.33.7.2  Limits for sequences of extended real numbers 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 40988.
Syntax	clsxlim 40958	Extend class notation with convergence relation for limits in the extended real numbers.
class ~~>*
Definition	df-xlim 40959	Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ ~~>* = (⇝𝑡‘(ordTop‘ ≤ ))
Theorem	xlimrel 40960	The limit on extended reals is a relation. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Rel ~~>*
Theorem	xlimres 40961	A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐹 ∈ (ℝ* ↑pm ℂ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ↾ (ℤ≥‘𝑀))~~>*𝐴))
Theorem	xlimcl 40962	The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝐹~~>*𝐴 → 𝐴 ∈ ℝ*)
Theorem	rexlimddv2 40963*	Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	xlimclim 40964	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 40753). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	xlimconst 40965*	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 40966	A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → 𝐹~~>*𝐴)
Theorem	xlimbr 40967*	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 40968	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 40969*	Lemma for cnrefiisp 40970 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ 𝐶 = (ℝ ∪ 𝐵)    &   ⊢ 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})    &   ⊢ 𝑋 = inf(𝐷, ℝ*, < )    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴))))
Theorem	cnrefiisp 40970*	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 40971*	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 40972*	Lemma for xlimmnfv 40974: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*-∞)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑋)
Theorem	xlimmnfvlem2 40973*	Lemma for xlimmnf 40981: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥)    ⇒   ⊢ (𝜑 → 𝐹~~>*-∞)
Theorem	xlimmnfv 40974*	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 40975*	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 40976*	Lemma for xlimpnfv 40978: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*+∞)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑋 ≤ (𝐹‘𝑘))
Theorem	xlimpnfvlem2 40977*	Lemma for xlimpnfv 40978: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹~~>*+∞)
Theorem	xlimpnfv 40978*	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 40979*	Lemma for xlimclim2 40980. Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	xlimclim2 40980	Given a sequence of extended reals, it converges to a real number 𝐴 w.r.t. the standard topology on the reals (see climreeq 40753), 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 40981*	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 40982*	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 40983*	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 40984*	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 40985	In this lemma for climxlim2 40986 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 40986	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 40987*	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 40988*	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 40989	A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (ℤ≥‘𝑀)) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	climresdm 40990	A real function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ (𝐹 ↾ (ℤ≥‘𝑀)) ∈ dom ⇝ ))
Theorem	dmclimxlim 40991	A real valued sequence that converges w.r.t. the topology on the complex numbers, converges w.r.t. the topology on the extended reals (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ~~>*)
Theorem	xlimmnflimsup2 40992	A sequence of extended reals converges to -∞ if and only if its superior limit is also -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*-∞ ↔ (lim sup‘𝐹) = -∞))
Theorem	xlimuni 40993	An infinite sequence converges to at most one limit (w.r.t. to the standard topology on the extended reals). (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝐹~~>*𝐴)    &   ⊢ (𝜑 → 𝐹~~>*𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	xlimclimdm 40994	A sequence of extended reals that converges to a real w.r.t. the standard topology on the extended reals, also converges w.r.t. to the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	xlimfun 40995	The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Fun ~~>*
Theorem	xlimmnflimsup 40996	If a sequence of extended reals converges to -∞ then its superior limit is also -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*-∞)    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) = -∞)
Theorem	xlimdm 40997	Two ways to express that a function has a limit. (The expression (~~>*‘𝐹) is sometimes useful as a shorthand for "the unique limit of the function 𝐹"). (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝐹 ∈ dom ~~>* ↔ 𝐹~~>*(~~>*‘𝐹))
Theorem	xlimpnfxnegmnf2 40998*	A sequence converges to +∞ if and only if its negation converges to -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*+∞ ↔ (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))~~>*-∞))
Theorem	xlimresdm 40999	A function converges in the extended reals iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝐹 ∈ (ℝ* ↑pm ℂ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ~~>* ↔ (𝐹 ↾ (ℤ≥‘𝑀)) ∈ dom ~~>*))
Theorem	xlimpnfliminf 41000	If a sequence of extended reals converges to +∞ then its superior limit is also +∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*+∞)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) = +∞)