:: COMPACT1 semantic presentation
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
proof
let S be Subset of X; ::_thesis: ( S is empty implies S is relatively-compact )
assume A1: S is empty ; ::_thesis: S is relatively-compact
then Cl S = S by PRE_TOPC:22;
hence S is relatively-compact by A1, Def2; ::_thesis: verum
end;
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
take {} T ; ::_thesis: {} T is relatively-compact
thus {} T is relatively-compact ; ::_thesis: verum
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;
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
hereby ::_thesis: ( ( for x being Point of X ex B being basis of x st B is compact ) implies X is liminally-compact )
assume A1: X is liminally-compact ; ::_thesis: for x being Point of X ex B being basis of x st B is compact
let x be Point of X; ::_thesis: ex B being basis of x st B is compact
set B = { Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V ) } ;
{ Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V ) } c= bool ([#] X)
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in { Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V ) } or A in bool ([#] X) )
assume A in { Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V ) } ; ::_thesis: A in bool ([#] X)
then ex Q being a_neighborhood of x st
( A = Q & Q is compact & ex V being a_neighborhood of x st Q c= V ) ;
hence A in bool ([#] X) ; ::_thesis: verum
end;
then reconsider B = { Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V ) } as Subset-Family of X ;
A2: B is basis of x
proof
let V be a_neighborhood of x; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of x st
( b1 in B & b1 c= V )
x in Int V by CONNSP_2:def_1;
then consider Q being Subset of X such that
A3: x in Int Q and
A4: Q c= Int V and
A5: Q is compact by A1, WAYBEL_3:def_9;
reconsider Q = Q as a_neighborhood of x by A3, CONNSP_2:def_1;
take Q ; ::_thesis: ( Q in B & Q c= V )
Int V c= V by TOPS_1:16;
hence ( Q in B & Q c= V ) by A4, A5, XBOOLE_1:1; ::_thesis: verum
end;
B is compact
proof
let U be Subset of X; :: according to COMPACT1:def_1 ::_thesis: ( U in B implies U is compact )
assume U in B ; ::_thesis: U is compact
then ex Q being a_neighborhood of x st
( U = Q & Q is compact & ex V being a_neighborhood of x st Q c= V ) ;
hence U is compact ; ::_thesis: verum
end;
hence ex B being basis of x st B is compact by A2; ::_thesis: verum
end;
assume A6: for x being Point of X ex B being basis of x st B is compact ; ::_thesis: X is liminally-compact
let x be Point of X; :: according to WAYBEL_3:def_9 ::_thesis: for b1 being Element of K19( the carrier of X) holds
( not x in b1 or not b1 is open or ex b2 being Element of K19( the carrier of X) st
( x in Int b2 & b2 c= b1 & b2 is compact ) )
let P be Subset of X; ::_thesis: ( not x in P or not P is open or ex b1 being Element of K19( the carrier of X) st
( x in Int b1 & b1 c= P & b1 is compact ) )
assume that
A7: x in P and
A8: P is open ; ::_thesis: ex b1 being Element of K19( the carrier of X) st
( x in Int b1 & b1 c= P & b1 is compact )
consider B being basis of x such that
A9: B is compact by A6;
x in Int P by A7, A8, TOPS_1:23;
then consider Q being Subset of X such that
A10: Q in B and
A11: x in Int Q and
A12: Q c= P by YELLOW13:def_1;
take Q ; ::_thesis: ( x in Int Q & Q c= P & Q is compact )
thus ( x in Int Q & Q c= P ) by A11, A12; ::_thesis: Q is compact
thus Q is compact by A9, A10, Def1; ::_thesis: verum
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;
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
proof
let X be non empty TopSpace; ::_thesis: ( X is liminally-compact implies X is locally-compact )
assume A1: X is liminally-compact ; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
consider B being basis of x such that
A2: B is compact by A1, Def3;
set V = the a_neighborhood of x;
consider Y being a_neighborhood of x such that
A3: Y in B and
Y c= the a_neighborhood of x by YELLOW13:def_2;
Y is compact by A2, A3, Def1;
hence ex U being a_neighborhood of x st U is compact ; ::_thesis: verum
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
let X be non empty regular TopSpace; ::_thesis: ( X is locally-compact implies X is liminally-compact )
assume A1: X is locally-compact ; ::_thesis: X is liminally-compact
let x be Point of X; :: according to COMPACT1:def_3 ::_thesis: ex B being basis of x st B is compact
set B = { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } ;
{ Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } c= bool ([#] X)
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } or A in bool ([#] X) )
assume A in { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } ; ::_thesis: A in bool ([#] X)
then ex Q being a_neighborhood of x st
( A = Q & Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) ;
hence A in bool ([#] X) ; ::_thesis: verum
end;
then reconsider B = { Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) } as Subset-Family of X ;
A2: B is basis of x
proof
let V be a_neighborhood of x; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of x st
( b1 in B & b1 c= V )
A3: x in Int V by CONNSP_2:def_1;
consider W being a_neighborhood of x such that
A4: W is compact by A1, Def6;
x in Int W by CONNSP_2:def_1;
then x in (Int V) /\ (Int W) by A3, XBOOLE_0:def_4;
then x in Int (V /\ W) by TOPS_1:17;
then consider Q being Subset of X such that
A5: Q is closed and
A6: Q c= V /\ W and
A7: x in Int Q by YELLOW_8:27;
reconsider Q = Q as a_neighborhood of x by A7, CONNSP_2:def_1;
take Q ; ::_thesis: ( Q in B & Q c= V )
V /\ W c= W by XBOOLE_1:17;
then Q is compact by A4, A5, A6, COMPTS_1:9, XBOOLE_1:1;
hence Q in B by A6; ::_thesis: Q c= V
V /\ W c= V by XBOOLE_1:17;
hence Q c= V by A6, XBOOLE_1:1; ::_thesis: verum
end;
B is compact
proof
let U be Subset of X; :: according to COMPACT1:def_1 ::_thesis: ( U in B implies U is compact )
assume U in B ; ::_thesis: U is compact
then ex Q being a_neighborhood of x st
( U = Q & Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) ;
hence U is compact ; ::_thesis: verum
end;
hence ex B being basis of x st B is compact by A2; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: ( X is locally-relatively-compact implies X is locally-closed/compact )
assume A1: X is locally-relatively-compact ; ::_thesis: X is locally-closed/compact
let x be Point of X; :: according to COMPACT1:def_5 ::_thesis: ex U being a_neighborhood of x st
( U is closed & U is compact )
consider U being a_neighborhood of x such that
A2: U is relatively-compact by A1, Def4;
A3: x in Int U by CONNSP_2:def_1;
Int U c= Int (Cl U) by PRE_TOPC:18, TOPS_1:19;
then Cl U is a_neighborhood of x by A3, CONNSP_2:def_1;
hence ex U being a_neighborhood of x st
( U is closed & U is compact ) by A2; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: ( X is locally-closed/compact implies X is locally-relatively-compact )
assume A1: X is locally-closed/compact ; ::_thesis: X is locally-relatively-compact
let x be Point of X; :: according to COMPACT1:def_4 ::_thesis: ex U being a_neighborhood of x st U is relatively-compact
consider U being a_neighborhood of x such that
A2: ( U is closed & U is compact ) by A1, Def5;
Cl U = U by A2, PRE_TOPC:22;
then U is relatively-compact by A2, Def2;
hence ex U being a_neighborhood of x st U is relatively-compact ; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: ( X is locally-relatively-compact implies X is locally-compact )
assume A1: X is locally-relatively-compact ; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
consider Y being a_neighborhood of x such that
A2: Y is relatively-compact by A1, Def4;
A3: x in Int Y by CONNSP_2:def_1;
Int Y c= Int (Cl Y) by PRE_TOPC:18, TOPS_1:19;
then Cl Y is a_neighborhood of x by A3, CONNSP_2:def_1;
hence ex U being a_neighborhood of x st U is compact by A2; ::_thesis: verum
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
let X be non empty Hausdorff TopSpace; ::_thesis: ( X is locally-compact implies X is locally-relatively-compact )
assume A1: X is locally-compact ; ::_thesis: X is locally-relatively-compact
let x be Point of X; :: according to COMPACT1:def_4 ::_thesis: ex U being a_neighborhood of x st U is relatively-compact
consider U being a_neighborhood of x such that
A2: U is compact by A1, Def6;
Cl U = U by A2, PRE_TOPC:22;
then U is relatively-compact by A2, Def2;
hence ex U being a_neighborhood of x st U is relatively-compact ; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: ( X is compact implies X is locally-compact )
set Y = [#] X;
assume A1: X is compact ; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
Int ([#] X) = [#] X by TOPS_1:23;
then [#] X is a_neighborhood of x by CONNSP_2:def_1;
hence ex U being a_neighborhood of x st U is compact by A1; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: ( X is discrete implies X is locally-compact )
assume A1: X is discrete ; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
set Y = {x};
{x} is open by A1, TDLAT_3:15;
then Int {x} = {x} by TOPS_1:23;
then x in Int {x} by TARSKI:def_1;
then reconsider Y = {x} as a_neighborhood of x by CONNSP_2:def_1;
Y is compact ;
hence ex U being a_neighborhood of x st U is compact ; ::_thesis: verum
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
set X = the non empty discrete TopSpace;
take the non empty discrete TopSpace ; ::_thesis: ( the non empty discrete TopSpace is discrete & not the non empty discrete TopSpace is empty )
thus ( the non empty discrete TopSpace is discrete & not the non empty discrete TopSpace is empty ) ; ::_thesis: verum
end;
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
proof
let x be Point of (X | C); :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
reconsider xx = x as Point of X by PRE_TOPC:25;
consider K being a_neighborhood of xx such that
A1: K is compact by Def6;
A2: [#] (X | C) = C by PRE_TOPC:8;
then reconsider KC = K /\ C as Subset of (X | C) by XBOOLE_1:17;
reconsider KC = KC as a_neighborhood of x by A2, TOPMETR:5;
take KC ; ::_thesis: KC is compact
A3: xx in Int K by CONNSP_2:def_1;
A4: [#] (X | K) = K by PRE_TOPC:8;
then reconsider KK = K /\ C as Subset of (X | K) by XBOOLE_1:17;
A5: KK is closed by A4, PRE_TOPC:13;
A6: Int K c= K by TOPS_1:16;
then A7: x in KC by A2, A3, XBOOLE_0:def_4;
X | K is compact by A1, A6, A3, COMPTS_1:3;
then KK is compact by A5, COMPTS_1:8;
then (X | K) | KK is compact by A7, COMPTS_1:3;
then X | (K /\ C) is compact by PRE_TOPC:7, XBOOLE_1:17;
then (X | C) | KC is compact by PRE_TOPC:7, XBOOLE_1:17;
hence KC is compact by A7, COMPTS_1:3; ::_thesis: verum
end;
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
proof
let x be Point of (X | P); :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
reconsider xx = x as Point of X by PRE_TOPC:25;
consider B being basis of xx such that
A1: B is compact by Def3;
A2: [#] (X | P) = P by PRE_TOPC:8;
then xx in P ;
then xx in Int P by TOPS_1:23;
then P is a_neighborhood of xx by CONNSP_2:def_1;
then consider K being a_neighborhood of xx such that
A3: K in B and
A4: K c= P by YELLOW13:def_2;
reconsider KK = K as Subset of (X | P) by A4, PRE_TOPC:8;
K is compact by A1, A3, Def1;
then A5: KK is compact by A2, COMPTS_1:2;
A6: Int K c= K by TOPS_1:16;
xx in Int K by CONNSP_2:def_1;
then A7: x in K by A6;
KK = K /\ P by A4, XBOOLE_1:28;
then KK is a_neighborhood of x by A4, A7, TOPMETR:5;
hence ex U being a_neighborhood of x st U is compact by A5; ::_thesis: verum
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
let X be non empty Hausdorff TopSpace; ::_thesis: for E being non empty Subset of X st X | E is dense & X | E is locally-compact holds
X | E is open
let E be non empty Subset of X; ::_thesis: ( X | E is dense & X | E is locally-compact implies X | E is open )
assume A1: ( X | E is dense & X | E is locally-compact ) ; ::_thesis: X | E is open
A2: [#] (X | E) = E by PRE_TOPC:8;
Int E = E
proof
thus Int E c= E by TOPS_1:16; :: according to XBOOLE_0:def_10 ::_thesis: E c= Int E
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in E or a in Int E )
assume A3: a in E ; ::_thesis: a in Int E
then reconsider x = a as Point of X ;
reconsider xx = x as Point of (X | E) by A3, PRE_TOPC:8;
set UE = { G where G is Subset of X : ( G is open & G c= E ) } ;
consider K being a_neighborhood of xx such that
A4: K is compact by A1, Def6;
reconsider KK = K as Subset of X by A2, XBOOLE_1:1;
A5: K c= [#] (X | E) ;
Int K in the topology of (X | E) by PRE_TOPC:def_2;
then consider G being Subset of X such that
A6: G in the topology of X and
A7: Int K = G /\ E by A2, PRE_TOPC:def_4;
A8: G is open by A6, PRE_TOPC:def_2;
for P being Subset of (X | E) st P = KK holds
P is compact by A4;
then KK is compact by A5, COMPTS_1:2;
then A9: Cl (G /\ E) c= KK by A7, TOPS_1:5, TOPS_1:16;
E is dense by A1, A2, TEX_3:def_1;
then A10: Cl (G /\ E) = Cl G by A8, TOPS_1:46;
G c= Cl G by PRE_TOPC:18;
then G c= K by A10, A9, XBOOLE_1:1;
then G c= E by A2, XBOOLE_1:1;
then A11: G in { G where G is Subset of X : ( G is open & G c= E ) } by A8;
A12: xx in Int K by CONNSP_2:def_1;
Int K c= G by A7, XBOOLE_1:17;
then a in union { G where G is Subset of X : ( G is open & G c= E ) } by A12, A11, TARSKI:def_4;
hence a in Int E by TEX_4:3; ::_thesis: verum
end;
hence X | E is open by A2, TSEP_1:16; ::_thesis: verum
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
let X, Y be TopSpace; ::_thesis: for A being Subset of X st [#] X c= [#] Y holds
(incl (X,Y)) .: A = A
let A be Subset of X; ::_thesis: ( [#] X c= [#] Y implies (incl (X,Y)) .: A = A )
assume [#] X c= [#] Y ; ::_thesis: (incl (X,Y)) .: A = A
hence (incl (X,Y)) .: A = (id ([#] X)) .: A by YELLOW_9:def_1
.= A by FUNCT_1:92 ;
::_thesis: verum
end;
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
proof
let X, Y be TopSpace; ::_thesis: ( [#] X c= [#] Y & ex Xy being Subset of Y st
( Xy = [#] X & the topology of (Y | Xy) = the topology of X ) implies incl (X,Y) is embedding )
assume A1: [#] X c= [#] Y ; ::_thesis: ( for Xy being Subset of Y holds
( not Xy = [#] X or not the topology of (Y | Xy) = the topology of X ) or incl (X,Y) is embedding )
A2: incl (X,Y) = id X by A1, YELLOW_9:def_1;
set YY = Y | (rng (incl (X,Y)));
A3: [#] (Y | (rng (incl (X,Y)))) = rng (incl (X,Y)) by PRE_TOPC:def_5;
A4: ( [#] Y = {} implies [#] X = {} ) by A1;
then reconsider h = incl (X,Y) as Function of X,(Y | (rng (incl (X,Y)))) by A3, FUNCT_2:6;
set f = id X;
given Xy being Subset of Y such that A5: Xy = [#] X and
A6: the topology of (Y | Xy) = the topology of X ; ::_thesis: incl (X,Y) is embedding
A7: for P being Subset of X st P is open holds
(h ") " P is open
proof
let P be Subset of X; ::_thesis: ( P is open implies (h ") " P is open )
reconsider Q = P as Subset of (Y | (rng (incl (X,Y)))) by A2, A3, RELAT_1:45;
assume P is open ; ::_thesis: (h ") " P is open
then A8: P in the topology of X by PRE_TOPC:def_2;
(h ") " P = h .: Q by A2, A3, TOPS_2:54
.= Q by A2, FUNCT_1:92 ;
hence (h ") " P in the topology of (Y | (rng (incl (X,Y)))) by A5, A6, A2, A8, RELAT_1:45; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
A9: ( [#] X = {} implies [#] X = {} ) ;
A10: for P being Subset of (Y | (rng (incl (X,Y)))) st P is open holds
h " P is open
proof
let P be Subset of (Y | (rng (incl (X,Y)))); ::_thesis: ( P is open implies h " P is open )
reconsider Q = P as Subset of X by A2, A3, RELAT_1:45;
assume P is open ; ::_thesis: h " P is open
then P in the topology of (Y | (rng (incl (X,Y)))) by PRE_TOPC:def_2;
then Q in the topology of X by A5, A6, A2, RELAT_1:45;
then Q is open by PRE_TOPC:def_2;
then (id X) " Q is open by A9, TOPS_2:43;
then (id X) " Q in the topology of X by PRE_TOPC:def_2;
hence h " P in the topology of X by A1, YELLOW_9:def_1; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
take h ; :: according to COMPACT1:def_7 ::_thesis: ( h = incl (X,Y) & h is being_homeomorphism )
thus h = incl (X,Y) ; ::_thesis: h is being_homeomorphism
thus ( dom h = [#] X & rng h = [#] (Y | (rng (incl (X,Y)))) ) by A4, FUNCT_2:def_1, PRE_TOPC:def_5; :: according to TOPS_2:def_5 ::_thesis: ( h is one-to-one & h is continuous & h " is continuous )
thus h is one-to-one by A2; ::_thesis: ( h is continuous & h " is continuous )
( [#] (Y | (rng (incl (X,Y)))) = {} implies [#] X = {} ) by A2, A3;
hence h is continuous by A10, TOPS_2:43; ::_thesis: h " is continuous
( [#] X = {} implies [#] (Y | (rng (incl (X,Y)))) = {} ) ;
hence h " is continuous by A7, TOPS_2:43; ::_thesis: verum
end;
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 ) } )
proof
set T = succ ([#] X);
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
set O = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } c= bool (succ ([#] X))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } or a in bool (succ ([#] X)) )
A1: now__::_thesis:_(_a_in__{__(U_\/_{([#]_X)})_where_U_is_Subset_of_X_:_(_U_is_open_&_U_`_is_compact_)__}__implies_a_c=_succ_([#]_X)_)
assume a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: a c= succ ([#] X)
then consider U being Subset of X such that
A2: a = U \/ {([#] X)} and
U is open and
U ` is compact ;
thus a c= succ ([#] X) ::_thesis: verum
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in a or A in succ ([#] X) )
assume A in a ; ::_thesis: A in succ ([#] X)
then ( A in U or A in {([#] X)} ) by A2, XBOOLE_0:def_3;
hence A in succ ([#] X) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
assume a in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: a in bool (succ ([#] X))
then ( a in the topology of X or a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by XBOOLE_0:def_3;
then a is Subset of (succ ([#] X)) by A1, XBOOLE_1:10;
hence a in bool (succ ([#] X)) ; ::_thesis: verum
end;
then reconsider O = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } as Subset-Family of (succ ([#] X)) ;
set Y = TopStruct(# (succ ([#] X)),O #);
not TopStruct(# (succ ([#] X)),O #) is empty ;
hence 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 ) } ) ; ::_thesis: verum
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
the carrier of (One-Point_Compactification X) = succ ([#] X) by Def9;
hence not One-Point_Compactification X is empty ; ::_thesis: verum
end;
end;
theorem Th4: :: COMPACT1:4
for X being TopStruct holds [#] X c= [#] (One-Point_Compactification X)
proof
let X be TopStruct ; ::_thesis: [#] X c= [#] (One-Point_Compactification X)
[#] (One-Point_Compactification X) = succ ([#] X) by Def9;
hence [#] X c= [#] (One-Point_Compactification X) by XBOOLE_1:7; ::_thesis: verum
end;
registration
let X be TopSpace;
cluster One-Point_Compactification X -> strict TopSpace-like ;
coherence
One-Point_Compactification X is TopSpace-like
proof
set Y = One-Point_Compactification X;
set T = succ ([#] X);
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
A1: not [#] X in [#] X ;
A2: the topology of (One-Point_Compactification X) = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
A3: [#] (One-Point_Compactification X) = succ ([#] X) by Def9;
One-Point_Compactification X is TopSpace-like
proof
([#] X) ` = (({} X) `) `
.= {} X ;
then succ ([#] X) in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
hence the carrier of (One-Point_Compactification X) in the topology of (One-Point_Compactification X) by A3, A2, XBOOLE_0:def_3; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K19(K19( the carrier of (One-Point_Compactification X))) holds
( not b1 c= the topology of (One-Point_Compactification X) or union b1 in the topology of (One-Point_Compactification X) ) ) & ( for b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not b2 in the topology of (One-Point_Compactification X) or b1 /\ b2 in the topology of (One-Point_Compactification X) ) ) )
hereby ::_thesis: for b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not b2 in the topology of (One-Point_Compactification X) or b1 /\ b2 in the topology of (One-Point_Compactification X) )
let a be Subset-Family of (One-Point_Compactification X); ::_thesis: ( a c= the topology of (One-Point_Compactification X) implies union b1 in the topology of (One-Point_Compactification X) )
A4: not [#] X in [#] X ;
set ua = { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } ;
A5: { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } c= the topology of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } or x in the topology of X )
assume x in { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } ; ::_thesis: x in the topology of X
then ex U being Subset of X st
( x = U & U is open & ( U in a or U \/ {([#] X)} in a ) ) ;
hence x in the topology of X by PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider ua = { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } as Subset-Family of X by XBOOLE_1:1;
union ua in the topology of X by A5, PRE_TOPC:def_1;
then A6: union ua is open by PRE_TOPC:def_2;
assume A7: a c= the topology of (One-Point_Compactification X) ; ::_thesis: union b1 in the topology of (One-Point_Compactification X)
A8: union ua = (union a) \ {([#] X)}
proof
thus union ua c= (union a) \ {([#] X)} :: according to XBOOLE_0:def_10 ::_thesis: (union a) \ {([#] X)} c= union ua
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union ua or x in (union a) \ {([#] X)} )
assume x in union ua ; ::_thesis: x in (union a) \ {([#] X)}
then consider A being set such that
A9: x in A and
A10: A in ua by TARSKI:def_4;
consider U being Subset of X such that
A11: A = U and
U is open and
A12: ( U in a or U \/ {([#] X)} in a ) by A10;
A13: now__::_thesis:_x_in_union_a
percases ( U in a or U \/ {([#] X)} in a ) by A12;
suppose U in a ; ::_thesis: x in union a
hence x in union a by A9, A11, TARSKI:def_4; ::_thesis: verum
end;
supposeA14: U \/ {([#] X)} in a ; ::_thesis: x in union a
x in U \/ {([#] X)} by A9, A11, XBOOLE_0:def_3;
hence x in union a by A14, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
now__::_thesis:_not_x_in_{([#]_X)}
assume x in {([#] X)} ; ::_thesis: contradiction
then A15: x = [#] X by TARSKI:def_1;
x in [#] X by A9, A11;
hence contradiction by A15; ::_thesis: verum
end;
hence x in (union a) \ {([#] X)} by A13, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union a) \ {([#] X)} or x in union ua )
assume A16: x in (union a) \ {([#] X)} ; ::_thesis: x in union ua
then x in union a by XBOOLE_0:def_5;
then consider A being set such that
A17: x in A and
A18: A in a by TARSKI:def_4;
percases ( A in the topology of X or A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A2, A7, A18, XBOOLE_0:def_3;
supposeA19: A in the topology of X ; ::_thesis: x in union ua
then reconsider U = A as Subset of X ;
U is open by A19, PRE_TOPC:def_2;
then U in ua by A18;
hence x in union ua by A17, TARSKI:def_4; ::_thesis: verum
end;
suppose A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: x in union ua
then consider U being Subset of X such that
A20: A = U \/ {([#] X)} and
A21: U is open and
U ` is compact ;
A22: U in ua by A18, A20, A21;
not x in {([#] X)} by A16, XBOOLE_0:def_5;
then x in U by A17, A20, XBOOLE_0:def_3;
hence x in union ua by A22, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
percases ( [#] X in union a or not [#] X in union a ) ;
supposeA23: [#] X in union a ; ::_thesis: union b1 in the topology of (One-Point_Compactification X)
then consider A being set such that
A24: [#] X in A and
A25: A in a by TARSKI:def_4;
( A in the topology of X or A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A2, A7, A25, XBOOLE_0:def_3;
then consider U being Subset of X such that
A26: A = U \/ {([#] X)} and
U is open and
A27: U ` is compact by A4, A24;
A28: now__::_thesis:_not_[#]_X_in_U
assume [#] X in U ; ::_thesis: contradiction
then [#] X in [#] X ;
hence contradiction ; ::_thesis: verum
end;
A \ {([#] X)} = U \ {([#] X)} by A26, XBOOLE_1:40
.= U by A28, ZFMISC_1:57 ;
then U c= union ua by A8, A25, XBOOLE_1:33, ZFMISC_1:74;
then A29: (union ua) ` is compact by A6, A27, COMPTS_1:9, XBOOLE_1:34;
(union ua) \/ {([#] X)} = (union a) \/ {([#] X)} by A8, XBOOLE_1:39
.= union a by A23, ZFMISC_1:40 ;
then union a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A6, A29;
hence union a in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA30: not [#] X in union a ; ::_thesis: union b1 in the topology of (One-Point_Compactification X)
A31: a c= the topology of X
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in a or A in the topology of X )
assume A32: A in a ; ::_thesis: A in the topology of X
assume not A in the topology of X ; ::_thesis: contradiction
then A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A2, A7, A32, XBOOLE_0:def_3;
then A33: ex U being Subset of X st
( A = U \/ {([#] X)} & U is open & U ` is compact ) ;
[#] X in {([#] X)} by TARSKI:def_1;
then [#] X in A by A33, XBOOLE_0:def_3;
hence contradiction by A30, A32, TARSKI:def_4; ::_thesis: verum
end;
then a is Subset-Family of ([#] X) by XBOOLE_1:1;
then union a in the topology of X by A31, PRE_TOPC:def_1;
hence union a in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let a, b be Subset of (One-Point_Compactification X); ::_thesis: ( not a in the topology of (One-Point_Compactification X) or not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )
assume A34: a in the topology of (One-Point_Compactification X) ; ::_thesis: ( not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )
assume A35: b in the topology of (One-Point_Compactification X) ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
percases ( ( a in the topology of X & b in the topology of X ) or ( a in the topology of X & b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) or ( b in the topology of X & a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) or ( a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } & b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) ) by A2, A34, A35, XBOOLE_0:def_3;
suppose ( a in the topology of X & b in the topology of X ) ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
then a /\ b in the topology of X by PRE_TOPC:def_1;
hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
supposethat A36: a in the topology of X and
A37: b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
reconsider a9 = a as Subset of X by A36;
not [#] X in a9 by A1;
then {([#] X)} misses a9 by ZFMISC_1:50;
then a9 /\ {([#] X)} = {} X by XBOOLE_0:def_7;
then reconsider aX = a9 /\ {([#] X)} as open Subset of X ;
consider U being Subset of X such that
A38: b = U \/ {([#] X)} and
A39: U is open and
U ` is compact by A37;
a9 is open by A36, PRE_TOPC:def_2;
then reconsider aXU = a9 /\ U as open Subset of X by A39;
a /\ b = aXU \/ aX by A38, XBOOLE_1:23;
then a /\ b in the topology of X by PRE_TOPC:def_2;
hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
supposethat A40: b in the topology of X and
A41: a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
reconsider b9 = b as Subset of X by A40;
not [#] X in b9 by A1;
then {([#] X)} misses b9 by ZFMISC_1:50;
then b9 /\ {([#] X)} = {} X by XBOOLE_0:def_7;
then reconsider bX = b9 /\ {([#] X)} as open Subset of X ;
consider U being Subset of X such that
A42: a = U \/ {([#] X)} and
A43: U is open and
U ` is compact by A41;
b9 is open by A40, PRE_TOPC:def_2;
then reconsider bXUa = b9 /\ U as open Subset of X by A43;
a /\ b = bXUa \/ bX by A42, XBOOLE_1:23;
then a /\ b in the topology of X by PRE_TOPC:def_2;
hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
supposethat A44: a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } and
A45: b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
consider Ua being Subset of X such that
A46: a = Ua \/ {([#] X)} and
A47: Ua is open and
A48: Ua ` is compact by A44;
consider Ub being Subset of X such that
A49: b = Ub \/ {([#] X)} and
A50: Ub is open and
A51: Ub ` is compact by A45;
(Ua `) \/ (Ub `) is compact by A48, A51, COMPTS_1:10;
then A52: (Ua /\ Ub) ` is compact by XBOOLE_1:54;
a /\ b = (Ua /\ Ub) \/ {([#] X)} by A46, A49, XBOOLE_1:24;
then a /\ b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A47, A50, A52;
hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence One-Point_Compactification X is TopSpace-like ; ::_thesis: verum
end;
end;
theorem Th5: :: COMPACT1:5
for X being TopStruct holds X is SubSpace of One-Point_Compactification X
proof
let X be TopStruct ; ::_thesis: X is SubSpace of One-Point_Compactification X
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
thus A1: [#] X c= [#] (One-Point_Compactification X) by Th4; :: according to PRE_TOPC:def_4 ::_thesis: for b1 being Element of K19( the carrier of X) holds
( ( not b1 in the topology of X or ex b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b2 in the topology of (One-Point_Compactification X) & b1 = b2 /\ ([#] X) ) ) & ( for b2 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b2 in the topology of (One-Point_Compactification X) or not b1 = b2 /\ ([#] X) ) or b1 in the topology of X ) )
let P be Subset of X; ::_thesis: ( ( not P in the topology of X or ex b1 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 in the topology of (One-Point_Compactification X) & P = b1 /\ ([#] X) ) ) & ( for b1 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not P = b1 /\ ([#] X) ) or P in the topology of X ) )
A2: the topology of (One-Point_Compactification X) = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
hereby ::_thesis: ( for b1 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not P = b1 /\ ([#] X) ) or P in the topology of X )
reconsider Q = P as Subset of (One-Point_Compactification X) by A1, XBOOLE_1:1;
assume A3: P in the topology of X ; ::_thesis: ex Q being Subset of (One-Point_Compactification X) st
( Q in the topology of (One-Point_Compactification X) & P = Q /\ ([#] X) )
take Q = Q; ::_thesis: ( Q in the topology of (One-Point_Compactification X) & P = Q /\ ([#] X) )
thus Q in the topology of (One-Point_Compactification X) by A2, A3, XBOOLE_0:def_3; ::_thesis: P = Q /\ ([#] X)
thus P = Q /\ ([#] X) by XBOOLE_1:28; ::_thesis: verum
end;
given Q being Subset of (One-Point_Compactification X) such that A4: Q in the topology of (One-Point_Compactification X) and
A5: P = Q /\ ([#] X) ; ::_thesis: P in the topology of X
percases ( Q in the topology of X or Q in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A2, A4, XBOOLE_0:def_3;
suppose Q in the topology of X ; ::_thesis: P in the topology of X
hence P in the topology of X by A5, XBOOLE_1:28; ::_thesis: verum
end;
suppose Q in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: P in the topology of X
then consider U being Subset of X such that
A6: Q = U \/ {([#] X)} and
A7: U is open and
U ` is compact ;
not [#] X in [#] X ;
then {([#] X)} misses [#] X by ZFMISC_1:50;
then {([#] X)} /\ ([#] X) = {} by XBOOLE_0:def_7;
then P = (U /\ ([#] X)) \/ {} by A5, A6, XBOOLE_1:23
.= U by XBOOLE_1:28 ;
hence P in the topology of X by A7, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
registration
let X be TopSpace;
cluster One-Point_Compactification X -> strict compact ;
coherence
One-Point_Compactification X is compact
proof
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
let F be Subset-Family of (One-Point_Compactification X); :: according to COMPTS_1:def_1 ::_thesis: ( not F is Cover of the carrier of (One-Point_Compactification X) or not F is open or ex b1 being Element of K19(K19( the carrier of (One-Point_Compactification X))) st
( b1 c= F & b1 is Cover of the carrier of (One-Point_Compactification X) & b1 is finite ) )
assume that
A1: F is Cover of (One-Point_Compactification X) and
A2: F is open ; ::_thesis: ex b1 being Element of K19(K19( the carrier of (One-Point_Compactification X))) st
( b1 c= F & b1 is Cover of the carrier of (One-Point_Compactification X) & b1 is finite )
A3: [#] (One-Point_Compactification X) c= union F by A1, SETFAM_1:def_11;
set Fx = { U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } ;
{ U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } c= the topology of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } or x in the topology of X )
assume x in { U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } ; ::_thesis: x in the topology of X
then ex U being Subset of X st
( x = U & U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) ;
hence x in the topology of X by PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider Fx = { U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) } as Subset-Family of X by XBOOLE_1:1;
A4: Fx is open
proof
let P be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not P in Fx or P is open )
assume P in Fx ; ::_thesis: P is open
then ex U being Subset of X st
( P = U & U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) ;
hence P is open ; ::_thesis: verum
end;
[#] X in {([#] X)} by TARSKI:def_1;
then [#] X in succ ([#] X) by XBOOLE_0:def_3;
then [#] X in [#] (One-Point_Compactification X) by Def9;
then consider A being set such that
A5: [#] X in A and
A6: A in F by A3, TARSKI:def_4;
reconsider A = A as Subset of (One-Point_Compactification X) by A6;
A is open by A2, A6, TOPS_2:def_1;
then A in the topology of (One-Point_Compactification X) by PRE_TOPC:def_2;
then A7: A in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
not [#] X in [#] X ;
then not A in the topology of X by A5;
then A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A7, XBOOLE_0:def_3;
then consider U being Subset of X such that
A8: A = U \/ {([#] X)} and
U is open and
A9: U ` is compact ;
Fx is Cover of X
proof
let x be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not x in the carrier of X or x in union Fx )
assume A10: x in the carrier of X ; ::_thesis: x in union Fx
then x in succ ([#] X) by XBOOLE_0:def_3;
then x in [#] (One-Point_Compactification X) by Def9;
then consider B being set such that
A11: x in B and
A12: B in F by A3, TARSKI:def_4;
reconsider B = B as Subset of (One-Point_Compactification X) by A12;
B is open by A2, A12, TOPS_2:def_1;
then B in the topology of (One-Point_Compactification X) by PRE_TOPC:def_2;
then A13: B in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
percases ( B in the topology of X or B in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A13, XBOOLE_0:def_3;
supposeA14: B in the topology of X ; ::_thesis: x in union Fx
then reconsider Bx = B as Subset of X ;
A15: ( ( Bx in F & not Bx \/ {([#] X)} in F ) or Bx \/ {([#] X)} in F ) by A12;
Bx is open by A14, PRE_TOPC:def_2;
then Bx in Fx by A15;
hence x in union Fx by A11, TARSKI:def_4; ::_thesis: verum
end;
suppose B in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: x in union Fx
then consider Bx being Subset of X such that
A16: B = Bx \/ {([#] X)} and
A17: Bx is open and
Bx ` is compact ;
A18: Bx in Fx by A12, A16, A17;
now__::_thesis:_not_x_in_{([#]_X)}
assume x in {([#] X)} ; ::_thesis: contradiction
then x = [#] X by TARSKI:def_1;
hence contradiction by A10; ::_thesis: verum
end;
then x in Bx by A11, A16, XBOOLE_0:def_3;
hence x in union Fx by A18, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
then [#] X = union Fx by SETFAM_1:45;
then Fx is Cover of U ` by SETFAM_1:def_11;
then consider Gx being Subset-Family of X such that
A19: Gx c= Fx and
A20: Gx is Cover of U ` and
A21: Gx is finite by A9, A4, COMPTS_1:def_4;
set GX = { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } ;
A22: { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } c= the topology of (One-Point_Compactification X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } or x in the topology of (One-Point_Compactification X) )
assume x in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } ; ::_thesis: x in the topology of (One-Point_Compactification X)
then consider W being Subset of (One-Point_Compactification X) such that
A23: x = W and
A24: W in F and
ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ;
W is open by A2, A24, TOPS_2:def_1;
hence x in the topology of (One-Point_Compactification X) by A23, PRE_TOPC:def_2; ::_thesis: verum
end;
defpred S1[ set , set ] means ( X in Gx & ( X \/ {([#] X)} in F implies c2 = X \/ {([#] X)} ) & ( not X \/ {([#] X)} in F implies c2 = X ) );
A25: for x being set st x in Gx holds
ex y being set st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Gx implies ex y being set st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S1[x,y] ) )
assume A26: x in Gx ; ::_thesis: ex y being set st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S1[x,y] )
then x in Fx by A19;
then consider U being Subset of X such that
A27: x = U and
U is open and
A28: ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ;
percases ( not U \/ {([#] X)} in F or U \/ {([#] X)} in F ) ;
supposeA29: not U \/ {([#] X)} in F ; ::_thesis: ex y being set st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S1[x,y] )
then reconsider y = U as Subset of (One-Point_Compactification X) by A28;
take y ; ::_thesis: ( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S1[x,y] )
thus y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } by A26, A27, A28, A29; ::_thesis: S1[x,y]
thus S1[x,y] by A26, A27, A29; ::_thesis: verum
end;
supposeA30: U \/ {([#] X)} in F ; ::_thesis: ex y being set st
( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S1[x,y] )
then reconsider y = U \/ {([#] X)} as Subset of (One-Point_Compactification X) ;
take y ; ::_thesis: ( y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } & S1[x,y] )
thus y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } by A26, A27, A30; ::_thesis: S1[x,y]
thus S1[x,y] by A26, A27, A30; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A31: dom f = Gx and
rng f c= { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } and
A32: for x being set st x in Gx holds
S1[x,f . x] from FUNCT_1:sch_5(A25);
A33: { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } or y in rng f )
assume y in { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } ; ::_thesis: y in rng f
then consider W being Subset of (One-Point_Compactification X) such that
A34: y = W and
W in F and
A35: ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ;
consider V being Subset of X such that
A36: V in Gx and
A37: ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) by A35;
f . V in rng f by A31, A36, FUNCT_1:3;
hence y in rng f by A32, A34, A36, A37; ::_thesis: verum
end;
rng f is finite by A21, A31, FINSET_1:8;
then reconsider GX = { W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) } as finite Subset-Family of (One-Point_Compactification X) by A33, A22, XBOOLE_1:1;
take G = GX \/ {A}; ::_thesis: ( G c= F & G is Cover of the carrier of (One-Point_Compactification X) & G is finite )
A38: GX c= F
proof
let P be set ; :: according to TARSKI:def_3 ::_thesis: ( not P in GX or P in F )
assume P in GX ; ::_thesis: P in F
then ex W being Subset of (One-Point_Compactification X) st
( P = W & W in F & ex V being Subset of X st
( V in Gx & ( ( V in F & not V \/ {([#] X)} in F & W = V ) or ( V \/ {([#] X)} in F & W = V \/ {([#] X)} ) ) ) ) ;
hence P in F ; ::_thesis: verum
end;
{A} c= F by A6, ZFMISC_1:31;
hence G c= F by A38, XBOOLE_1:8; ::_thesis: ( G is Cover of the carrier of (One-Point_Compactification X) & G is finite )
union G = [#] (One-Point_Compactification X)
proof
thus union G c= [#] (One-Point_Compactification X) ; :: according to XBOOLE_0:def_10 ::_thesis: [#] (One-Point_Compactification X) c= union G
let P be set ; :: according to TARSKI:def_3 ::_thesis: ( not P in [#] (One-Point_Compactification X) or P in union G )
assume P in [#] (One-Point_Compactification X) ; ::_thesis: P in union G
then A39: P in succ ([#] X) by Def9;
percases ( P in [#] X or P in {([#] X)} ) by A39, XBOOLE_0:def_3;
suppose P in [#] X ; ::_thesis: P in union G
then P in (U `) \/ U by PRE_TOPC:2;
then A40: ( P in U ` or P in U ) by XBOOLE_0:def_3;
A41: union Gx c= union GX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union Gx or z in union GX )
assume z in union Gx ; ::_thesis: z in union GX
then consider S being set such that
A42: z in S and
A43: S in Gx by TARSKI:def_4;
S in Fx by A19, A43;
then consider Z being Subset of X such that
A44: S = Z and
Z is open and
A45: ( ( Z in F & not Z \/ {([#] X)} in F ) or Z \/ {([#] X)} in F ) ;
percases ( ( Z in F & not Z \/ {([#] X)} in F ) or Z \/ {([#] X)} in F ) by A45;
suppose ( Z in F & not Z \/ {([#] X)} in F ) ; ::_thesis: z in union GX
then Z in GX by A43, A44;
hence z in union GX by A42, A44, TARSKI:def_4; ::_thesis: verum
end;
supposeA46: Z \/ {([#] X)} in F ; ::_thesis: z in union GX
A47: z in Z \/ {([#] X)} by A42, A44, XBOOLE_0:def_3;
Z \/ {([#] X)} in GX by A43, A44, A46;
hence z in union GX by A47, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
U ` c= union Gx by A20, SETFAM_1:def_11;
then ( P in union Gx or P in U ) by A40;
then ( P in union GX or P in A ) by A8, A41, XBOOLE_0:def_3;
then ( P in union GX or P in union {A} ) by ZFMISC_1:25;
then P in (union GX) \/ (union {A}) by XBOOLE_0:def_3;
hence P in union G by ZFMISC_1:78; ::_thesis: verum
end;
supposeA48: P in {([#] X)} ; ::_thesis: P in union G
A in {A} by TARSKI:def_1;
then A49: A in G by XBOOLE_0:def_3;
P = [#] X by A48, TARSKI:def_1;
hence P in union G by A5, A49, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence G is Cover of (One-Point_Compactification X) by SETFAM_1:def_11; ::_thesis: G is finite
thus G is finite ; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: ( ( X is Hausdorff & X is locally-compact ) iff One-Point_Compactification X is Hausdorff )
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
A1: not [#] X in [#] X ;
A2: [#] (One-Point_Compactification X) = succ ([#] X) by Def9;
[#] X in {([#] X)} by TARSKI:def_1;
then reconsider q = [#] X as Point of (One-Point_Compactification X) by A2, XBOOLE_0:def_3;
A3: the topology of (One-Point_Compactification X) = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
A4: [#] X c= [#] (One-Point_Compactification X) by Th4;
thus ( X is Hausdorff & X is locally-compact implies One-Point_Compactification X is Hausdorff ) ::_thesis: ( One-Point_Compactification X is Hausdorff implies ( X is Hausdorff & X is locally-compact ) )
proof
assume that
A5: X is Hausdorff and
A6: X is locally-compact ; ::_thesis: One-Point_Compactification X is Hausdorff
let p, q be Point of (One-Point_Compactification X); :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A7: p <> q ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
percases ( ( p in [#] X & q in [#] X ) or ( p in [#] X & q in {([#] X)} ) or ( q in [#] X & p in {([#] X)} ) or ( p in {([#] X)} & q in {([#] X)} ) ) by A2, XBOOLE_0:def_3;
suppose ( p in [#] X & q in [#] X ) ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
then consider W, V being Subset of X such that
A8: W is open and
A9: V is open and
A10: p in W and
A11: q in V and
A12: W misses V by A5, A7, PRE_TOPC:def_10;
reconsider W = W, V = V as Subset of (One-Point_Compactification X) by A4, XBOOLE_1:1;
V in the topology of X by A9, PRE_TOPC:def_2;
then A13: V in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def_3;
take W ; ::_thesis: ex b1 being Element of K19( the carrier of (One-Point_Compactification X)) st
( W is open & b1 is open & p in W & q in b1 & W misses b1 )
take V ; ::_thesis: ( W is open & V is open & p in W & q in V & W misses V )
W in the topology of X by A8, PRE_TOPC:def_2;
then W in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def_3;
hence ( W is open & V is open ) by A13, PRE_TOPC:def_2; ::_thesis: ( p in W & q in V & W misses V )
thus ( p in W & q in V & W misses V ) by A10, A11, A12; ::_thesis: verum
end;
supposethat A14: p in [#] X and
A15: q in {([#] X)} ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
reconsider px = p as Point of X by A14;
consider P being a_neighborhood of px such that
A16: P is compact by A6, Def6;
[#] X c= [#] (One-Point_Compactification X) by A2, XBOOLE_1:7;
then reconsider W = Int P as Subset of (One-Point_Compactification X) by XBOOLE_1:1;
(P `) ` = P ;
then (P `) \/ {([#] X)} in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A5, A16;
then A17: (P `) \/ {([#] X)} in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def_3;
then reconsider V = (P `) \/ {([#] X)} as Subset of (One-Point_Compactification X) ;
take W ; ::_thesis: ex b1 being Element of K19( the carrier of (One-Point_Compactification X)) st
( W is open & b1 is open & p in W & q in b1 & W misses b1 )
take V ; ::_thesis: ( W is open & V is open & p in W & q in V & W misses V )
W in the topology of X by PRE_TOPC:def_2;
then W in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def_3;
hence W is open by PRE_TOPC:def_2; ::_thesis: ( V is open & p in W & q in V & W misses V )
thus V is open by A17, PRE_TOPC:def_2; ::_thesis: ( p in W & q in V & W misses V )
thus p in W by CONNSP_2:def_1; ::_thesis: ( q in V & W misses V )
thus q in V by A15, XBOOLE_0:def_3; ::_thesis: W misses V
not [#] X in [#] X ;
then not [#] X in Int P ;
then A18: Int P misses {([#] X)} by ZFMISC_1:50;
Int P c= P by TOPS_1:16;
then Int P misses P ` by SUBSET_1:24;
hence W misses V by A18, XBOOLE_1:70; ::_thesis: verum
end;
supposethat A19: q in [#] X and
A20: p in {([#] X)} ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
reconsider qx = q as Point of X by A19;
consider Q being a_neighborhood of qx such that
A21: Q is compact by A6, Def6;
[#] X c= [#] (One-Point_Compactification X) by Th4;
then reconsider W = Int Q as Subset of (One-Point_Compactification X) by XBOOLE_1:1;
(Q `) ` = Q ;
then (Q `) \/ {([#] X)} in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A5, A21;
then A22: (Q `) \/ {([#] X)} in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def_3;
then reconsider V = (Q `) \/ {([#] X)} as Subset of (One-Point_Compactification X) ;
take V ; ::_thesis: ex b1 being Element of K19( the carrier of (One-Point_Compactification X)) st
( V is open & b1 is open & p in V & q in b1 & V misses b1 )
take W ; ::_thesis: ( V is open & W is open & p in V & q in W & V misses W )
thus V is open by A22, PRE_TOPC:def_2; ::_thesis: ( W is open & p in V & q in W & V misses W )
W in the topology of X by PRE_TOPC:def_2;
then W in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def_3;
hence W is open by PRE_TOPC:def_2; ::_thesis: ( p in V & q in W & V misses W )
thus p in V by A20, XBOOLE_0:def_3; ::_thesis: ( q in W & V misses W )
thus q in W by CONNSP_2:def_1; ::_thesis: V misses W
not [#] X in [#] X ;
then not [#] X in Int Q ;
then A23: Int Q misses {([#] X)} by ZFMISC_1:50;
Int Q c= Q by TOPS_1:16;
then Int Q misses Q ` by SUBSET_1:24;
hence V misses W by A23, XBOOLE_1:70; ::_thesis: verum
end;
supposeA24: ( p in {([#] X)} & q in {([#] X)} ) ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
then p = [#] X by TARSKI:def_1;
hence ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A7, A24, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
A25: X is SubSpace of One-Point_Compactification X by Th5;
assume A26: One-Point_Compactification X is Hausdorff ; ::_thesis: ( X is Hausdorff & X is locally-compact )
hence X is Hausdorff by A25; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
x in [#] X ;
then reconsider p = x as Point of (One-Point_Compactification X) by A4;
not [#] X in [#] X ;
then p <> q ;
then consider V, U being Subset of (One-Point_Compactification X) such that
A27: V is open and
A28: U is open and
A29: p in V and
A30: q in U and
A31: V misses U by A26, PRE_TOPC:def_10;
A32: now__::_thesis:_not_U_in_the_topology_of_X
assume U in the topology of X ; ::_thesis: contradiction
then q in [#] X by A30;
hence contradiction ; ::_thesis: verum
end;
U in the topology of (One-Point_Compactification X) by A28, PRE_TOPC:def_2;
then U in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A3, A32, XBOOLE_0:def_3;
then consider W being Subset of X such that
A33: U = W \/ {([#] X)} and
W is open and
A34: W ` is compact ;
A35: ([#] X) \ U = (([#] X) \ W) /\ (([#] X) \ {([#] X)}) by A33, XBOOLE_1:53
.= (([#] X) \ W) /\ ([#] X) by A1, ZFMISC_1:57
.= ([#] X) \ W by XBOOLE_1:28 ;
A36: [#] X in {([#] X)} by TARSKI:def_1;
then A37: [#] X in U by A33, XBOOLE_0:def_3;
A38: ([#] (One-Point_Compactification X)) \ U = (([#] X) \ U) \/ ({([#] X)} \ U) by A2, XBOOLE_1:42
.= (([#] X) \ W) \/ {} by A37, A35, ZFMISC_1:60
.= W ` ;
A39: V c= U ` by A31, SUBSET_1:23;
then A40: V c= [#] X by A38, XBOOLE_1:1;
A41: now__::_thesis:_not_V_in__{__(U_\/_{([#]_X)})_where_U_is_Subset_of_X_:_(_U_is_open_&_U_`_is_compact_)__}_
assume V in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: contradiction
then ex S being Subset of X st
( V = S \/ {([#] X)} & S is open & S ` is compact ) ;
then [#] X in V by A36, XBOOLE_0:def_3;
then [#] X in [#] X by A40;
hence contradiction ; ::_thesis: verum
end;
V in the topology of (One-Point_Compactification X) by A27, PRE_TOPC:def_2;
then V in the topology of X by A3, A41, XBOOLE_0:def_3;
then reconsider Vx = V as open Subset of X by PRE_TOPC:def_2;
set K = Cl Vx;
A42: Int Vx c= Int (Cl Vx) by PRE_TOPC:18, TOPS_1:19;
x in Int Vx by A29, TOPS_1:23;
then reconsider K = Cl Vx as a_neighborhood of x by A42, CONNSP_2:def_1;
take K ; ::_thesis: K is compact
(U `) /\ ([#] X) = W ` by A38, XBOOLE_1:28;
then W ` is closed by A25, A28, PRE_TOPC:13;
hence K is compact by A34, A39, A38, COMPTS_1:9, TOPS_1:5; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: ( not X is compact iff ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) )
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
A1: not [#] X in [#] X ;
A2: [#] (One-Point_Compactification X) = succ ([#] X) by Def9;
A3: [#] X in {([#] X)} by TARSKI:def_1;
then A4: [#] X in [#] (One-Point_Compactification X) by A2, XBOOLE_0:def_3;
A5: the topology of (One-Point_Compactification X) = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
thus ( not X is compact implies ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) ) ::_thesis: ( ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) implies not X is compact )
proof
assume not X is compact ; ::_thesis: ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense )
then A6: not [#] X is compact by COMPTS_1:1;
[#] X c= [#] (One-Point_Compactification X) by Th4;
then reconsider X9 = [#] X as Subset of (One-Point_Compactification X) ;
take X9 ; ::_thesis: ( X9 = [#] X & X9 is dense )
thus X9 = [#] X ; ::_thesis: X9 is dense
thus Cl X9 c= [#] (One-Point_Compactification X) ; :: according to XBOOLE_0:def_10,TOPS_1:def_3 ::_thesis: [#] (One-Point_Compactification X) c= Cl X9
A7: [#] X c= Cl X9 by PRE_TOPC:18;
A8: now__::_thesis:_[#]_X_in_Cl_X9
reconsider Xe = [#] X as Element of (One-Point_Compactification X) by A3, A2, XBOOLE_0:def_3;
assume A9: not [#] X in Cl X9 ; ::_thesis: contradiction
reconsider XX = {Xe} as Subset of (One-Point_Compactification X) ;
A10: now__::_thesis:_not_XX_in_the_topology_of_X
assume XX in the topology of X ; ::_thesis: contradiction
then [#] X in [#] X by A3;
hence contradiction ; ::_thesis: verum
end;
([#] (One-Point_Compactification X)) \ (Cl X9) = (([#] X) \ (Cl X9)) \/ ({([#] X)} \ (Cl X9)) by A2, XBOOLE_1:42
.= {} \/ ({([#] X)} \ (Cl X9)) by A7, XBOOLE_1:37
.= XX by A9, ZFMISC_1:59 ;
then XX is open by PRE_TOPC:def_3;
then XX in the topology of (One-Point_Compactification X) by PRE_TOPC:def_2;
then XX in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A5, A10, XBOOLE_0:def_3;
then consider U being Subset of X such that
A11: XX = U \/ {([#] X)} and
U is open and
A12: U ` is compact ;
now__::_thesis:_not_U_=_XX
assume U = XX ; ::_thesis: contradiction
then [#] X in [#] X by A3;
hence contradiction ; ::_thesis: verum
end;
then U = {} X by A11, ZFMISC_1:37;
hence contradiction by A6, A12; ::_thesis: verum
end;
[#] (One-Point_Compactification X) c= (Cl X9) \/ {([#] X)} by A2, PRE_TOPC:18, XBOOLE_1:9;
hence [#] (One-Point_Compactification X) c= Cl X9 by A8, ZFMISC_1:40; ::_thesis: verum
end;
given X9 being Subset of (One-Point_Compactification X) such that A13: X9 = [#] X and
A14: X9 is dense ; ::_thesis: not X is compact
A15: Cl X9 = [#] (One-Point_Compactification X) by A14, TOPS_1:def_3;
assume X is compact ; ::_thesis: contradiction
then [#] X is compact ;
then ({} X) ` is compact ;
then ({} X) \/ {([#] X)} in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
then A16: {([#] X)} in the topology of (One-Point_Compactification X) by A5, XBOOLE_0:def_3;
then reconsider X1 = {([#] X)} as Subset of (One-Point_Compactification X) ;
X1 is open by A16, PRE_TOPC:def_2;
then A17: Cl (X1 `) = X1 ` by PRE_TOPC:22;
X1 ` = ([#] X) \ X1 by A2, XBOOLE_1:40
.= [#] X by A1, ZFMISC_1:57 ;
hence contradiction by A13, A15, A17, A4; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: ( not X is compact implies incl (X,(One-Point_Compactification X)) is compactification )
set h = incl (X,(One-Point_Compactification X));
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
assume not X is compact ; ::_thesis: incl (X,(One-Point_Compactification X)) is compactification
then A1: ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) by Th7;
A2: [#] X c= [#] (One-Point_Compactification X) by Th4;
then reconsider Xy = [#] X as Subset of (One-Point_Compactification X) ;
A3: [#] ((One-Point_Compactification X) | Xy) = Xy by PRE_TOPC:def_5;
A4: the topology of (One-Point_Compactification X) = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
the topology of ((One-Point_Compactification X) | Xy) = the topology of X
proof
thus the topology of ((One-Point_Compactification X) | Xy) c= the topology of X :: according to XBOOLE_0:def_10 ::_thesis: the topology of X c= the topology of ((One-Point_Compactification X) | Xy)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of ((One-Point_Compactification X) | Xy) or x in the topology of X )
assume A5: x in the topology of ((One-Point_Compactification X) | Xy) ; ::_thesis: x in the topology of X
then reconsider P = x as Subset of ((One-Point_Compactification X) | Xy) ;
consider Q being Subset of (One-Point_Compactification X) such that
A6: Q in the topology of (One-Point_Compactification X) and
A7: P = Q /\ ([#] ((One-Point_Compactification X) | Xy)) by A5, PRE_TOPC:def_4;
percases ( Q in the topology of X or Q in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A4, A6, XBOOLE_0:def_3;
suppose Q in the topology of X ; ::_thesis: x in the topology of X
hence x in the topology of X by A3, A7, XBOOLE_1:28; ::_thesis: verum
end;
suppose Q in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; ::_thesis: x in the topology of X
then consider U being Subset of X such that
A8: Q = U \/ {([#] X)} and
A9: U is open and
U ` is compact ;
not [#] X in [#] X ;
then {([#] X)} misses [#] X by ZFMISC_1:50;
then {([#] X)} /\ ([#] X) = {} by XBOOLE_0:def_7;
then P = (U /\ ([#] X)) \/ {} by A3, A7, A8, XBOOLE_1:23
.= U by XBOOLE_1:28 ;
hence x in the topology of X by A9, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of X or x in the topology of ((One-Point_Compactification X) | Xy) )
assume A10: x in the topology of X ; ::_thesis: x in the topology of ((One-Point_Compactification X) | Xy)
then reconsider P = x as Subset of ((One-Point_Compactification X) | Xy) by A3;
reconsider Q = P as Subset of (One-Point_Compactification X) by A3, XBOOLE_1:1;
A11: P = Q /\ ([#] ((One-Point_Compactification X) | Xy)) by XBOOLE_1:28;
Q in the topology of (One-Point_Compactification X) by A4, A10, XBOOLE_0:def_3;
hence x in the topology of ((One-Point_Compactification X) | Xy) by A11, PRE_TOPC:def_4; ::_thesis: verum
end;
hence incl (X,(One-Point_Compactification X)) is embedding by A2, Th3; :: according to COMPACT1:def_8 ::_thesis: ( One-Point_Compactification X is compact & (incl (X,(One-Point_Compactification X))) .: ([#] X) is dense )
thus One-Point_Compactification X is compact ; ::_thesis: (incl (X,(One-Point_Compactification X))) .: ([#] X) is dense
thus (incl (X,(One-Point_Compactification X))) .: ([#] X) is dense by A2, A1, Th2; ::_thesis: verum
end;