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