:: Alexandroff One Point Compactification
:: by Czeslaw Bylinski
::
:: Received August 13, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, SETFAM_1, RCOMP_1, SUBSET_1, XBOOLE_0, WAYBEL_3,
YELLOW13, CONNSP_2, TARSKI, ZFMISC_1, TOPS_1, CARD_5, COMPTS_1, NATTRA_1,
RELAT_1, FUNCT_3, FUNCT_1, QUOFIELD, TOPS_2, ORDINAL2, STRUCT_0,
ORDINAL1, FINSET_1, COMPACT1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, SETFAM_1,
ORDINAL1, FINSET_1, FINSUB_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1,
TOPS_2, TDLAT_3, TSEP_1, TEX_3, COMPTS_1, CONNSP_2, WAYBEL_3, YELLOW_9,
YELLOW13;
constructors FINSOP_1, DOMAIN_1, TOPS_1, TOPS_2, YELLOW_9, YELLOW13, TDLAT_3,
CONNSP_2, T_0TOPSP, WAYBEL_3, TSEP_1, TEX_3, COMPTS_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FINSET_1, STRUCT_0, FINSUB_1, RELAT_1,
TOPS_1, BORSUK_2, FUNCT_1, PRE_TOPC, TEX_1, YELLOW13, COMPTS_1, RELSET_1;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, WAYBEL_3,
YELLOW13, SETFAM_1;
equalities ORDINAL1, STRUCT_0, SUBSET_1;
expansions TARSKI, XBOOLE_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, WAYBEL_3;
theorems XBOOLE_1, ZFMISC_1, YELLOW_8, YELLOW_9, XBOOLE_0, CONNSP_2, TEX_3,
TEX_4, PRE_TOPC, TOPS_1, TOPS_2, TSEP_1, TARSKI, FUNCT_1, FINSET_1,
TDLAT_3, FUNCT_2, SUBSET_1, COMPTS_1, TOPMETR, YELLOW13, SETFAM_1;
schemes FUNCT_1;
begin :: Preliminaires
definition
let X be TopSpace, P be Subset-Family of X;
attr P is compact means
for U being Subset of X st U in P holds U is compact;
end;
definition
let X be TopSpace, U be Subset of X;
attr U is relatively-compact means
:Def2:
Cl U is compact;
end;
registration
let X be TopSpace;
cluster empty -> relatively-compact for Subset of X;
coherence
by PRE_TOPC:22;
end;
registration
let T be TopSpace;
cluster relatively-compact for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
registration
let X be TopSpace, U be relatively-compact Subset of X;
cluster Cl U -> compact;
coherence by Def2;
end;
notation
let X be TopSpace, U be Subset of X;
synonym U is pre-compact for U is relatively-compact;
end;
:: see WAYBEL_3:def 9
notation
let X be non empty TopSpace;
synonym X is liminally-compact for X is locally-compact;
end;
:: see WAYBEL_3:def 9
definition
let X be non empty TopSpace;
redefine attr X is liminally-compact means :: redefines liminally-compact (COMPACT1, synonym) → locally-compact (WAYBEL_3, definition)
:Def3:
for x being Point of X ex B being basis of x st B is compact;
compatibility
proof
hereby
assume
A1: X is liminally-compact;
let x be Point of X;
set B = {Q where Q is a_neighborhood of x: Q is compact & ex V being
a_neighborhood of x st Q c= V};
B c= bool [#]X
proof
let A be object;
assume A in B;
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 thesis;
end;
then reconsider B as Subset-Family of X;
A2: B is basis of x
proof
let V be a_neighborhood of x;
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;
reconsider Q as a_neighborhood of x by A3,CONNSP_2:def 1;
take Q;
Int V c= V by TOPS_1:16;
hence thesis by A4,A5;
end;
B is compact
proof
let U be Subset of X;
assume U in B;
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 thesis;
end;
hence ex B being basis of x st B is compact by A2;
end;
assume
A6: for x being Point of X ex B being basis of x st B is compact;
let x be Point of X, P be Subset of X such that
A7: x in P and
A8: P is open;
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;
thus x in Int Q & Q c= P by A11,A12;
thus thesis by A9,A10;
end;
end;
definition
let X be non empty TopSpace;
attr X is locally-relatively-compact means
for x being Point of X ex
U being a_neighborhood of x st U is relatively-compact;
end;
definition
let X be non empty TopSpace;
attr X is locally-closed/compact means
for x being Point of X ex U being a_neighborhood of x st U is closed compact;
end;
definition
let X be non empty TopSpace;
attr X is locally-compact means
:Def6:
for x being Point of X ex U being a_neighborhood of x st U is compact;
end;
registration
cluster liminally-compact -> locally-compact for non empty TopSpace;
coherence
proof
let X be non empty TopSpace such that
A1: X is liminally-compact;
let x be Point of X;
consider B being basis of x such that
A2: B is compact by A1;
set V = the a_neighborhood of x;
consider Y being a_neighborhood of x such that
A3: Y in B and
Y c= V by YELLOW13:def 2;
Y is compact by A2,A3;
hence thesis;
end;
end;
registration
cluster locally-compact -> liminally-compact for
non empty regular TopSpace;
coherence
proof
let X be non empty regular TopSpace such that
A1: X is locally-compact;
let x be Point of X;
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};
B c= bool [#]X
proof
let A be object;
assume A in B;
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 thesis;
end;
then reconsider B as Subset-Family of X;
A2: B is basis of x
proof
let V be a_neighborhood of x;
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;
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 as a_neighborhood of x by A7,CONNSP_2:def 1;
take Q;
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;
V /\ W c= V by XBOOLE_1:17;
hence thesis by A6;
end;
B is compact
proof
let U be Subset of X;
assume U in B;
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 thesis;
end;
hence thesis by A2;
end;
end;
registration
cluster locally-relatively-compact -> locally-closed/compact for non empty
TopSpace;
coherence
proof
let X be non empty TopSpace such that
A1: X is locally-relatively-compact;
let x be Point of X;
consider U being a_neighborhood of x such that
A2: U is relatively-compact by A1;
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 thesis by A2;
end;
end;
registration
cluster locally-closed/compact -> locally-relatively-compact for non empty
TopSpace;
coherence
proof
let X be non empty TopSpace such that
A1: X is locally-closed/compact;
let x be Point of X;
consider U being a_neighborhood of x such that
A2: U is closed compact by A1;
Cl U = U by A2,PRE_TOPC:22;
then U is relatively-compact by A2;
hence thesis;
end;
end;
registration
cluster locally-relatively-compact -> locally-compact for
non empty TopSpace;
coherence
proof
let X be non empty TopSpace such that
A1: X is locally-relatively-compact;
let x be Point of X;
consider Y being a_neighborhood of x such that
A2: Y is relatively-compact by A1;
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 thesis by A2;
end;
end;
registration
cluster locally-compact -> locally-relatively-compact for
non empty Hausdorff
TopSpace;
coherence
proof
let X be non empty Hausdorff TopSpace such that
A1: X is locally-compact;
let x be Point of X;
consider U being a_neighborhood of x such that
A2: U is compact by A1;
Cl U = U by A2,PRE_TOPC:22;
then U is relatively-compact by A2;
hence thesis;
end;
end;
registration
cluster compact -> locally-compact for non empty TopSpace;
coherence
proof
let X be non empty TopSpace;
set Y = [#]X;
assume
A1: X is compact;
let x be Point of X;
Int Y = Y by TOPS_1:23;
then Y is a_neighborhood of x by CONNSP_2:def 1;
hence thesis by A1;
end;
end;
registration
cluster discrete -> locally-compact for non empty TopSpace;
coherence
proof
let X be non empty TopSpace such that
A1: X is discrete;
let x be Point of X;
set Y = {x};
Y is open by A1,TDLAT_3:15;
then Int Y = Y by TOPS_1:23;
then x in Int Y by TARSKI:def 1;
then reconsider Y as a_neighborhood of x by CONNSP_2:def 1;
Y is compact;
hence thesis;
end;
end;
registration
cluster discrete non empty for TopSpace;
existence
proof
set X = the discrete non empty TopSpace;
take X;
thus thesis;
end;
end;
registration
let X be locally-compact non empty TopSpace, C be closed non empty Subset
of X;
cluster X | C -> locally-compact;
coherence
proof
let x be Point of X|C;
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 as a_neighborhood of x by A2,TOPMETR:5;
take KC;
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 thesis by A7,COMPTS_1:3;
end;
end;
registration
let X be locally-compact non empty regular TopSpace, P be open non empty
Subset of X;
cluster X | P -> locally-compact;
coherence
proof
let x be Point of X|P;
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;
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 thesis by A5;
end;
end;
theorem
for X being Hausdorff non empty TopSpace, E being non empty Subset of
X st X|E is dense locally-compact holds X|E is open
proof
let X be Hausdorff non empty TopSpace, E be non empty Subset of X such that
A1: X|E is dense locally-compact;
A2: [#](X|E) = E by PRE_TOPC:8;
Int E = E
proof
thus Int E c= E by TOPS_1:16;
let a be object;
assume
A3: a in 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;
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;
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,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;
then G c= E by A2,XBOOLE_1:1;
then
A11: G in UE 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 UE by A12,A11,TARSKI:def 4;
hence thesis by TEX_4:3;
end;
hence thesis by A2,TSEP_1:16;
end;
theorem Th2:
for X,Y being TopSpace, A being Subset of X st [#]X c= [#]Y holds
incl(X,Y).:A = A
proof
let X,Y be TopSpace, A be Subset of X;
assume [#]X c= [#]Y;
hence incl(X,Y).:A = id([#]X).:A by YELLOW_9:def 1
.= A by FUNCT_1:92;
end;
definition
let X,Y be TopSpace, f be Function of X,Y;
attr f is embedding means
ex h being Function of X, Y | (rng f) st h = f & h is being_homeomorphism;
end;
theorem Th3:
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 such that
A1: [#]X c= [#]Y;
A2: incl(X,Y) = id X by A1,YELLOW_9:def 1;
set YY = Y| (rng incl(X,Y));
A3: [#]YY = 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,YY 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;
A7: for P being Subset of X st P is open holds (h")"P is open
proof
let P be Subset of X;
reconsider Q = P as Subset of YY by A2,A3;
assume P is open;
then
A8: P in the topology of X;
(h")"P = h.:Q by A2,A3,TOPS_2:54
.= Q by A2,FUNCT_1:92;
hence (h")"P in the topology of YY by A5,A6,A2,A8;
end;
A9: [#]X = {} implies [#]X = {};
A10: for P being Subset of YY st P is open holds h"P is open
proof
let P be Subset of YY;
reconsider Q = P as Subset of X by A2,A3;
assume P is open;
then P in the topology of YY;
then Q in the topology of X by A5,A6,A2;
then Q is open;
then f"Q is open by A9,TOPS_2:43;
then f"Q in the topology of X;
hence h"P in the topology of X by A1,YELLOW_9:def 1;
end;
take h;
thus h = incl(X,Y);
thus dom h = [#]X & rng h = [#]YY by A4,FUNCT_2:def 1,PRE_TOPC:def 5;
thus h is one-to-one by A2;
[#]YY = {} implies [#]X = {} by A2,A3;
hence h is continuous by A10,TOPS_2:43;
[#]X = {} implies [#]YY = {};
hence thesis by A7,TOPS_2:43;
end;
definition
let X be TopSpace, Y be TopSpace, h be Function of X,Y;
attr h is compactification means
h is embedding & Y is compact & h.:( [#]X) is dense;
end;
registration
let X be TopSpace, Y be TopSpace;
cluster compactification -> embedding for Function of X,Y;
coherence;
end;
definition
let X be TopStruct;
func One-Point_Compactification(X) -> strict TopStruct means
:Def9:
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
proof
set T = succ [#]X, D = {U \/ {[#]X} where U is Subset of X: U is open & U`
is compact}, O = (the topology of X) \/ D;
O c= bool T
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
A1: now
assume a in D;
then consider U being Subset of X such that
A2: a = U \/ {[#]X} and
U is open and
U` is compact;
thus aa c= T
proof
let A be object;
assume A in aa;
then A in U or A in {[#]X} by A2,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
end;
assume a in O;
then a in the topology of X or a in D by XBOOLE_0:def 3;
then a is Subset of T by A1,XBOOLE_1:10;
hence thesis;
end;
then reconsider O as Subset-Family of T;
set Y = TopStruct(#T,O#);
Y is non empty;
hence thesis;
end;
uniqueness;
end;
registration
let X be TopStruct;
cluster One-Point_Compactification(X) -> non empty;
coherence
proof
the carrier of One-Point_Compactification(X) = succ([#]X) by Def9;
hence thesis;
end;
end;
theorem Th4:
for X being TopStruct holds [#]X c= [#]One-Point_Compactification (X)
proof
let X be TopStruct;
[#]One-Point_Compactification(X) = succ([#]X) by Def9;
hence thesis by XBOOLE_1:7;
end;
registration
let X be TopSpace;
cluster One-Point_Compactification(X) -> TopSpace-like;
coherence
proof
set Y = One-Point_Compactification(X);
set T = succ [#]X, 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) \/
D by Def9;
A3: [#]One-Point_Compactification(X) = T by Def9;
Y is TopSpace-like
proof
([#]X)` = ({}X)`` .= {}X;
then T in D;
hence the carrier of Y in the topology of Y by A3,A2,XBOOLE_0:def 3;
hereby
let a be Subset-Family of Y;
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: ua c= the topology of X
proof
let x be object;
assume x in ua;
then
ex U being Subset of X st x = U & U is open & (U in a or U \/ {
[#]X} in a);
hence thesis;
end;
then reconsider ua 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;
assume
A7: a c= the topology of Y;
A8: union ua = (union a) \ {[#]X}
proof
thus union ua c= (union a) \ {[#]X}
proof
let x be object;
assume x in union ua;
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
per cases by A12;
suppose
U in a;
hence x in union a by A9,A11,TARSKI:def 4;
end;
suppose
A14: U \/ {[#]X} in a;
x in U \/ {[#]X} by A9,A11,XBOOLE_0:def 3;
hence x in union a by A14,TARSKI:def 4;
end;
end;
now
assume x in {[#]X};
then
A15: x = [#]X by TARSKI:def 1;
A: x in [#]X by A9,A11;
reconsider xx = x as set by TARSKI:1;
not xx in xx;
hence contradiction by A,A15;
end;
hence thesis by A13,XBOOLE_0:def 5;
end;
let x be object;
assume
A16: x in (union a) \ {[#]X};
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;
per cases by A2,A7,A18,XBOOLE_0:def 3;
suppose
A19: A in the topology of X;
then reconsider U = A as Subset of X;
U is open by A19;
then U in ua by A18;
hence thesis by A17,TARSKI:def 4;
end;
suppose
A in D;
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 thesis by A22,TARSKI:def 4;
end;
end;
per cases;
suppose
A23: [#]X in union a;
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 D 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
assume [#]X in U;
then [#]X in [#]X;
hence contradiction;
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 D by A6,A29;
hence union a in the topology of Y by A2,XBOOLE_0:def 3;
end;
suppose
A30: not [#]X in union a;
A31: a c= the topology of X
proof
let A be object;
reconsider AA=A as set by TARSKI:1;
assume
A32: A in a;
assume not A in the topology of X;
then A in D 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 AA by A33,XBOOLE_0:def 3;
hence contradiction by A30,A32,TARSKI:def 4;
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 Y by A2,XBOOLE_0:def 3;
end;
end;
let a,b be Subset of Y;
assume
A34: a in the topology of Y;
assume
A35: b in the topology of Y;
per cases by A2,A34,A35,XBOOLE_0:def 3;
suppose
a in the topology of X & b in the topology of X;
then a /\ b in the topology of X by PRE_TOPC:def 1;
hence a /\ b in the topology of Y by A2,XBOOLE_0:def 3;
end;
suppose that
A36: a in the topology of X and
A37: b in D;
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;
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;
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 Y by A2,XBOOLE_0:def 3;
end;
suppose that
A40: b in the topology of X and
A41: a in D;
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;
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;
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 Y by A2,XBOOLE_0:def 3;
end;
suppose that
A44: a in D and
A45: b in D;
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 D by A47,A50,A52;
hence a /\ b in the topology of Y by A2,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
end;
theorem Th5:
for X being TopStruct holds X is SubSpace of One-Point_Compactification(X)
proof
let X be TopStruct;
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;
let P being Subset of X;
A2: the topology of One-Point_Compactification(X) = (the topology of X) \/ D
by Def9;
hereby
reconsider Q = P as Subset of One-Point_Compactification(X) by A1,
XBOOLE_1:1;
assume
A3: P in the topology of X;
take Q;
thus Q in the topology of One-Point_Compactification(X) by A2,A3,
XBOOLE_0:def 3;
thus P = Q /\ [#]X by XBOOLE_1:28;
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;
per cases by A2,A4,XBOOLE_0:def 3;
suppose
Q in the topology of X;
hence thesis by A5,XBOOLE_1:28;
end;
suppose
Q in D;
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 = {};
then P = (U /\ [#]X) \/ {} by A5,A6,XBOOLE_1:23
.= U by XBOOLE_1:28;
hence thesis by A7;
end;
end;
registration
let X be TopSpace;
cluster One-Point_Compactification(X) -> compact;
coherence
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) such that
A1: F is Cover of One-Point_Compactification(X) and
A2: F is open;
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)};
Fx c= the topology of X
proof
let x be object;
assume x in Fx;
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 thesis;
end;
then reconsider Fx as Subset-Family of X by XBOOLE_1:1;
A4: Fx is open
proof
let P be Subset of X;
assume P in Fx;
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 thesis;
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 as Subset of One-Point_Compactification(X) by A6;
A is open by A2,A6;
then A in the topology of One-Point_Compactification(X);
then
A7: A in (the topology of X) \/ D by Def9;
not [#]X in [#]X;
then not A in the topology of X by A5;
then A in D 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 object;
assume
A10: x in the carrier of X;
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 as Subset of One-Point_Compactification(X) by A12;
B is open by A2,A12;
then B in the topology of One-Point_Compactification(X);
then
A13: B in (the topology of X) \/ D by Def9;
per cases by A13,XBOOLE_0:def 3;
suppose
A14: B in the topology of X;
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;
then Bx in Fx by A15;
hence x in union Fx by A11,TARSKI:def 4;
end;
suppose
B in D;
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
assume x in {[#]X};
then A: x = [#]X by TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
not xx in xx;
hence contradiction by A,A10;
end;
then x in Bx by A11,A16,XBOOLE_0:def 3;
hence x in union Fx by A18,TARSKI:def 4;
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;
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: GX c= the topology of One-Point_Compactification(X)
proof
let x be object;
assume x in GX;
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;
hence thesis by A23;
end;
defpred P[object,object] means
ex D1 being set st D1 = $1 & ($1 in Gx & (D1 \/ {[#]X} in F
implies $2 = D1 \/
{[#]X}) & (not D1 \/ {[#]X} in F implies $2 = $1));
A25: for x being object st x in Gx ex y being object st y in GX & P[x,y]
proof
let x be object;
assume
A26: x in Gx;
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;
per cases;
suppose
A29: not U \/ {[#]X} in F;
then reconsider
y = U as Subset of One-Point_Compactification(X) by A28;
reconsider y as object;
take y;
thus y in GX by A26,A27,A28,A29;
thus thesis by A26,A27,A29;
end;
suppose
A30: U \/ {[#]X} in F;
then reconsider
y = U \/ {[#]X} as Subset of One-Point_Compactification(X);
take y;
thus y in GX by A26,A27,A30;
thus thesis by A26,A27,A30;
end;
end;
consider f being Function such that
A31: dom f = Gx and
rng f c= GX and
A32: for x being object st x in Gx holds P[x,f.x] from FUNCT_1:sch 6(A25);
A33: GX c= rng f
proof
let y be object;
assume y in GX;
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;
A38: f.V in rng f by A31,A36,FUNCT_1:3;
P[V,f.V] by A32,A36;
hence thesis by A34,A37,A38;
end;
rng f is finite by A21,A31,FINSET_1:8;
then reconsider
GX as finite Subset-Family of One-Point_Compactification(X ) by A33,A22,
XBOOLE_1:1;
take G = GX \/ {A};
A39: GX c= F
proof
let P be object;
assume P in GX;
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 thesis;
end;
{A} c= F by A6,ZFMISC_1:31;
hence G c= F by A39,XBOOLE_1:8;
union G = [#]One-Point_Compactification(X)
proof
thus union G c= [#]One-Point_Compactification(X);
let P be object;
assume P in [#]One-Point_Compactification(X);
then
A40: P in succ([#]X) by Def9;
per cases by A40,XBOOLE_0:def 3;
suppose
P in [#]X;
then P in U` \/ U by PRE_TOPC:2;
then
A41: P in U` or P in U by XBOOLE_0:def 3;
A42: union Gx c= union GX
proof
let z be object;
assume z in union Gx;
then consider S being set such that
A43: z in S and
A44: S in Gx by TARSKI:def 4;
S in Fx by A19,A44;
then consider Z being Subset of X such that
A45: S = Z and
Z is open and
A46: Z in F & not Z \/ {[#]X} in F or Z \/ {[#]X} in F;
per cases by A46;
suppose
Z in F & not Z \/ {[#]X} in F;
then Z in GX by A44,A45;
hence thesis by A43,A45,TARSKI:def 4;
end;
suppose
A47: Z \/ {[#]X} in F;
A48: z in Z \/ {[#]X} by A43,A45,XBOOLE_0:def 3;
Z \/ {[#]X} in GX by A44,A45,A47;
hence thesis by A48,TARSKI:def 4;
end;
end;
U` c= union Gx by A20,SETFAM_1:def 11;
then P in union Gx or P in U by A41;
then P in union GX or P in A by A8,A42,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 thesis by ZFMISC_1:78;
end;
suppose
A49: P in {[#]X};
A in {A} by TARSKI:def 1;
then
A50: A in G by XBOOLE_0:def 3;
P = [#]X by A49,TARSKI:def 1;
hence thesis by A5,A50,TARSKI:def 4;
end;
end;
hence G is Cover of One-Point_Compactification(X) by SETFAM_1:def 11;
thus thesis;
end;
end;
theorem
for X being non empty TopSpace holds X is Hausdorff locally-compact
iff One-Point_Compactification(X) is Hausdorff
proof
let X be non empty TopSpace;
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) \/ D
by Def9;
A4: [#]X c= [#]One-Point_Compactification(X) by Th4;
thus X is Hausdorff locally-compact implies One-Point_Compactification(X) is
Hausdorff
proof
assume that
A5: X is Hausdorff and
A6: X is locally-compact;
let p, q be Point of One-Point_Compactification(X) such that
A7: p <> q;
per cases by A2,XBOOLE_0:def 3;
suppose
p in [#]X & q in [#]X;
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;
reconsider W,V as Subset of One-Point_Compactification(X) by A4,
XBOOLE_1:1;
V in the topology of X by A9;
then
A13: V in the topology of One-Point_Compactification(X) by A3,XBOOLE_0:def 3;
take W,V;
W in the topology of X by A8;
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;
thus thesis by A10,A11,A12;
end;
suppose that
A14: p in [#]X and
A15: q in {[#]X};
reconsider px = p as Point of X by A14;
consider P being a_neighborhood of px such that
A16: P is compact by A6;
[#]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 D 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,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;
thus V is open by A17;
thus p in W by CONNSP_2:def 1;
thus q in V by A15,XBOOLE_0:def 3;
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 thesis by A18,XBOOLE_1:70;
end;
suppose that
A19: q in [#]X and
A20: p in {[#]X};
reconsider qx = q as Point of X by A19;
consider Q being a_neighborhood of qx such that
A21: Q is compact by A6;
[#]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 D 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,W;
thus V is open by A22;
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;
thus p in V by A20,XBOOLE_0:def 3;
thus q in W by CONNSP_2:def 1;
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 thesis by A23,XBOOLE_1:70;
end;
suppose
A24: p in {[#]X} & q in {[#]X};
then p = [#]X by TARSKI:def 1;
hence thesis by A7,A24,TARSKI:def 1;
end;
end;
A25: X is SubSpace of One-Point_Compactification(X) by Th5;
assume
A26: One-Point_Compactification(X) is Hausdorff;
hence X is Hausdorff by A25;
let x be Point of X;
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;
A32: now
assume U in the topology of X;
then q in [#]X by A30;
hence contradiction;
end;
U in the topology of One-Point_Compactification(X) by A28;
then U in D 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
assume V in D;
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;
end;
V in the topology of One-Point_Compactification(X) by A27;
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 K by PRE_TOPC:18,TOPS_1:19;
x in Int Vx by A29,TOPS_1:23;
then reconsider K as a_neighborhood of x by A42,CONNSP_2:def 1;
take K;
U` /\ [#]X = W` by A38,XBOOLE_1:28;
then W` is closed by A25,A28,PRE_TOPC:13;
hence thesis by A34,A39,A38,COMPTS_1:9,TOPS_1:5;
end;
theorem Th7:
for X being non empty TopSpace holds X is non compact iff ex X9
being Subset of One-Point_Compactification(X) st X9 = [#]X & X9 is dense
proof
let X be non empty TopSpace;
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) \/ D
by Def9;
thus X is non compact implies ex X9 being Subset of
One-Point_Compactification(X) st X9 = [#]X & X9 is dense
proof
assume X is non compact;
then
A6: [#]X is non compact;
[#]X c= [#]One-Point_Compactification(X) by Th4;
then reconsider X9 = [#]X as Subset of One-Point_Compactification(X);
take X9;
thus X9 = [#]X;
thus Cl(X9) c= [#]One-Point_Compactification(X);
A7: [#]X c= Cl(X9) by PRE_TOPC:18;
A8: now
reconsider Xe = [#]X as Element of One-Point_Compactification(X) by A3,A2
,XBOOLE_0:def 3;
assume
A9: not [#]X in Cl(X9);
reconsider XX = {Xe} as Subset of One-Point_Compactification(X);
A10: now
assume XX in the topology of X;
then [#]X in [#]X by A3;
hence contradiction;
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);
then XX in D 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
assume U = XX;
then [#]X in [#]X by A3;
hence contradiction;
end;
then U = {}X by A11,ZFMISC_1:37;
hence contradiction by A6,A12;
end;
[#]One-Point_Compactification(X) c= Cl(X9) \/ {[#]X} by A2,PRE_TOPC:18
,XBOOLE_1:9;
hence thesis by A8,ZFMISC_1:40;
end;
given X9 being Subset of One-Point_Compactification(X) such that
A13: X9 = [#]X and
A14: X9 is dense;
A15: Cl X9= [#]One-Point_Compactification(X) by A14;
assume X is compact;
then [#]X is compact;
then ({}X)` is compact;
then {}X \/ {[#]X} in D;
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;
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;
end;
theorem
for X being non empty TopSpace st X is non compact holds incl(X,
One-Point_Compactification X) is compactification
proof
let X be non empty TopSpace;
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 X is non compact;
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) \/ D
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
proof
let x be object;
assume
A5: x in the topology of (One-Point_Compactification X) | Xy;
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;
per cases by A4,A6,XBOOLE_0:def 3;
suppose
Q in the topology of X;
hence thesis by A3,A7,XBOOLE_1:28;
end;
suppose
Q in D;
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 = {};
then P = (U /\ [#]X) \/ {} by A3,A7,A8,XBOOLE_1:23
.= U by XBOOLE_1:28;
hence thesis by A9;
end;
end;
let x be object;
assume
A10: x in the topology of X;
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 thesis by A11,PRE_TOPC:def 4;
end;
hence h is embedding by A2,Th3;
thus One-Point_Compactification(X) is compact;
thus thesis by A1,Th2;
end;