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 𝐺 , ℝ* , < ) )