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 φFV
limsupvald.2 G=ksupFk+∞**<
Assertion limsupvald φlim supF=supranG*<

Proof

Step Hyp Ref Expression
1 limsupvald.1 φFV
2 limsupvald.2 G=ksupFk+∞**<
3 2 limsupval FVlim supF=supranG*<
4 1 3 syl φlim supF=supranG*<