:: Compact Spaces
:: by Agata Darmochwa{\l}
::
:: Received September 19, 1989
:: Copyright (c) 1990-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, SUBSET_1, RCOMP_1, SETFAM_1, TARSKI, FINSET_1,
XBOOLE_0, CARD_5, RELAT_1, ZFMISC_1, FUNCT_1, STRUCT_0, ORDINAL2, TOPS_2,
FUNCT_4, COMPTS_1, PARTFUN1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_3, SETFAM_1, FINSET_1, DOMAIN_1, FUNCT_4, STRUCT_0,
PRE_TOPC, TOPS_2;
constructors SETFAM_1, DOMAIN_1, FUNCT_3, FINSET_1, TOPS_2, FUNCT_4, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, PRE_TOPC,
TOPS_1;
requirements SUBSET, BOOLE;
definitions TARSKI, TOPS_2, XBOOLE_0, PRE_TOPC;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, TOPS_2, XBOOLE_0, PRE_TOPC;
theorems TARSKI, SETFAM_1, FUNCT_1, FUNCT_3, ZFMISC_1, ORDERS_1, PRE_TOPC,
TOPS_1, TOPS_2, RELAT_1, XBOOLE_0, XBOOLE_1, SUBSET_1, FUNCT_2, STRUCT_0,
FUNCT_4, RELSET_1, FINSET_1, PARTFUN1;
schemes MCART_1;
begin
reserve x, y, z for set,
T for TopStruct,
A for SubSpace of T,
P, Q for Subset of T;
definition
let T be TopStruct;
attr T is compact means
for F being Subset-Family of T st F is Cover
of T & F is open ex G being Subset-Family of T st G c= F & G is Cover of T & G
is finite;
end;
definition
let T be non empty TopSpace;
redefine attr T is regular means :: redefines regular (PRE_TOPC, definition)
for p being Point of T, P being Subset of T
st P <> {} & P is closed & p in P` ex W, V being Subset of T st W is open & V
is open & p in W & P c= V & W misses V;
compatibility
proof
thus T is regular implies for p being Point of T, P being Subset of T st P
<> {} & P is closed & p in P` ex W, V being Subset of T st W is open & V is
open & p in W & P c= V & W misses V;
assume
A1: for p being Point of T, P being Subset of T st P <> {} & P is
closed & p in P` ex W, V being Subset of T st W is open & V is open & p in W &
P c= V & W misses V;
let p being Point of T, P being Subset of T;
assume that
A2: P is closed and
A3: p in P`;
per cases;
suppose
A4: P = {};
take G1 = [#]T, G2 = {}T;
thus G1 is open & G2 is open;
thus p in G1;
thus thesis by A4;
end;
suppose
P <> {};
hence thesis by A1,A2,A3;
end;
end;
redefine attr T is normal means :: redefines normal (PRE_TOPC, definition)
for W, V being Subset of T st W <> {} & V <>
{} & W is closed & V is closed & W misses V ex P, Q being Subset of T st P is
open & Q is open & W c= P & V c= Q & P misses Q;
compatibility
proof
thus T is normal implies for W, V being Subset of T st W <> {} & V <> {} &
W is closed & V is closed & W misses V ex P, Q being Subset of T st P is open &
Q is open & W c= P & V c= Q & P misses Q;
assume
A5: for W, V being Subset of T st W <> {} & V <> {} & W is closed & V
is closed & W misses V ex P, Q being Subset of T st P is open & Q is open & W
c= P & V c= Q & P misses Q;
let F1,F2 be Subset of T such that
A6: F1 is closed and
A7: F2 is closed and
A8: F1 misses F2;
per cases;
suppose
A9: F1 = {};
take G1 = {}T, G2 = [#]T;
thus G1 is open & G2 is open;
thus F1 c= G1 by A9;
thus F2 c= G2;
thus thesis;
end;
suppose
A10: F2 = {};
take G1 = [#]T, G2 = {}T;
thus G1 is open & G2 is open;
thus F1 c= G1;
thus F2 c= G2 by A10;
thus thesis;
end;
suppose
F1 <> {} & F2 <> {};
hence thesis by A5,A6,A7,A8;
end;
end;
end;
notation
let T be TopStruct;
synonym T is Hausdorff for T is T_2;
end;
definition
let T be TopStruct, P be Subset of T;
attr P is compact means
:Def4:
for F being Subset-Family of T st F is Cover
of P & F is open ex G being Subset-Family of T st G c= F & G is Cover of P & G
is finite;
end;
registration
let T;
cluster empty -> compact for Subset of T;
coherence
proof
reconsider C = {} as Subset-Family of T by XBOOLE_1:2;
let S be Subset of T;
assume S is empty;
then
A1: S c= union C;
let F be Subset-Family of T such that
F is Cover of S and
F is open;
take C;
thus thesis by A1,SETFAM_1:def 11;
end;
end;
theorem
T is compact iff [#]T is compact;
theorem Th2:
Q c= [#] A implies (Q is compact iff for P being Subset of A st
P=Q holds P is compact )
proof
[#] A c= [#] T by PRE_TOPC:def 4;
then reconsider AA = [#] A as Subset of T;
assume
A1: Q c= [#] A;
then
A2: Q /\ AA = Q by XBOOLE_1:28;
thus Q is compact implies for P being Subset of A st P=Q holds P is compact
proof
assume
A3: Q is compact;
let P be Subset of A such that
A4: P = Q;
thus P is compact
proof
let G be Subset-Family of A;
set GG = G;
assume that
A5: G is Cover of P and
A6: G is open;
consider F being Subset-Family of T such that
A7: F is open and
A8: for AA being Subset of T st AA = [#] A holds GG=F|AA by A6,TOPS_2:39;
A9: Q c= union G by A4,A5,SETFAM_1:def 11;
union(F|AA) c= union F by TOPS_2:34;
then union G c= union F by A8;
then Q c= union F by A9;
then F is Cover of Q by SETFAM_1:def 11;
then consider F9 being Subset-Family of T such that
A10: F9 c= F and
A11: F9 is Cover of Q and
A12: F9 is finite by A3,A7;
F9|AA c= bool [#](T|AA);
then reconsider G9 = F9|AA as Subset-Family of A by PRE_TOPC:def 5;
take G9;
F9|AA c= F|AA by A10,TOPS_2:30;
hence G9 c= G by A8;
Q c= union F9 by A11,SETFAM_1:def 11;
then P c= union G9 by A2,A4,TOPS_2:32;
hence G9 is Cover of P by SETFAM_1:def 11;
thus thesis by A12,TOPS_2:36;
end;
end;
thus (for P being Subset of A st P=Q holds P is compact) implies Q is compact
proof
reconsider QQ = Q as Subset of A by A1;
assume for P being Subset of A st P=Q holds P is compact;
then
A13: QQ is compact;
thus Q is compact
proof
let F be Subset-Family of T;
set F9 = F;
assume that
A14: F is Cover of Q and
A15: F is open;
consider f being Function such that
A16: dom f = F9 and
A17: rng f = F9|AA and
A18: for x st x in F for Q being Subset of T st Q = x holds f.x = Q
/\ AA by TOPS_2:40;
F9|AA c= bool [#](T|AA);
then reconsider F9 = rng f as Subset-Family of A by A17,PRE_TOPC:def 5;
A19: F9 is open
proof
let X be Subset of A;
assume
A20: X in F9;
then reconsider Y = X as Subset of T|AA by A17;
consider R being Subset of T such that
A21: R in F and
A22: R /\ AA = Y by A17,A20,TOPS_2:def 3;
R is open by A15,A21;
then R in the topology of T;
then X in the topology of A by A22,PRE_TOPC:def 4;
hence thesis;
end;
Q c= union F by A14,SETFAM_1:def 11;
then QQ c= union F9 by A2,A17,TOPS_2:32;
then F9 is Cover of QQ by SETFAM_1:def 11;
then consider G being Subset-Family of A such that
A23: G c= F9 and
A24: G is Cover of QQ and
A25: G is finite by A13,A19;
consider X being set such that
A26: X c= dom f and
A27: X is finite and
A28: f.:X=G by A23,A25,ORDERS_1:85;
reconsider G9=X as Subset-Family of T by A16,A26,TOPS_2:2;
take G9;
Q c= union G9
proof
let x be object;
assume
A29: x in Q;
QQ c= union G by A24,SETFAM_1:def 11;
then consider Y being set such that
A30: x in Y and
A31: Y in G by A29,TARSKI:def 4;
consider z being object such that
A32: z in dom f and
A33: z in X and
A34: f.z=Y by A28,A31,FUNCT_1:def 6;
reconsider Z=z as Subset of T by A16,A32;
Y = Z /\ AA by A16,A18,A32,A34;
then x in Z by A30,XBOOLE_0:def 4;
hence thesis by A33,TARSKI:def 4;
end;
hence thesis by A16,A26,A27,SETFAM_1:def 11;
end;
end;
end;
theorem Th3:
( P = {} implies (P is compact iff T|P is compact) ) & ( T is
TopSpace-like & P <> {} implies (P is compact iff T|P is compact) )
proof
A1: [#](T|P) = P by PRE_TOPC:def 5;
thus P = {} implies (P is compact iff T|P is compact);
assume that
A2: T is TopSpace-like and
A3: P <> {};
reconsider T9 = T as non empty TopSpace by A2,A3;
reconsider P9 = P as non empty Subset of T9 by A3;
A4: [#](T9|P9) is compact iff T9|P9 is compact;
hence P is compact implies T|P is compact by A1,Th2;
assume T|P is compact;
then for Q being Subset of T|P st Q=P holds Q is compact by A4,PRE_TOPC:def 5
;
hence thesis by A1,Th2;
end;
theorem Th4:
for T being non empty TopSpace holds T is compact iff for F
being Subset-Family of T st F is centered & F is closed holds meet F <> {}
proof
let T be non empty TopSpace;
thus T is compact implies for F being Subset-Family of T st F is centered &
F is closed holds meet F <> {}
proof
assume
A1: T is compact;
let F be Subset-Family of T such that
A2: F is centered and
A3: F is closed;
reconsider C = COMPLEMENT(F) as Subset-Family of T;
assume
A4: meet F = {};
F <> {} by A2,FINSET_1:def 3;
then union COMPLEMENT(F) = (meet F)` by TOPS_2:7
.= [#] T by A4;
then
A5: COMPLEMENT(F) is Cover of T by SETFAM_1:def 11;
COMPLEMENT(F) is open by A3,TOPS_2:9;
then consider G9 being Subset-Family of T such that
A6: G9 c= C and
A7: G9 is Cover of T and
A8: G9 is finite by A1,A5;
set F9= COMPLEMENT(G9);
A9: F9 is finite by A8,TOPS_2:8;
A10: F9 c= F
proof
let X be object;
assume
A11: X in F9;
then reconsider X1=X as Subset of T;
X1` in G9 by A11,SETFAM_1:def 7;
then X1`` in F by A6,SETFAM_1:def 7;
hence thesis;
end;
G9 <> {} by A7,TOPS_2:3;
then
A12: F9 <> {} by TOPS_2:5;
meet F9 = (union G9)` by A7,TOPS_2:3,6
.= ([#] T) \ ([#] T) by A7,SETFAM_1:45
.= {} by XBOOLE_1:37;
hence contradiction by A2,A10,A9,A12,FINSET_1:def 3;
end;
assume
A13: for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {};
thus T is compact
proof
let F be Subset-Family of T such that
A14: F is Cover of T and
A15: F is open;
reconsider G=COMPLEMENT(F) as Subset-Family of T;
A16: G is closed by A15,TOPS_2:10;
F <> {} by A14,TOPS_2:3;
then
A17: G <> {} by TOPS_2:5;
meet G = (union F)` by A14,TOPS_2:3,6
.= ([#] T) \ ([#] T) by A14,SETFAM_1:45
.= {} by XBOOLE_1:37;
then not G is centered by A13,A16;
then consider G9 being set such that
A18: G9 <> {} and
A19: G9 c= G and
A20: G9 is finite and
A21: meet G9 = {} by A17,FINSET_1:def 3;
reconsider G9 as Subset-Family of T by A19,XBOOLE_1:1;
take F9=COMPLEMENT(G9);
thus F9 c= F
proof
let A be object;
assume
A22: A in F9;
then reconsider A1=A as Subset of T;
A1` in G9 by A22,SETFAM_1:def 7;
then A1`` in F by A19,SETFAM_1:def 7;
hence thesis;
end;
union F9 = (meet G9)` by A18,TOPS_2:7
.= [#] T by A21;
hence F9 is Cover of T by SETFAM_1:def 11;
thus thesis by A20,TOPS_2:8;
end;
end;
theorem
for T being non empty TopSpace holds T is compact iff for F being
Subset-Family of T st F <> {} & F is closed & meet F = {} ex G being
Subset-Family of T st G <> {} & G c= F & G is finite & meet G = {}
proof
let T be non empty TopSpace;
thus T is compact implies for F being Subset-Family of T st F <> {} & F is
closed & meet F = {} ex G being Subset-Family of T st G <> {} & G c= F & G is
finite & meet G = {}
proof
assume
A1: T is compact;
let F be Subset-Family of T such that
A2: F <> {} and
A3: F is closed and
A4: meet F = {};
not F is centered by A1,A3,A4,Th4;
then consider G being set such that
A5: G <> {} and
A6: G c= F and
A7: G is finite and
A8: meet G = {} by A2,FINSET_1:def 3;
reconsider G as Subset-Family of T by A6,XBOOLE_1:1;
take G;
thus thesis by A5,A6,A7,A8;
end;
assume
A9: for F being Subset-Family of T st F <> {} & F is closed & meet F =
{} ex G being Subset-Family of T st G <> {} & G c= F & G is finite & meet G =
{};
for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {}
proof
let F be Subset-Family of T;
assume that
A10: F is centered and
A11: F is closed;
assume
A12: meet F = {};
F <> {} by A10,FINSET_1:def 3;
then ex G being Subset-Family of T st G <> {} & G c= F & G is finite &
meet G = {} by A9,A11,A12;
hence contradiction by A10,FINSET_1:def 3;
end;
hence thesis by Th4;
end;
reserve TS for TopSpace;
reserve PS, QS for Subset of TS;
theorem Th6:
TS is T_2 implies for A being Subset of TS st A <> {} & A is
compact for p being Point of TS st p in A` ex PS,QS st PS is open & QS is open
& p in PS & A c= QS & PS misses QS
proof
assume
A1: TS is T_2;
let F be Subset of TS such that
A2: F <> {} and
A3: F is compact;
set z = the Element of F;
let a be Point of TS;
assume a in F`;
then
A4: not a in F by XBOOLE_0:def 5;
defpred P[object,object,object] means
ex PS,QS st $2=PS & $3=QS & PS is open & QS is
open & a in PS & $1 in QS & PS /\ QS = {};
A5: for x being object holds x in F implies
ex y,z being object st y in the topology of TS & z in the topology of
TS & P[x,y,z]
proof let x be object;
assume
A6: x in F;
then reconsider p=x as Point of TS;
consider W,V being Subset of TS such that
A7: W is open and
A8: V is open and
A9: a in W and
A10: p in V and
A11: W misses V by A1,A4,A6;
reconsider PS=W, QS=V as set;
take PS,QS;
thus PS in the topology of TS & QS in the topology of TS by A7,A8;
take W,V;
thus thesis by A7,A8,A9,A10,A11;
end;
consider f,g being Function such that
A12: dom f = F & dom g = F and
A13: for x being object st x in F holds P[x,f.x,g.x] from MCART_1:sch 1(A5);
g.:F c= bool the carrier of TS
proof
let x be object;
assume x in g.:F;
then consider y being object such that
y in dom g and
A14: y in F and
A15: g.y=x by FUNCT_1:def 6;
ex PS,QS st f.y=PS & g.y=QS & PS is open & QS is open & a in PS & y
in QS & PS /\ QS = {} by A13,A14;
hence thesis by A15;
end;
then reconsider C = g.:F as Subset-Family of TS;
A16: C is open
proof
let G be Subset of TS;
assume G in C;
then consider x being object such that
x in dom g and
A17: x in F and
A18: G = g.x by FUNCT_1:def 6;
ex PS,QS st f.x=PS & g.x=QS & PS is open & QS is open & a in PS & x
in QS & PS /\ QS = {} by A13,A17;
hence thesis by A18;
end;
F c= union C
proof
let x be object;
assume
A19: x in F;
then consider PS,QS such that
f.x=PS and
A20: g.x=QS and
PS is open and
QS is open and
a in PS and
A21: x in QS and
PS /\ QS = {} by A13;
QS in C by A12,A19,A20,FUNCT_1:def 6;
hence thesis by A21,TARSKI:def 4;
end;
then C is Cover of F by SETFAM_1:def 11;
then consider C9 being Subset-Family of TS such that
A22: C9 c= C and
A23: C9 is Cover of F and
A24: C9 is finite by A3,A16;
C9 c= rng g by A12,A22,RELAT_1:113;
then consider H9 being set such that
A25: H9 c= dom g and
A26: H9 is finite and
A27: g.:H9 = C9 by A24,ORDERS_1:85;
f.:H9 c= bool the carrier of TS
proof
let x be object;
assume x in f.:H9;
then consider y being object such that
y in dom f and
A28: y in H9 and
A29: f.y=x by FUNCT_1:def 6;
ex PS,QS st f.y=PS & g.y=QS & PS is open & QS is open & a in PS & y
in QS & PS /\ QS = {} by A12,A13,A25,A28;
hence thesis by A29;
end;
then reconsider B = f.:H9 as Subset-Family of TS;
take G0 = meet B, G1 = union C9;
B is open
proof
let G be Subset of TS;
assume G in B;
then consider x being object such that
A30: x in dom f and
x in H9 and
A31: G = f.x by FUNCT_1:def 6;
ex PS,QS st f.x=PS & g.x=QS & PS is open & QS is open & a in PS & x
in QS & PS /\ QS = {} by A12,A13,A30;
hence thesis by A31;
end;
hence G0 is open by A26,TOPS_2:20;
thus G1 is open by A16,A22,TOPS_2:11,19;
A32: for G being set st G in B holds a in G
proof
let G be set;
assume
A33: G in B;
then reconsider G9 = G as Subset of TS;
consider x being object such that
A34: x in dom f and
x in H9 and
A35: G9 = f.x by A33,FUNCT_1:def 6;
ex PS,QS st f.x=PS & g.x=QS & PS is open & QS is open & a in PS & x
in QS & PS /\ QS = {} by A12,A13,A34;
hence thesis by A35;
end;
F c= union C9 by A23,SETFAM_1:def 11;
then z in union C9 by A2;
then consider D being set such that
z in D and
A36: D in C9 by TARSKI:def 4;
reconsider D9 = D as Subset of TS by A36;
consider y being object such that
A37: y in dom g and
A38: y in H9 and
D9 = g.y by A27,A36,FUNCT_1:def 6;
ex PS,QS st f.y=PS & g.y=QS & PS is open & QS is open & a in PS &
y in QS & PS /\ QS = {} by A12,A13,A37;
then B <> {} by A12,A37,A38,FUNCT_1:def 6;
hence a in G0 by A32,SETFAM_1:def 1;
thus F c= G1 by A23,SETFAM_1:def 11;
thus G0 /\ G1 = {}
proof
set x = the Element of (meet B) /\ (union C9);
assume
A39: G0 /\ G1 <> {};
then
A40: x in meet B by XBOOLE_0:def 4;
x in union C9 by A39,XBOOLE_0:def 4;
then consider A being set such that
A41: x in A and
A42: A in C9 by TARSKI:def 4;
consider z being object such that
A43: z in dom g and
A44: z in H9 and
A45: A = g.z by A27,A42,FUNCT_1:def 6;
consider PS,QS such that
A46: f.z=PS and
A47: g.z=QS and
PS is open and
QS is open and
a in PS and
z in QS and
A48: PS /\ QS = {} by A12,A13,A43;
PS in B by A12,A43,A44,A46,FUNCT_1:def 6;
then x in PS by A40,SETFAM_1:def 1;
hence contradiction by A41,A45,A47,A48,XBOOLE_0:def 4;
end;
end;
theorem Th7:
TS is T_2 & PS is compact implies PS is closed
proof
assume that
A1: TS is T_2 and
A2: PS is compact;
per cases;
suppose
PS = {};
hence thesis;
end;
suppose
A3: PS <> {};
now
let a be set;
thus a in PS` implies ex Q being Subset of TS st Q is open & Q c= PS` &
a in Q
proof
assume
A4: a in PS`;
then reconsider p=a as Point of TS;
consider W,V being Subset of TS such that
A5: W is open and
V is open and
A6: p in W and
A7: PS c= V and
A8: W misses V by A1,A2,A3,A4,Th6;
take Q = W;
W misses V`` by A8;
then
A9: W c= V` by SUBSET_1:24;
V` c= PS` by A7,SUBSET_1:12;
hence thesis by A5,A6,A9;
end;
thus (ex Q being Subset of TS st Q is open & Q c= PS` & a in Q) implies
a in PS`;
end;
then PS` is open by TOPS_1:25;
hence thesis;
end;
end;
theorem Th8:
T is compact & P is closed implies P is compact
proof
assume that
A1: T is compact and
A2: P is closed;
reconsider pp = {P`} as Subset-Family of T;
let F be Subset-Family of T such that
A3: F is Cover of P and
A4: F is open;
set FP = F \/ pp;
A5: P` is open by A2;
A6: FP is open
proof
let H be Subset of T;
assume H in FP;
then H in F or H in {P`} by XBOOLE_0:def 3;
hence thesis by A4,A5,TARSKI:def 1;
end;
reconsider M = {P`} as Subset-Family of T;
(F \/ {P`}) \ {P`} = F \ {P`} by XBOOLE_1:40;
then
A7: (F \/ {P`}) \ {P`} c= F by XBOOLE_1:36;
P c= union F by A3,SETFAM_1:def 11;
then P \/ (P`) c= (union F) \/ (P`) by XBOOLE_1:9;
then [#] T c= (union F) \/ (P`) by PRE_TOPC:2;
then [#] T = (union F) \/ (P`)
.= (union F) \/ (union {P`}) by ZFMISC_1:25
.= union (F \/ {P`}) by ZFMISC_1:78;
then FP is Cover of T by SETFAM_1:def 11;
then consider G being Subset-Family of T such that
A8: G c= FP and
A9: G is Cover of T and
A10: G is finite by A1,A6;
reconsider G9 = G \ pp as Subset-Family of T;
take G9;
G9 c= (F \/ {P`}) \ {P`} by A8,XBOOLE_1:33;
hence G9 c= F by A7;
(union G) \ union M = [#] T \ (union {P`}) by A9,SETFAM_1:45
.= P`` by ZFMISC_1:25
.= P;
then P c= union G9 by TOPS_2:4;
hence G9 is Cover of P by SETFAM_1:def 11;
thus thesis by A10;
end;
theorem Th9:
PS is compact & QS c= PS & QS is closed implies QS is compact
proof
assume that
A1: PS is compact and
A2: QS c= PS and
A3: QS is closed;
per cases;
suppose
PS = {};
hence thesis by A2;
end;
suppose
PS <> {};
then TS|PS is compact by A1,Th3;
then
A4: for QQ being Subset of TS|PS st QQ=QS holds QQ is compact by A3,Th8,
TOPS_2:26;
PS = [#] (TS|PS) by PRE_TOPC:def 5;
hence thesis by A2,A4,Th2;
end;
end;
theorem
P is compact & Q is compact implies P \/ Q is compact
proof
assume that
A1: P is compact and
A2: Q is compact;
let F be Subset-Family of T such that
A3: F is Cover of (P \/ Q) and
A4: F is open;
A5: P \/ Q c= union F by A3,SETFAM_1:def 11;
Q c= P \/ Q by XBOOLE_1:7;
then Q c= union F by A5;
then F is Cover of Q by SETFAM_1:def 11;
then consider G2 being Subset-Family of T such that
A6: G2 c= F and
A7: G2 is Cover of Q and
A8: G2 is finite by A2,A4;
A9: Q c= union G2 by A7,SETFAM_1:def 11;
P c= P \/ Q by XBOOLE_1:7;
then P c= union F by A5;
then F is Cover of P by SETFAM_1:def 11;
then consider G1 being Subset-Family of T such that
A10: G1 c= F and
A11: G1 is Cover of P and
A12: G1 is finite by A1,A4;
reconsider G = G1 \/ G2 as Subset-Family of T;
take G;
thus G c= F by A10,A6,XBOOLE_1:8;
P c= union G1 by A11,SETFAM_1:def 11;
then P \/ Q c= union G1 \/ union G2 by A9,XBOOLE_1:13;
then P \/ Q c= union (G1 \/ G2) by ZFMISC_1:78;
hence G is Cover of (P \/ Q) by SETFAM_1:def 11;
thus thesis by A12,A8;
end;
theorem
TS is T_2 & PS is compact & QS is compact implies PS /\ QS is compact
proof
assume that
A1: TS is T_2 and
A2: PS is compact and
A3: QS is compact;
A4: QS is closed by A1,A3,Th7;
PS is closed by A1,A2,Th7;
hence thesis by A2,A4,Th9,XBOOLE_1:17;
end;
theorem
for TS being non empty TopSpace holds TS is T_2 & TS is compact
implies TS is regular
by Th6,Th8;
theorem
for TS being non empty TopSpace holds TS is T_2 & TS is compact
implies TS is normal
proof
let TS be non empty TopSpace;
assume that
A1: TS is T_2 and
A2: TS is compact;
let A,B be Subset of TS such that
A3: A <> {} and
A4: B <> {} and
A5: A is closed and
A6: B is closed and
A7: A /\ B = {};
defpred P[object,object,object] means
ex P,Q being Subset of TS st $2 = P & $3 = Q &
P is open & Q is open & $1 in P & B c= Q & P /\ Q = {};
A8: for x being object holds x in A implies
ex y,z being object st y in the topology of TS & z in the topology of
TS & P[x,y,z]
proof let x be object;
assume
A9: x in A;
then reconsider p=x as Point of TS;
not p in B by A7,A9,XBOOLE_0:def 4;
then p in B` by SUBSET_1:29;
then consider W,V being Subset of TS such that
A10: W is open and
A11: V is open and
A12: p in W and
A13: B c= V and
A14: W misses V by A1,A2,A4,A6,Th6,Th8;
reconsider X = W, Y = V as set;
take X,Y;
thus X in the topology of TS & Y in the topology of TS by A10,A11;
W /\ V = {} by A14;
hence thesis by A10,A11,A12,A13;
end;
consider f,g being Function such that
A15: dom f = A & dom g = A and
A16: for x being object st x in A holds P[x,f.x,g.x] from MCART_1:sch 1(A8);
f.:A c= bool the carrier of TS
proof
let x be object;
assume x in f.:A;
then consider y being object such that
y in dom f and
A17: y in A and
A18: f.y=x by FUNCT_1:def 6;
ex P,Q being Subset of TS st f.y=P & g.y=Q & P is open & Q is open &
y in P & B c= Q & P /\ Q = {} by A16,A17;
hence thesis by A18;
end;
then reconsider Cf = f.:A as Subset-Family of TS;
A c= union Cf
proof
let x be object;
assume
A19: x in A;
then consider P,Q being Subset of TS such that
A20: f.x=P and
g.x=Q and
P is open and
Q is open and
A21: x in P and
B c= Q and
P /\ Q = {} by A16;
P in Cf by A15,A19,A20,FUNCT_1:def 6;
hence thesis by A21,TARSKI:def 4;
end;
then
A22: Cf is Cover of A by SETFAM_1:def 11;
A23: Cf is open
proof
let G be Subset of TS;
assume G in Cf;
then consider x being object such that
x in dom f and
A24: x in A and
A25: G = f.x by FUNCT_1:def 6;
ex P,Q being Subset of TS st f.x=P & g.x=Q & P is open & Q is open &
x in P & B c= Q & P /\ Q = {} by A16,A24;
hence thesis by A25;
end;
A is compact by A2,A5,Th8;
then consider C being Subset-Family of TS such that
A26: C c= Cf and
A27: C is Cover of A and
A28: C is finite by A22,A23;
set z = the Element of A;
A c= union C by A27,SETFAM_1:def 11;
then z in union C by A3;
then consider D being set such that
z in D and
A29: D in C by TARSKI:def 4;
C c= rng f by A15,A26,RELAT_1:113;
then consider H9 being set such that
A30: H9 c= dom f and
A31: H9 is finite and
A32: f.:H9 = C by A28,ORDERS_1:85;
g.:H9 c= bool the carrier of TS
proof
let x be object;
assume x in g.:H9;
then consider y being object such that
y in dom g and
A33: y in H9 and
A34: g.y=x by FUNCT_1:def 6;
ex P,Q being Subset of TS st f.y=P & g.y=Q & P is open & Q is open &
y in P & B c= Q & P /\ Q = {} by A15,A16,A30,A33;
hence thesis by A34;
end;
then reconsider Bk = g.:H9 as Subset-Family of TS;
consider y being object such that
A35: y in dom f and
A36: y in H9 and
D = f.y by A32,A29,FUNCT_1:def 6;
A37: for X being set st X in Bk holds B c= X
proof
let X be set;
assume
A38: X in Bk;
then reconsider X9 = X as Subset of TS;
consider x being object such that
A39: x in dom g and
x in H9 and
A40: X9 = g.x by A38,FUNCT_1:def 6;
ex P,Q being Subset of TS st f.x = P & g.x = Q & P is open & Q is
open & x in P & B c= Q & P /\ Q = {} by A15,A16,A39;
hence thesis by A40;
end;
take W = union C, V = meet Bk;
thus W is open by A23,A26,TOPS_2:11,19;
Bk is open
proof
let G be Subset of TS;
assume G in Bk;
then consider x being object such that
A41: x in dom g and
x in H9 and
A42: G = g.x by FUNCT_1:def 6;
ex P,Q being Subset of TS st f.x = P & g.x = Q & P is open & Q is
open & x in P & B c= Q & P /\ Q = {} by A15,A16,A41;
hence thesis by A42;
end;
hence V is open by A31,TOPS_2:20;
thus A c= W by A27,SETFAM_1:def 11;
ex P,Q being Subset of TS st f.y = P & g.y = Q & P is open & Q is
open & y in P & B c= Q & P /\ Q = {} by A15,A16,A35;
then Bk <> {} by A15,A35,A36,FUNCT_1:def 6;
hence B c= V by A37,SETFAM_1:5;
thus W /\ V = {}
proof
set x = the Element of (union C) /\ (meet Bk);
assume
A43: W /\ V <> {};
then
A44: x in meet Bk by XBOOLE_0:def 4;
x in (union C) by A43,XBOOLE_0:def 4;
then consider D being set such that
A45: x in D and
A46: D in C by TARSKI:def 4;
consider z being object such that
A47: z in dom f and
A48: z in H9 and
A49: D = f.z by A32,A46,FUNCT_1:def 6;
consider P,Q being Subset of TS such that
A50: f.z = P and
A51: g.z = Q and
P is open and
Q is open and
z in P and
B c= Q and
A52: P /\ Q = {} by A15,A16,A47;
Q in Bk by A15,A47,A48,A51,FUNCT_1:def 6;
then x in Q by A44,SETFAM_1:def 1;
hence contradiction by A45,A49,A50,A52,XBOOLE_0:def 4;
end;
end;
reserve S for non empty TopStruct;
reserve f for Function of T,S;
theorem
T is compact & f is continuous & rng f = [#] S implies S is compact
proof
assume
A1: T is compact;
[#] T c= dom f by FUNCT_2:def 1;
then
A2: [#] T c= f"(f.:([#] T)) by FUNCT_1:76;
assume that
A3: f is continuous and
A4: rng f = [#] S;
let F be Subset-Family of S such that
A5: F is Cover of S and
A6: F is open;
set F1=F;
reconsider G = ("f).:F1 as Subset-Family of T by TOPS_2:42;
union G = f"(union F) by A4,FUNCT_3:26
.= f"(rng f) by A4,A5,SETFAM_1:45
.= f"(f.: (dom f)) by RELAT_1:113
.= f"(f.:([#] T)) by FUNCT_2:def 1;
then
A7: G is Cover of T by A2,SETFAM_1:def 11;
A8: (.:f).:((.:f)"F) c= F by FUNCT_1:75;
(.:f).:(("f).:F) c= (.:f).:((.:f)"F) by FUNCT_3:29,RELAT_1:123;
then
A9: (.:f).:G c= F by A8;
G is open by A3,A6,TOPS_2:47;
then consider G9 being Subset-Family of T such that
A10: G9 c= G and
A11: G9 is Cover of T and
A12: G9 is finite by A1,A7;
reconsider F9=(.:f).:G9 as Subset-Family of S;
take F9;
(.:f).:G9 c= (.:f).:G by A10,RELAT_1:123;
hence F9 c= F by A9;
dom f = [#] T by FUNCT_2:def 1;
then union F9 = f.:(union G9) by FUNCT_3:14
.= f.:([#] T) by A11,SETFAM_1:45
.= f.:dom f by FUNCT_2:def 1
.= [#] S by A4,RELAT_1:113;
hence F9 is Cover of S by SETFAM_1:def 11;
thus thesis by A12;
end;
theorem Th15:
f is continuous & rng f = [#] S & P is compact implies f.:P is compact
proof
assume that
A1: f is continuous and
A2: rng f = [#] S and
A3: P is compact;
let F be Subset-Family of S such that
A4: F is Cover of f.:P and
A5: F is open;
reconsider G = ("f).:F as Subset-Family of T by TOPS_2:42;
f.:P c= union F by A4,SETFAM_1:def 11;
then
A6: f"(f.:P) c= f"(union F) by RELAT_1:143;
P c= [#] T;
then P c= dom f by FUNCT_2:def 1;
then
A7: P c= f"(f.:P) by FUNCT_1:76;
union G = f"(union F) by A2,FUNCT_3:26;
then P c= union G by A6,A7;
then
A8: G is Cover of P by SETFAM_1:def 11;
G is open by A1,A5,TOPS_2:47;
then consider G9 being Subset-Family of T such that
A9: G9 c= G and
A10: G9 is Cover of P and
A11: G9 is finite by A3,A8;
reconsider F9= (.:f).:G9 as Subset-Family of S;
take F9;
A12: (.:f).:((.:f)"F) c= F by FUNCT_1:75;
(.:f).:(("f).:F) c= (.:f).:((.:f)"F) by FUNCT_3:29,RELAT_1:123;
then
A13: (.:f).:G c= F by A12;
(.:f).:G9 c= (.:f).:G by A9,RELAT_1:123;
hence F9 c= F by A13;
A14: P c= union G9 by A10,SETFAM_1:def 11;
dom f = [#] T by FUNCT_2:def 1;
then union F9 = f.:(union G9) by FUNCT_3:14;
then f.:P c= union F9 by A14,RELAT_1:123;
hence F9 is Cover of f.:P by SETFAM_1:def 11;
thus thesis by A11;
end;
reserve SS for non empty TopSpace;
reserve f for Function of TS,SS;
theorem Th16:
TS is compact & SS is T_2 & rng f = [#] SS & f is continuous
implies for PS st PS is closed holds f.:PS is closed
proof
assume that
A1: TS is compact and
A2: SS is T_2 and
A3: rng f = [#] SS and
A4: f is continuous;
let PS;
assume PS is closed;
then PS is compact by A1,Th8;
hence thesis by A2,A3,A4,Th7,Th15;
end;
theorem
TS is compact & SS is T_2 & rng f = [#]SS & f is
one-to-one & f is continuous implies f is being_homeomorphism
proof
assume that
A1: TS is compact and
A2: SS is T_2 and
A3: rng f = [#] SS and
A4: f is one-to-one and
A5: f is continuous;
A6: dom f = [#]TS by FUNCT_2:def 1;
for P being Subset of TS holds P is closed iff f.:P is closed
proof
let P be Subset of TS;
A7: P c= f"(f.:P) by A6,FUNCT_1:76;
thus P is closed implies f.:P is closed by A1,A2,A3,A5,Th16;
assume f.:P is closed;
then
A8: f"(f.:P) is closed by A5;
f"(f.:P) c= P by A4,FUNCT_1:82;
hence thesis by A8,A7,XBOOLE_0:def 10;
end;
hence thesis by A6,A3,A4,TOPS_2:58;
end;
definition
let D be set;
func 1TopSp D -> TopStruct equals
TopStruct (# D, [#] bool D #);
coherence;
end;
registration
let D be set;
cluster 1TopSp D -> strict TopSpace-like;
coherence
by ZFMISC_1:def 1;
end;
registration
let D be non empty set;
cluster 1TopSp D -> non empty;
coherence;
end;
registration
let x be set;
cluster 1TopSp {x} -> T_2;
coherence
proof
let p, q be Point of 1TopSp {x};
assume
A1: p <> q;
p = x by TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
end;
registration
cluster T_2 non empty for TopSpace;
existence
proof
take 1TopSp {{}};
thus thesis;
end;
end;
registration
let T be T_2 non empty TopSpace;
cluster compact -> closed for Subset of T;
coherence by Th7;
end;
registration
let A be finite set;
cluster 1TopSp A -> finite;
coherence;
end;
registration
cluster non empty finite strict for TopSpace;
existence
proof
take 1TopSp {{}};
thus thesis;
end;
end;
registration
cluster finite -> compact for TopSpace;
coherence;
end;
theorem
for T being TopSpace st the carrier of T is finite holds T is compact;
registration
let T be TopSpace;
cluster finite -> compact for Subset of T;
coherence
proof
let A be Subset of T;
assume A is finite;
then reconsider B = A as finite Subset of T;
[#](T|B) = B by PRE_TOPC:def 5;
then
A1: T|B is compact;
B = {} or B <> {};
hence thesis by A1,Th3;
end;
end;
registration
let T be non empty TopSpace;
cluster non empty compact for Subset of T;
existence
proof
set A = the finite non empty Subset of T;
take A;
thus thesis;
end;
end;
:: comp. TOPMETR:3, 2008.07.06, A.T.
registration
cluster empty -> T_2 for TopStruct;
coherence
by STRUCT_0:def 10;
end;
registration
let T be T_2 TopStruct;
cluster -> T_2 for SubSpace of T;
coherence
proof
let A be SubSpace of T;
per cases;
suppose
A is empty;
hence thesis;
end;
suppose
A1: A is non empty;
let p,q be Point of A such that
A2: not p = q;
[#]A c= [#]T by PRE_TOPC:def 4;
then T is non empty by A1;
then reconsider p9 = p, q9 = q as Point of T by A1,PRE_TOPC:25;
consider W,V being Subset of T such that
A3: W is open and
A4: V is open and
A5: p9 in W and
A6: q9 in V and
A7: W misses V by A2,PRE_TOPC:def 10;
reconsider W9 = W /\ [#] A, V9 = V /\ [#] A as Subset of A;
V in the topology of T by A4;
then
A8: V9 in the topology of A by PRE_TOPC:def 4;
take W9, V9;
W in the topology of T by A3;
then W9 in the topology of A by PRE_TOPC:def 4;
hence W9 is open & V9 is open by A8;
thus p in W9 & q in V9 by A1,A5,A6,XBOOLE_0:def 4;
A9: W /\ V = {} by A7;
W9 /\ V9 = W /\ (V /\ [#] A) /\ [#] A by XBOOLE_1:16
.= {} /\ [#] A by A9,XBOOLE_1:16
.= {};
hence thesis;
end;
end;
end;
:: from BORSUK_1, 2008.07.07, A.T.
theorem Th19:
for X being TopStruct for Y being SubSpace of X, A being Subset
of X, B being Subset of Y st A = B holds A is compact iff B is compact
proof
let X be TopStruct;
let Y be SubSpace of X, A be Subset of X, B be Subset of Y such that
A1: A = B;
A2: B c= [#] Y;
hence A is compact implies B is compact by A1,Th2;
assume B is compact;
then for P being Subset of Y st P = A holds P is compact by A1;
hence thesis by A1,A2,Th2;
end;
:: from TOPMETR2, 2008.07.07, A.T.
reserve T, S for non empty TopSpace,
p for Point of T;
Lm1:
for X being set
for T1,T2 being SubSpace of T,
f being Function of T1,S, g being Function of T2,S
st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X &
T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous
& f|X tolerates g|X holds f+*g is continuous Function of T,S
proof
let X be set;
let T1,T2 be SubSpace of T, f be Function of T1,S, g be Function of T2,S;
assume that
A1: ([#] T1) \/ ([#] T2) = [#] T and
A2: ([#] T1) /\ ([#] T2) = X and
A3: T1 is compact and
A4: T2 is compact and
A5: T is T_2 and
A6: f is continuous and
A7: g is continuous and
A8: f|X tolerates g|X;
set h = f+*g;
A9: dom g = [#] T2 by FUNCT_2:def 1;
rng h c= rng f \/ rng g by FUNCT_4:17;
then
A10: rng h c= the carrier of S by XBOOLE_1:1;
A11: dom f = [#] T1 by FUNCT_2:def 1;
then dom h = the carrier of T by A1,A9,FUNCT_4:def 1;
then reconsider h as Function of T,S by A10,FUNCT_2:def 1,RELSET_1:4;
for P being Subset of S st P is closed holds h"P is closed
proof
let P be Subset of S;
[#] T1 c= [#] T by A1,XBOOLE_1:7;
then reconsider P1 = f"P as Subset of T by XBOOLE_1:1;
[#] T2 c= [#] T by A1,XBOOLE_1:7;
then reconsider P2 = g"P as Subset of T by XBOOLE_1:1;
A12: dom h = dom f \/ dom g by FUNCT_4:def 1;
A13: now
let x be object;
thus x in h"P /\ [#] T2 implies x in g"P
proof
assume
A14: x in h"P /\ [#] T2;
then x in h"P by XBOOLE_0:def 4;
then
A15: h.x in P by FUNCT_1:def 7;
g.x = h.x by A9,A14,FUNCT_4:13;
hence thesis by A9,A14,A15,FUNCT_1:def 7;
end;
assume
A16: x in g"P;
then
A17: x in dom g by FUNCT_1:def 7;
g.x in P by A16,FUNCT_1:def 7;
then
A18: h.x in P by A17,FUNCT_4:13;
x in dom h by A12,A17,XBOOLE_0:def 3;
then x in h"P by A18,FUNCT_1:def 7;
hence x in h"P /\ [#] T2 by A16,XBOOLE_0:def 4;
end;
A19: for x being set st x in [#] T1 holds h.x = f.x
proof
let x be set such that
A20: x in [#] T1;
A21: dom g = the carrier of T2 by FUNCT_2:def 1;
per cases;
suppose
A22: x in [#] T2;
then x in [#] T1 /\ [#] T2 by A20,XBOOLE_0:def 4;
then
A23: x in X by A2;
then
A24: (f|X).x = f.x & (g|X).x = g.x by FUNCT_1:49;
x in dom(f|X) & x in dom(g|X) by A11,A20,A21,A22,A23,RELAT_1:57;
then x in dom(f|X) /\ dom(g|X) by XBOOLE_0:def 4;
then (f|X).x = (g|X).x by A8,PARTFUN1:def 4;
hence thesis by A9,A22,A24,FUNCT_4:13;
end;
suppose not x in [#] T2;
hence thesis by A9,FUNCT_4:11;
end;
end;
now
let x be object;
thus x in h"P /\ [#] T1 implies x in f"P
proof
assume
A25: x in h"P /\ [#] T1;
then x in h"P by XBOOLE_0:def 4;
then
A26: h.x in P by FUNCT_1:def 7;
f.x = h.x by A19,A25;
hence thesis by A11,A25,A26,FUNCT_1:def 7;
end;
assume
A27: x in f"P;
then x in dom f by FUNCT_1:def 7;
then
A28: x in dom h by A12,XBOOLE_0:def 3;
f.x in P by A27,FUNCT_1:def 7;
then h.x in P by A19,A27;
then x in h"P by A28,FUNCT_1:def 7;
hence x in h"P /\ [#] T1 by A27,XBOOLE_0:def 4;
end;
then
A29: h"P /\ [#] T1 = f"P by TARSKI:2;
assume
A30: P is closed;
then f"P is closed by A6;
then f"P is compact by A3,Th8;
then
A31: P1 is compact by Th19;
g"P is closed by A7,A30;
then g"P is compact by A4,Th8;
then
A32: P2 is compact by Th19;
h"P = h"P /\ ([#] T1 \/ [#] T2) by A11,A9,A12,RELAT_1:132,XBOOLE_1:28
.= (h"P /\ [#](T1)) \/ (h"P /\ [#](T2)) by XBOOLE_1:23;
then h"P = f"P \/ g"P by A29,A13,TARSKI:2;
hence thesis by A5,A31,A32;
end;
hence thesis by PRE_TOPC:def 6;
end;
theorem
for T1,T2 being SubSpace of T,
f being Function of T1,S, g being Function of T2,S
st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} &
T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous
& f.p = g.p holds f+*g is continuous Function of T,S
proof
let T1,T2 be SubSpace of T, f be Function of T1,S, g be Function of T2,S;
assume
A1: ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} &
T1 is compact & T2 is compact & T is T_2 & f is continuous &
g is continuous;
assume f.p = g.p;
then f|{p} tolerates g|{p} by PARTFUN1:81;
hence thesis by A1,Lm1;
end;
theorem
for T being non empty TopSpace, T1, T2 being SubSpace of T,
p1,p2 being Point of T
for f being Function of T1,S, g being Function of T2,S st
([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} &
T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous
& f.p1 = g.p1 & f.p2 = g.p2 holds f+*g is continuous Function of T,S
proof
let T be non empty TopSpace, T1, T2 be SubSpace of T, p1,p2 be Point of T;
let f be Function of T1,S, g be Function of T2,S;
assume
A1: ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} &
T1 is compact & T2 is compact & T is T_2 & f is continuous &
g is continuous;
assume f.p1 = g.p1 & f.p2 = g.p2;
then f|{p1,p2} tolerates g|{p1,p2} by PARTFUN1:82;
hence thesis by A1,Lm1;
end;
begin :: Addenda, the 2009.03 revision, A.T.
registration
let S be TopStruct;
cluster the topology of S -> open;
coherence
proof
let P be Subset of S;
thus thesis;
end;
end;
:: TOPGEN_2, A.T. 2009.03.15
registration
let T be TopSpace;
cluster open non empty for Subset-Family of T;
existence
proof
take the topology of T;
thus thesis;
end;
end;
theorem Th22:
for T being non empty TopSpace, F being set holds F is open
Subset-Family of T iff F is open Subset-Family of the TopStruct of T
proof
let T be non empty TopSpace, F be set;
thus F is open Subset-Family of T implies F is open Subset-Family of the
TopStruct of T
proof
assume
A1: F is open Subset-Family of T;
then reconsider F as Subset-Family of the TopStruct of T;
F is open
by A1,TOPS_2:def 1,PRE_TOPC:30;
hence thesis;
end;
assume
A2: F is open Subset-Family of the TopStruct of T;
then reconsider F as Subset-Family of T;
F is open
by A2,TOPS_2:def 1,PRE_TOPC:30;
hence thesis;
end;
theorem
for T being non empty TopSpace, X being set holds
X is compact Subset of T iff X is compact Subset of the TopStruct of T
proof
let T be non empty TopSpace, X being set;
thus X is compact Subset of T implies X is compact Subset of the TopStruct
of T
proof
assume
A1: X is compact Subset of T;
then reconsider Z=X as Subset of the TopStruct of T;
Z is compact by Th22,A1,Def4;
hence thesis;
end;
assume
A2: X is compact Subset of the TopStruct of T;
then reconsider Z = X as Subset of T;
Z is compact by Th22,A2,Def4;
hence thesis;
end;
theorem
for X being set
for T1,T2 being SubSpace of T,
f being Function of T1,S, g being Function of T2,S
st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X &
T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous
& f|X tolerates g|X holds f+*g is continuous Function of T,S by Lm1;