:: deftheorem defines lim_infs-preserving WAYBEL21:def 4 :
for S, T being non empty RelStr
for f being Function of S,T holds
( f is lim_infs-preserving iff for N being net of S holds f . (lim_inf N) = lim_inf (f * N) );