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	$$⊢\phi \to F\in V$$
	limsupvald.2	$$⊢G=\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$$
Assertion	limsupvald	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)=inf\left(\mathrm{ran}G,{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		limsupvald.1	$$⊢\phi \to F\in V$$
2		limsupvald.2	$$⊢G=\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right]\cap {ℝ}^{*},{ℝ}^{*},<\right)\right)$$
3	2	limsupval	$$⊢F\in V\to \mathrm{lim\; sup}\left(F\right)=inf\left(\mathrm{ran}G,{ℝ}^{*},<\right)$$
4	1 3	syl	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)=inf\left(\mathrm{ran}G,{ℝ}^{*},<\right)$$