:: by Czeslaw Bylinski

::

:: Received August 13, 2007

:: Copyright (c) 2007-2018 Association of Mizar Users

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

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

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;

coherence

for b_{1} being Subset of X st b_{1} is empty holds

b_{1} is relatively-compact
by PRE_TOPC:22;

end;
coherence

for b

b

registration
end;

registration
end;

:: see WAYBEL_3:def 9

definition

let X be non empty TopSpace;

( X is liminally-compact iff for x being Point of X ex B being basis of x st B is compact )

end;
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 for x being Point of X ex B being basis of x st B is compact ;

( X is liminally-compact iff for x being Point of X ex B being basis of x st B is compact )

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

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;

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

for x being Point of X ex U being a_neighborhood of x st U is relatively-compact ;

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

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;

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

for x being Point of X ex U being a_neighborhood of x st

( U is closed & U is compact );

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

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;

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

for x being Point of X ex U being a_neighborhood of x st 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 );

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

coherence

for b_{1} being non empty TopSpace st b_{1} is liminally-compact holds

b_{1} is locally-compact

end;
for b

b

proof end;

registration

for b_{1} being non empty regular TopSpace st b_{1} is locally-compact holds

b_{1} is liminally-compact
end;

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

coherence for b

b

proof end;

registration

for b_{1} being non empty TopSpace st b_{1} is locally-relatively-compact holds

b_{1} is locally-closed/compact
end;

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

coherence for b

b

proof end;

registration

for b_{1} being non empty TopSpace st b_{1} is locally-closed/compact holds

b_{1} is locally-relatively-compact
end;

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

coherence for b

b

proof end;

registration

for b_{1} being non empty TopSpace st b_{1} is locally-relatively-compact holds

b_{1} is locally-compact
end;

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

coherence for b

b

proof end;

registration

for b_{1} being non empty Hausdorff TopSpace st b_{1} is locally-compact holds

b_{1} is locally-relatively-compact
end;

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

coherence for b

b

proof end;

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is compact holds

b_{1} is locally-compact

end;
for b

b

proof end;

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is discrete holds

b_{1} is locally-compact

end;
for b

b

proof end;

registration
end;

registration

let X be non empty locally-compact TopSpace;

let C be non empty closed Subset of X;

coherence

X | C is locally-compact

end;
let C be non empty closed Subset of X;

coherence

X | C is locally-compact

proof end;

registration

let X be non empty regular locally-compact TopSpace;

let P be non empty open Subset of X;

coherence

X | P is locally-compact

end;
let P be non empty open Subset of X;

coherence

X | P is locally-compact

proof 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

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;

definition

let X, Y be TopSpace;

let f be Function of X,Y;

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

ex h being Function of X,(Y | (rng f)) st

( h = f & h is being_homeomorphism );

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

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

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

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

( h is embedding & Y is compact & h .: ([#] X) is dense );

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

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;

for b_{1} being Function of X,Y st b_{1} is compactification holds

b_{1} is embedding
;

end;
cluster Function-like V18( the carrier of X, the carrier of Y) compactification -> embedding for Function of ,;

coherence for b

b

definition

let X be TopStruct ;

ex b_{1} being strict TopStruct st

( the carrier of b_{1} = succ ([#] X) & the topology of b_{1} = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } )

for b_{1}, b_{2} being strict TopStruct st the carrier of b_{1} = succ ([#] X) & the topology of b_{1} = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } & the carrier of b_{2} = succ ([#] X) & the topology of b_{2} = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } holds

b_{1} = b_{2}
;

end;
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 ( 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 ) } );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines One-Point_Compactification COMPACT1:def 9 :

for X being TopStruct

for b_{2} being strict TopStruct holds

( b_{2} = One-Point_Compactification X iff ( the carrier of b_{2} = succ ([#] X) & the topology of b_{2} = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) );

for X being TopStruct

for b

( b

registration
end;

registration
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 )

( ( 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 ) )

( 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

incl (X,(One-Point_Compactification X)) is compactification

proof end;