:: deftheorem defines compact-preserving WAYBEL34:def 14 :
for S, T being non empty reflexive RelStr
for f being Function of S,T holds
( f is compact-preserving iff for s being Element of S st s is compact holds
f . s is compact );