:: deftheorem defines injective WAYBEL18:def 5 :
for Z being TopStruct holds
( Z is injective iff for X being non empty TopSpace
for f being Function of X,Z st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,Z st
( g is continuous & g | the carrier of X = f ) );