begin
:: deftheorem Def1 defines compact COMPACT1:def 1 :
for X being TopSpace
for P being Subset-Family of X holds
( P is compact iff for U being Subset of X st U in P holds
U is compact );
:: deftheorem Def2 defines relatively-compact COMPACT1:def 2 :
for X being TopSpace
for U being Subset of X holds
( U is relatively-compact iff Cl U is compact );
:: deftheorem Def3 defines liminally-compact COMPACT1:def 3 :
for X being non empty TopSpace holds
( X is liminally-compact iff for x being Point of X ex B being basis of x st B is compact );
:: deftheorem Def4 defines locally-relatively-compact COMPACT1:def 4 :
for X being non empty TopSpace holds
( X is locally-relatively-compact iff for x being Point of X ex U being a_neighborhood of x st U is relatively-compact );
:: deftheorem Def5 defines locally-closed/compact COMPACT1:def 5 :
for X being non empty TopSpace holds
( X is locally-closed/compact iff for x being Point of X ex U being a_neighborhood of x st
( U is closed & U is compact ) );
:: deftheorem Def6 defines locally-compact COMPACT1:def 6 :
for X being non empty TopSpace holds
( X is locally-compact iff for x being Point of X ex U being a_neighborhood of x st U is compact );
theorem
theorem Th2:
:: deftheorem defines embedding COMPACT1:def 7 :
for X, Y being TopSpace
for f being Function of X,Y holds
( f is embedding iff ex h being Function of X,(Y | (rng f)) st
( h = f & h is being_homeomorphism ) );
theorem Th3:
:: deftheorem Def8 defines compactification COMPACT1:def 8 :
for X, Y being TopSpace
for h being Function of X,Y holds
( h is compactification iff ( h is embedding & Y is compact & h .: ([#] X) is dense ) );
:: deftheorem Def9 defines One-Point_Compactification COMPACT1:def 9 :
for X being TopStruct
for b2 being strict TopStruct holds
( b2 = One-Point_Compactification X iff ( the carrier of b2 = succ ([#] X) & the topology of b2 = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) );
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem