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


begin

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

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

definition
let X be TopSpace;
let U be Subset of X;
attrU 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
proofend;
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
proofend;
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 )
proofend;
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;
attrX is locally-relatively-compact  means :Def4: :: COMPACT1:def 4
 for x being Point of X ex U being a_neighborhood of x st U is relatively-compact ;
end;

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

definition
let X be non empty TopSpace;
attrX is locally-closed/compact  means :Def5: :: 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 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 ) );

definition
let X be non empty TopSpace;
attrX 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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
end;

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

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

registration
let X be non empty regular locally-compact TopSpace;
let P be non empty open Subset of X;
clusterX | P ->  locally-compact ;
coherence
 X | P is locally-compact
proofend;
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
proofend;

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
proofend;

definition
let X, Y be TopSpace;
let f be Function of X,Y;
attrf 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
proofend;

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

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

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 by Def8;
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 )  }  )
proofend;
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
proofend;
end;

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

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

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

registration
let X be TopSpace;
cluster One-Point_Compactification X ->  strict compact ;
coherence
 One-Point_Compactification X is compact
proofend;
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 )
proofend;

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

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