:: 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 b₁ being Subset of X st b₁ is empty holds
b₁ 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 b₁ being Subset of T st b₁ 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 b₁ being non empty TopSpace st b₁ is liminally-compact holds
b₁ is locally-compact

proof end;

end;

registration

cluster non empty TopSpace-like regular locally-compact -> non empty regular liminally-compact for TopStruct ;

coherence
for b₁ being non empty regular TopSpace st b₁ is locally-compact holds
b₁ is liminally-compact

proof end;

end;

registration

cluster non empty TopSpace-like locally-relatively-compact -> non empty locally-closed/compact for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is locally-relatively-compact holds
b₁ 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 b₁ being non empty TopSpace st b₁ is locally-closed/compact holds
b₁ is locally-relatively-compact

proof end;

end;

registration

cluster non empty TopSpace-like locally-relatively-compact -> non empty locally-compact for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is locally-relatively-compact holds
b₁ 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 b₁ being non empty Hausdorff TopSpace st b₁ is locally-compact holds
b₁ is locally-relatively-compact

proof end;

end;

registration

cluster non empty TopSpace-like compact -> non empty locally-compact for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is compact holds
b₁ is locally-compact

proof end;

end;

registration

cluster non empty TopSpace-like discrete -> non empty locally-compact for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is discrete holds
b₁ is locally-compact

proof end;

end;

registration

cluster non empty TopSpace-like discrete for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is discrete & not b₁ 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 b₁ being Function of X,Y st b₁ is compactification holds
b₁ 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 b₁ being strict TopStruct st
( the carrier of b₁ = succ ([#] X) & the topology of b₁ = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } )

proof end;

uniqueness
for b₁, b₂ being strict TopStruct st the carrier of b₁ = succ ([#] X) & the topology of b₁ = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } & the carrier of b<sub>2</sub> = succ ([#] X) & the topology of b<sub>2</sub> = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } holds
b₁ = b₂ ;

end;

:: deftheorem Def9 defines One-Point_Compactification COMPACT1:def 9 :
for X being TopStruct
for b₂ being strict TopStruct holds
( b₂ = One-Point_Compactification X iff ( the carrier of b₂ = succ ([#] X) & the topology of b₂ = 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;