Metamath Proof Explorer


Theorem limsupvald

Description: The superior limit of a sequence F of extended real numbers is the infimum of the set of suprema of all restrictions of F to an upperset of reals . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsupvald.1 ( 𝜑𝐹𝑉 )
limsupvald.2 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
Assertion limsupvald ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 limsupvald.1 ( 𝜑𝐹𝑉 )
2 limsupvald.2 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
3 2 limsupval ( 𝐹𝑉 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )
4 1 3 syl ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )