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	|- ( ph -> F e. V )
	limsupvald.2	|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
Assertion	limsupvald	|- ( ph -> ( limsup ` F ) = inf ( ran G , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		limsupvald.1	|- ( ph -> F e. V )
2		limsupvald.2	|- G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
3	2	limsupval	|- ( F e. V -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
4	1 3	syl	|- ( ph -> ( limsup ` F ) = inf ( ran G , RR* , < ) )