:: deftheorem Def8 defines lim_sup MESFUNC8:def 8 :
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b₃ being PartFunc of X,ExtREAL holds
( b₃ = lim_sup f iff ( dom b₃ = dom (f . 0) & ( for x being Element of X st x in dom b₃ holds
b₃ . x = lim_sup (f # x) ) ) );