:: COMPACT1 semantic presentation

begin

definition
let X be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let P be ( ( ) ( ) Subset-Family of ) ;
attr P is compact means :: COMPACT1:def 1
 for U being ( ( ) ( ) Subset of ) st U : ( ( ) ( ) Subset of ) in P : ( ( ) ( ) Element of K19(K19(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) holds
U : ( ( ) ( ) Subset of ) is compact ;
end;

definition
let X be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let U be ( ( ) ( ) Subset of ) ;
attr U is relatively-compact means :: COMPACT1:def 2
 Cl U : ( ( ) ( ) Element of K19(K19(X : ( ( ) ( ) TopStruct ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( ) Element of K19( the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) is compact ;
end;

registration
let X be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster empty -> relatively-compact for ( ( ) ( ) Element of K19( the carrier of X : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ;
end;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster relatively-compact for ( ( ) ( ) Element of K19( the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ;
end;

registration
let X be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let U be ( ( relatively-compact ) ( relatively-compact ) Subset of ) ;
cluster Cl U : ( ( relatively-compact ) ( relatively-compact ) Element of K19( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( closed ) Element of K19( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) -> compact ;
end;

notation
let X be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let U be ( ( ) ( ) Subset of ) ;
synonym pre-compact U for relatively-compact ;
end;

notation
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
synonym liminally-compact X for locally-compact ;
end;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
redefine attr X is locally-compact means :: COMPACT1:def 3
 for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) ex B being ( ( ) ( non empty ) basis of x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) st B : ( ( ) ( non empty ) basis of b1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) is compact ;
end;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
attr X is locally-relatively-compact means :: COMPACT1:def 4
 for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) ex U being ( ( ) ( ) a_neighborhood of x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) st U : ( ( ) ( ) a_neighborhood of b1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) is relatively-compact ;
end;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
attr X is locally-closed/compact means :: COMPACT1:def 5
 for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) ex U being ( ( ) ( ) a_neighborhood of x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) st
( U : ( ( ) ( ) a_neighborhood of b1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) is closed & U : ( ( ) ( ) a_neighborhood of b1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) is compact );
end;

definition
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
attr X is locally-compact means :: COMPACT1:def 6
 for x being ( ( ) ( ) Point of ( ( ) ( ) set ) ) ex U being ( ( ) ( ) a_neighborhood of x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) st U : ( ( ) ( ) a_neighborhood of b1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) is compact ;
end;

registration
cluster non empty TopSpace-like liminally-compact -> non empty TopSpace-like locally-compact for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster non empty TopSpace-like regular locally-compact -> non empty TopSpace-like regular liminally-compact for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster non empty TopSpace-like locally-relatively-compact -> non empty TopSpace-like locally-closed/compact for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster non empty TopSpace-like locally-closed/compact -> non empty TopSpace-like locally-relatively-compact for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster non empty TopSpace-like locally-relatively-compact -> non empty TopSpace-like locally-compact for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster non empty TopSpace-like Hausdorff locally-compact -> non empty TopSpace-like Hausdorff locally-relatively-compact for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster non empty TopSpace-like compact -> non empty TopSpace-like locally-compact for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster non empty TopSpace-like discrete -> non empty TopSpace-like locally-compact for ( ( ) ( ) TopStruct ) ;
end;

registration
cluster non empty TopSpace-like discrete for ( ( ) ( ) TopStruct ) ;
end;

registration
let X be ( ( non empty TopSpace-like locally-compact ) ( non empty TopSpace-like locally-compact ) TopSpace) ;
let C be ( ( non empty closed ) ( non empty closed ) Subset of ) ;
cluster X : ( ( non empty TopSpace-like locally-compact ) ( non empty TopSpace-like locally-compact ) TopStruct ) | C : ( ( non empty closed ) ( non empty closed ) Element of K19( the carrier of X : ( ( non empty TopSpace-like locally-compact ) ( non empty TopSpace-like locally-compact ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of X : ( ( non empty TopSpace-like locally-compact ) ( non empty TopSpace-like locally-compact ) TopStruct ) ) -> strict locally-compact ;
end;

registration
let X be ( ( non empty TopSpace-like regular locally-compact ) ( non empty TopSpace-like regular liminally-compact locally-compact ) TopSpace) ;
let P be ( ( non empty open ) ( non empty open ) Subset of ) ;
cluster X : ( ( non empty TopSpace-like regular locally-compact ) ( non empty TopSpace-like regular liminally-compact locally-compact ) TopStruct ) | P : ( ( non empty open ) ( non empty open ) Element of K19( the carrier of X : ( ( non empty TopSpace-like regular locally-compact ) ( non empty TopSpace-like regular liminally-compact locally-compact ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of X : ( ( non empty TopSpace-like regular locally-compact ) ( non empty TopSpace-like regular liminally-compact locally-compact ) TopStruct ) ) -> strict locally-compact ;
end;

theorem :: COMPACT1:1
for X being ( ( non empty TopSpace-like Hausdorff ) ( non empty TopSpace-like T_0 T_1 Hausdorff ) TopSpace)
for E being ( ( non empty ) ( non empty ) Subset of ) st X : ( ( non empty TopSpace-like Hausdorff ) ( non empty TopSpace-like T_0 T_1 Hausdorff ) TopSpace) | E : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of b1 : ( ( non empty TopSpace-like Hausdorff ) ( non empty TopSpace-like T_0 T_1 Hausdorff ) TopSpace) ) is dense & X : ( ( non empty TopSpace-like Hausdorff ) ( non empty TopSpace-like T_0 T_1 Hausdorff ) TopSpace) | E : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of b1 : ( ( non empty TopSpace-like Hausdorff ) ( non empty TopSpace-like T_0 T_1 Hausdorff ) TopSpace) ) is locally-compact holds
X : ( ( non empty TopSpace-like Hausdorff ) ( non empty TopSpace-like T_0 T_1 Hausdorff ) TopSpace) | E : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of b1 : ( ( non empty TopSpace-like Hausdorff ) ( non empty TopSpace-like T_0 T_1 Hausdorff ) TopSpace) ) is open ;

theorem :: COMPACT1:2
for X, Y being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for A being ( ( ) ( ) Subset of ) st [#] X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed dense ) Element of K19( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) c= [#] Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non proper open closed dense ) Element of K19( the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) holds
(incl (X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) )) : ( ( Function-like V18( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) = A : ( ( ) ( ) Subset of ) ;

definition
let X, Y be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let f be ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ;
attr f is embedding means :: COMPACT1:def 7
 ex h being ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) , the carrier of (Y : ( ( ) ( ) set ) | (rng f : ( ( ) ( ) Element of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( strict ) ( strict ) SubSpace of Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of (Y : ( ( ) ( ) set ) | (rng f : ( ( ) ( ) Element of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( strict ) ( strict ) SubSpace of Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) , the carrier of (Y : ( ( ) ( ) set ) | (rng f : ( ( ) ( ) Element of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( strict ) ( strict ) SubSpace of Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st
( h : ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of (Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | (rng f : ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of (Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | (rng f : ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of (Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | (rng f : ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = f : ( ( ) ( ) Element of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) & h : ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of (Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | (rng f : ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of (Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | (rng f : ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of (Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | (rng f : ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is being_homeomorphism );
end;

theorem :: COMPACT1:3
for X, Y being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) st [#] X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed dense ) Element of K19( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) c= [#] Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non proper open closed dense ) Element of K19( the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) & ex Xy being ( ( ) ( ) Subset of ) st
( Xy : ( ( ) ( ) Subset of ) = [#] X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed dense ) Element of K19( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) & the topology of (Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | Xy : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( non empty open ) Element of K19(K19( the carrier of (b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( strict TopSpace-like ) SubSpace of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) = the topology of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( non empty open ) Element of K19(K19( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) holds
incl (X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) : ( ( Function-like V18( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of b2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) is embedding ;

definition
let X, Y be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let h be ( ( Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the carrier of Y : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ;
attr h is compactification means :: COMPACT1:def 8
( h : ( ( ) ( ) Element of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) is embedding & Y : ( ( ) ( ) set ) is compact & h : ( ( ) ( ) Element of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) .: ([#] X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non proper open closed dense ) Element of K19( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) is dense );
end;

registration
let X, Y be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) , the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) compactification -> Function-like V18( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) , the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) embedding for ( ( ) ( ) Element of K19(K20( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) , the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ;
end;

definition
let X be ( ( ) ( ) TopStruct ) ;
func One-Point_Compactification X -> ( ( strict ) ( strict ) TopStruct ) means :: COMPACT1:def 9
( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = succ ([#] X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non proper open closed dense ) Element of K19( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( ) set ) & the topology of it : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19(K19( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) = the topology of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( non empty open ) Element of K19(K19( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) \/ { (U : ( ( ) ( ) Subset of ) \/ {([#] X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non proper open closed dense ) Element of K19( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) } : ( ( ) ( non empty finite ) Element of K19(K19( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ) : ( ( ) ( non empty ) set ) where U is ( ( ) ( ) Subset of ) : ( U : ( ( ) ( ) Subset of ) is open & U : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of K19( the carrier of X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) is compact ) } : ( ( ) ( non empty ) set ) );
end;

registration
let X be ( ( ) ( ) TopStruct ) ;
cluster One-Point_Compactification X : ( ( ) ( ) TopStruct ) : ( ( strict ) ( strict ) TopStruct ) -> non empty strict ;
end;

theorem :: COMPACT1:4
for X being ( ( ) ( ) TopStruct ) holds [#] X : ( ( ) ( ) TopStruct ) : ( ( ) ( non proper dense ) Element of K19( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) c= [#] (One-Point_Compactification X : ( ( ) ( ) TopStruct ) ) : ( ( strict ) ( non empty strict ) TopStruct ) : ( ( ) ( non empty non proper dense ) Element of K19( the carrier of (One-Point_Compactification b1 : ( ( ) ( ) TopStruct ) ) : ( ( strict ) ( non empty strict ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) ;

registration
let X be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster One-Point_Compactification X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( strict ) ( non empty strict ) TopStruct ) -> strict TopSpace-like ;
end;

theorem :: COMPACT1:5
for X being ( ( ) ( ) TopStruct ) holds X : ( ( ) ( ) TopStruct ) is ( ( ) ( ) SubSpace of One-Point_Compactification X : ( ( ) ( ) TopStruct ) : ( ( strict ) ( non empty strict ) TopStruct ) ) ;

registration
let X be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster One-Point_Compactification X : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) -> strict compact ;
end;

theorem :: COMPACT1:6
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( ( X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is Hausdorff & X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally-compact ) iff One-Point_Compactification X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( strict ) ( non empty strict TopSpace-like compact locally-compact ) TopStruct ) is Hausdorff ) ;

theorem :: COMPACT1:7
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
( not X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is compact iff ex X9 being ( ( ) ( ) Subset of ) st
( X9 : ( ( ) ( ) Subset of ) = [#] X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty non proper open closed dense non boundary ) Element of K19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) & X9 : ( ( ) ( ) Subset of ) is dense ) ) ;

theorem :: COMPACT1:8
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st not X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is compact holds
incl (X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,(One-Point_Compactification X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty strict TopSpace-like compact locally-compact ) TopStruct ) ) : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (One-Point_Compactification b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty strict TopSpace-like compact locally-compact ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (One-Point_Compactification b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty strict TopSpace-like compact locally-compact ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (One-Point_Compactification b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty strict TopSpace-like compact locally-compact ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (One-Point_Compactification b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( strict ) ( non empty strict TopSpace-like compact locally-compact ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty V21() V23() V24() ) set ) ) is compactification ;