:: Alexandroff One Point Compactification
:: by Czeslaw Bylinski
::
:: Received August 13, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users


definition
let X be TopSpace;
let P be Subset-Family of X;
attr P is compact means :: COMPACT1:def 1
 for U being Subset of X st U in P holds
U is compact ;
end;

:: deftheorem 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 );

definition
let X be TopSpace;
let U be Subset of X;
attr U is relatively-compact means :Def2: :: COMPACT1:def 2
 Cl U is compact ;
end;

:: 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 );

registration
let X be TopSpace;
cluster empty -> relatively-compact for Element of K19( the carrier of X);
coherence
for b1 being Subset of X st b1 is empty holds
b1 is relatively-compact by PRE_TOPC:22;
end;

registration
let T be TopSpace;
cluster relatively-compact for Element of K19( the carrier of T);
existence
ex b1 being Subset of T st b1 is relatively-compact
proof end;
end;

registration
let X be TopSpace;
let U be relatively-compact Subset of X;
cluster Cl U -> compact ;
coherence
Cl U is compact by Def2;
end;

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

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

:: see WAYBEL_3:def 9
definition
let X be non empty TopSpace;
redefine attr X is locally-compact means :Def3: :: COMPACT1:def 3
 for x being Point of X ex B being basis of x st B is compact ;
compatibility
( X is liminally-compact iff for x being Point of X ex B being basis of x st B is compact )
proof end;
end;

:: 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 );

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

:: deftheorem 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 );

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

:: deftheorem 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 ) );

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

:: 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 );

registration
cluster non empty TopSpace-like liminally-compact -> non empty locally-compact for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is liminally-compact holds
b1 is locally-compact
proof end;
end;

registration
cluster non empty TopSpace-like regular locally-compact -> non empty regular liminally-compact for TopStruct ;
coherence
for b1 being non empty regular TopSpace st b1 is locally-compact holds
b1 is liminally-compact
proof end;
end;

registration
cluster non empty TopSpace-like locally-relatively-compact -> non empty locally-closed/compact for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is locally-relatively-compact holds
b1 is locally-closed/compact
proof end;
end;

registration
cluster non empty TopSpace-like locally-closed/compact -> non empty locally-relatively-compact for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is locally-closed/compact holds
b1 is locally-relatively-compact
proof end;
end;

registration
cluster non empty TopSpace-like locally-relatively-compact -> non empty locally-compact for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is locally-relatively-compact holds
b1 is locally-compact
proof end;
end;

registration
cluster non empty TopSpace-like Hausdorff locally-compact -> non empty Hausdorff locally-relatively-compact for TopStruct ;
coherence
for b1 being non empty Hausdorff TopSpace st b1 is locally-compact holds
b1 is locally-relatively-compact
proof end;
end;

registration
cluster non empty TopSpace-like compact -> non empty locally-compact for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is compact holds
b1 is locally-compact
proof end;
end;

registration
cluster non empty TopSpace-like discrete -> non empty locally-compact for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is discrete holds
b1 is locally-compact
proof end;
end;

registration
cluster non empty TopSpace-like discrete for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is discrete & not b1 is empty )
proof end;
end;

registration
let X be non empty locally-compact TopSpace;
let C be non empty closed Subset of X;
cluster X | C -> locally-compact ;
coherence
X | C is locally-compact
proof end;
end;

registration
let X be non empty regular locally-compact TopSpace;
let P be non empty open Subset of X;
cluster X | P -> locally-compact ;
coherence
X | P is locally-compact
proof end;
end;

theorem :: COMPACT1:1
for X being non empty Hausdorff TopSpace
for E being non empty Subset of X st X | E is dense & X | E is locally-compact holds
X | E is open
proof end;

theorem Th2: :: COMPACT1:2
for X, Y being TopSpace
for A being Subset of X st [#] X c= [#] Y holds
(incl (X,Y)) .: A = A
proof end;

definition
let X, Y be TopSpace;
let f be Function of X,Y;
attr f is embedding means :: COMPACT1:def 7
 ex h being Function of X,(Y | (rng f)) st
( h = f & h is being_homeomorphism );
end;

:: 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: :: COMPACT1:3
for X, Y being TopSpace st [#] X c= [#] Y & ex Xy being Subset of Y st
( Xy = [#] X & the topology of (Y | Xy) = the topology of X ) holds
incl (X,Y) is embedding
proof end;

definition
let X, Y be TopSpace;
let h be Function of X,Y;
attr h is compactification means :: COMPACT1:def 8
( h is embedding & Y is compact & h .: ([#] X) is dense );
end;

:: deftheorem 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 ) );

registration
let X, Y be TopSpace;
cluster Function-like V18( the carrier of X, the carrier of Y) compactification -> embedding for Element of K19(K20( the carrier of X, the carrier of Y));
coherence
for b1 being Function of X,Y st b1 is compactification holds
b1 is embedding ;
end;

definition
let X be TopStruct ;
func One-Point_Compactification X -> strict TopStruct means :Def9: :: COMPACT1:def 9
( the carrier of it = succ ([#] X) & the topology of it = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } );
existence
ex b1 being strict TopStruct st
( the carrier of b1 = succ ([#] X) & the topology of b1 = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } )
proof end;
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = succ ([#] X) & the topology of b1 = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } & 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 ) } holds
b1 = b2 ;
end;

:: 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 ) } ) );

registration
let X be TopStruct ;
cluster One-Point_Compactification X -> non empty strict ;
coherence
not One-Point_Compactification X is empty
proof end;
end;

theorem Th4: :: COMPACT1:4
for X being TopStruct holds [#] X c= [#] (One-Point_Compactification X)
proof end;

registration
let X be TopSpace;
cluster One-Point_Compactification X -> strict TopSpace-like ;
coherence
One-Point_Compactification X is TopSpace-like
proof end;
end;

theorem Th5: :: COMPACT1:5
for X being TopStruct holds X is SubSpace of One-Point_Compactification X
proof end;

registration
let X be TopSpace;
cluster One-Point_Compactification X -> strict compact ;
coherence
One-Point_Compactification X is compact
proof end;
end;

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

theorem Th7: :: COMPACT1:7
for X being non empty TopSpace holds
( not X is compact iff ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) )
proof end;

theorem :: COMPACT1:8
for X being non empty TopSpace st not X is compact holds
incl (X,(One-Point_Compactification X)) is compactification
proof end;