Copyright (c) 1992 Association of Mizar Users
environ
vocabulary BOOLE, PRE_TOPC, SUBSET_1, RELAT_1, TARSKI, SETFAM_1, CONNSP_1,
TSEP_1;
notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, CONNSP_1, BORSUK_1;
constructors CONNSP_1, BORSUK_1, MEMBERED;
clusters PRE_TOPC, BORSUK_1, STRUCT_0, COMPLSP1, SUBSET_1, TOPS_1, MEMBERED,
ZFMISC_1;
requirements BOOLE, SUBSET;
definitions PRE_TOPC;
theorems PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, BORSUK_1, SUBSET_1, XBOOLE_0,
XBOOLE_1;
begin
Lm1: for A being set for B,C,D being Subset of A st B \ C = {}
holds B misses (D \ C)
proof let A be set; let B,C,D be Subset of A;
assume B \ C = {}; then B c= C & C misses (D \ C) by XBOOLE_1:37,79;
hence thesis by XBOOLE_1:63;
end;
Lm2: for A being set for B,C,D being Subset of A st B misses C
holds B misses (C \ D)
proof let A be set; let B,C,D be Subset of A;
assume B misses C; then C \ D c= C & C misses B by XBOOLE_1:36;
hence thesis by XBOOLE_1:63;
end;
Lm3: for A,B,C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)
proof let A,B,C be set;
A1: A \ C c= A by XBOOLE_1:36;
A2: (A \ C) misses C by XBOOLE_1:79;
thus (A /\ B) \ C = (A \ C) /\ B by XBOOLE_1:49
.= (A \ C) \ ((A \ C) \ B) by XBOOLE_1:48
.= (A \ C) \ (A \ (C \/ B)) by XBOOLE_1:41
.= ((A \ C) \ A) \/ ((A \ C) /\ (C \/ B)) by XBOOLE_1:52
.= {} \/ ((A \ C) /\ (C \/ B)) by A1,XBOOLE_1:37
.= (A \ C) /\ ((B \ C) \/ C) by XBOOLE_1:39
.= (A \ C) /\ (B \ C) \/ (A \ C) /\ C by XBOOLE_1:23
.= (A \ C) /\ (B \ C) \/ {} by A2,XBOOLE_0:def 7
.= (A \ C) /\ (B \ C);
end;
::1. Some Properties of Subspaces of Topological Spaces.
reserve X for TopSpace;
theorem Th1:
for X being TopStruct, X0 being SubSpace of X holds the carrier of X0
is Subset of X
proof let X be TopStruct, X0 be SubSpace of X;
reconsider A = [#]X0 as Subset of [#]X by PRE_TOPC:def 9;
A c= [#]X & [#]X0 = the carrier of X0 by PRE_TOPC:12;
hence thesis by PRE_TOPC:16;
end;
theorem Th2:
for X being TopStruct holds X is SubSpace of X
proof
let X be TopStruct;
thus [#]X c= [#]X;
thus for P being Subset of X holds P in the topology of X iff
ex Q being Subset of X
st Q in the topology of X & P = Q /\ [#]X
proof let P be Subset of X;
thus P in the topology of X implies
ex Q being Subset of X st
Q in the topology of X & P = Q /\ [#]X
proof assume A1: P in the topology of X;
take P;
thus thesis by A1,PRE_TOPC:15;
end;
thus thesis by PRE_TOPC:15;
end;
end;
theorem
for X being strict TopStruct holds X|[#]X = X
proof let X be strict TopStruct;
reconsider X0 = X as SubSpace of X by Th2;
reconsider P = [#]X0 as Subset of X;
X|P = X0 by PRE_TOPC:def 10;
hence thesis;
end;
theorem Th4:
for X1, X2 being SubSpace of X holds
the carrier of X1 c= the carrier of X2 iff X1 is SubSpace of X2
proof let X1, X2 be SubSpace of X;
set A1 = the carrier of X1, A2 = the carrier of X2;
A1: A1 = [#]X1 & A2 = [#]X2 & (the carrier of X) = [#]X by PRE_TOPC:12;
thus the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2
proof assume A2: A1 c= A2;
for P being Subset of X1 holds P in the topology of X1 iff
ex Q being Subset of X2 st Q in the topology of X2 &
P = Q /\ A1
proof let P be Subset of X1;
thus P in the topology of X1 implies
ex Q being Subset of X2 st
Q in the topology of X2 & P = Q /\ A1
proof assume P in the topology of X1;
then consider R being Subset of X such that
A3: R in the topology of X and A4: P = R /\ A1 by A1,PRE_TOPC:def 9;
reconsider Q = R /\ A2 as Subset of X2 by XBOOLE_1:17;
take Q;
thus Q in the topology of X2 by A1,A3,PRE_TOPC:def 9;
Q /\ A1 = R /\ (A2 /\ A1) by XBOOLE_1:16
.= R /\ A1 by A2,XBOOLE_1:28;
hence thesis by A4;
end;
given Q being Subset of X2 such that
A5: Q in the topology of X2 and A6: P = Q /\ A1;
consider R being Subset of X such that
A7: R in the topology of X and A8: Q = R /\ [#]X2 by A5,PRE_TOPC:def 9;
P = R /\ (A2 /\ A1) by A1,A6,A8,XBOOLE_1:16
.= R /\ A1 by A2,XBOOLE_1:28;
hence thesis by A1,A7,PRE_TOPC:def 9;
end;
hence thesis by A1,A2,PRE_TOPC:def 9;
end;
thus X1 is SubSpace of X2 implies the carrier of X1 c= the carrier of X2
by A1,PRE_TOPC:def 9;
end;
Lm4:
for X being TopStruct, X0 being SubSpace of X holds
the TopStruct of X0 is strict SubSpace of X
proof let X be TopStruct, X0 be SubSpace of X;
set S = the TopStruct of X0;
S is SubSpace of X
proof
A1: [#](S) = the carrier of S & [#]
(X0) = the carrier of X0 by PRE_TOPC:12;
hence [#](S) c= [#](X) by PRE_TOPC:def 9;
let P be Subset of S;
thus P in
the topology of S implies ex Q being Subset of X st
Q in the topology of X & P = Q /\ [#](S) by A1,PRE_TOPC:def 9;
given Q being Subset of X such that
A2: Q in the topology of X & P = Q /\ [#](S);
thus P in the topology of S by A1,A2,PRE_TOPC:def 9;
end;
hence thesis;
end;
theorem Th5:
for X being TopStruct
for X1, X2 being SubSpace of X
st the carrier of X1 = the carrier of X2
holds the TopStruct of X1 = the TopStruct of X2
proof
let X be TopStruct;
let X1, X2 be SubSpace of X;
set A1 = the carrier of X1, A2 = the carrier of X2;
assume A1: A1 = A2;
reconsider S1 = the TopStruct of X1, S2 = the TopStruct of X2
as strict SubSpace of X by Lm4;
A2: A1 = [#]S1 & A2 = [#]S2 by PRE_TOPC:12;
reconsider A1, A2 as Subset of X by BORSUK_1:35;
S1 = X|(A1) & X|(A2) = S2 by A2,PRE_TOPC:def 10;
hence thesis by A1;
end;
theorem
for X1, X2 being SubSpace of X st
X1 is SubSpace of X2 & X2 is SubSpace of X1 holds
the TopStruct of X1 = the TopStruct of X2
proof let X1,X2 be SubSpace of X;
set A1 = the carrier of X1, A2 = the carrier of X2;
assume X1 is SubSpace of X2 & X2 is SubSpace of X1;
then A1 c= A2 & A2 c= A1 by Th4;
then A1 = A2 by XBOOLE_0:def 10;
hence thesis by Th5;
end;
theorem Th7:
for X1 being SubSpace of X for X2 being SubSpace of X1
holds X2 is SubSpace of X
proof let X1 be SubSpace of X; let X2 be SubSpace of X1;
A1: [#]X1 c= [#]X & [#]X2 c= [#]X1 by PRE_TOPC:def 9;
hence [#](X2) c= [#](X) by XBOOLE_1:1;
thus for P being Subset of X2 holds P in
the topology of X2 iff
ex Q being Subset of X
st Q in the topology of X & P = Q /\ [#]X2
proof let P be Subset of X2;
reconsider P1 = P as Subset of X2;
thus P in the topology of X2 implies
ex Q being Subset of X
st Q in the topology of X & P = Q /\ [#]X2
proof assume P in the topology of X2;
then consider R being Subset of X1 such that
A2: R in the topology of X1 and A3: P = R /\ [#]X2 by PRE_TOPC:def 9;
consider Q being Subset of X such that
A4: Q in the topology of X and A5: R = Q /\ [#]X1 by A2,PRE_TOPC:def 9;
Q /\ [#]X2 = Q /\ ([#]X1 /\ [#]X2) by A1,XBOOLE_1:28
.= P by A3,A5,XBOOLE_1:16;
hence thesis by A4;
end;
given Q being Subset of X such that
A6: Q in the topology of X and A7: P = Q /\ [#]X2;
reconsider Q1 = Q as Subset of X;
A8: Q1 is open by A6,PRE_TOPC:def 5;
Q /\ [#]X1 c= [#]X1 & [#]X1 = the carrier of X1 by PRE_TOPC:12,
XBOOLE_1:17;
then reconsider R = Q /\ [#]X1 as Subset of X1;
A9: R is open by A8,TOPS_2:32;
R /\ [#]X2 = Q /\ ([#]X1 /\ [#]X2) by XBOOLE_1:16
.= P by A1,A7,XBOOLE_1:28;
then P1 is open by A9,TOPS_2:32;
hence thesis by PRE_TOPC:def 5;
end;
end;
theorem Th8:
for X0 being SubSpace of X, C, A being Subset of X,
B being Subset of X0 st
C is closed & C c= the carrier of X0 & A c= C & A = B holds
B is closed iff A is closed
proof
let X0 be SubSpace of X, C, A be Subset of X,
B be Subset of X0 such that
A1: C is closed and A2: C c= the carrier of X0 and A3: A c= C and A4: A = B;
thus B is closed implies A is closed
proof assume B is closed;
then consider F being Subset of X such that
A5: F is closed and A6: F /\ [#]X0 = B by PRE_TOPC:43;
[#]X0 = the carrier of X0 by PRE_TOPC:12;
then A7: F /\ C c= A by A2,A4,A6,XBOOLE_1:26;
A c= F by A4,A6,XBOOLE_1:17;
then A c= F /\ C by A3,XBOOLE_1:19;
then A = F /\ C by A7,XBOOLE_0:def 10;
hence A is closed by A1,A5,TOPS_1:35;
end;
thus A is closed implies B is closed by A4,TOPS_2:34;
end;
theorem Th9:
for X0 being SubSpace of X, C, A being Subset of X,
B being Subset of X0 st
C is open & C c= the carrier of X0 & A c= C & A = B holds
B is open iff A is open
proof
let X0 be SubSpace of X, C, A be Subset of X,
B be Subset of X0 such that
A1: C is open and A2: C c= the carrier of X0 and A3: A c= C and A4: A = B;
thus B is open implies A is open
proof assume B is open;
then consider F being Subset of X such that
A5: F is open and A6: F /\ [#]X0 = B by TOPS_2:32;
[#]X0 = the carrier of X0 by PRE_TOPC:12;
then A7: F /\ C c= A by A2,A4,A6,XBOOLE_1:26;
A c= F by A4,A6,XBOOLE_1:17;
then A c= F /\ C by A3,XBOOLE_1:19;
then A = F /\ C by A7,XBOOLE_0:def 10;
hence A is open by A1,A5,TOPS_1:38;
end;
thus A is open implies B is open by A4,TOPS_2:33;
end;
theorem Th10:
for X being non empty TopStruct, A0 being non empty Subset of X
ex X0 being strict non empty SubSpace of X st A0 = the carrier of X0
proof let X be non empty TopStruct,
A0 be non empty Subset of X;
take X0 = X|A0;
A0 = [#]X0 by PRE_TOPC:def 10;
hence thesis by PRE_TOPC:12;
end;
::Properties of Closed Subspaces (for the definition see BORSUK_1:def 13).
theorem Th11:
for X0 being SubSpace of X, A being Subset of X
st A = the carrier of X0 holds
X0 is closed SubSpace of X iff A is closed
proof let X0 be SubSpace of X, A be Subset of X;
assume A1: A = the carrier of X0;
hence X0 is closed SubSpace of X implies A is closed by BORSUK_1:def 14;
thus A is closed implies X0 is closed SubSpace of X
proof assume A is closed;
then for B be Subset of X
holds B = the carrier of X0 implies B is closed by A1;
hence thesis by BORSUK_1:def 14;
end;
end;
theorem
for X0 being closed SubSpace of X,
A being Subset of X,
B being Subset of X0
st A = B holds B is closed iff A is closed
proof
let X0 be closed SubSpace of X, A be Subset of X,
B be Subset of X0 such that
A1: A = B;
the carrier of X0 is Subset of X by Th1;
then reconsider C = the carrier of X0 as Subset of X;
C is closed by Th11;
hence thesis by A1,Th8;
end;
theorem
for X1 being closed SubSpace of X,
X2 being closed SubSpace of X1 holds
X2 is closed SubSpace of X
proof let X1 be closed SubSpace of X,
X2 be closed SubSpace of X1;
now let B be Subset of X;
A1: the carrier of X2 c= the carrier of X1 by BORSUK_1:35;
assume A2: B = the carrier of X2;
then reconsider BB = B as Subset of X1 by A1;
BB is closed by A2,BORSUK_1:def 14;
then A3: ex A being Subset of X st
A is closed & A /\ [#]X1 = BB by PRE_TOPC:43;
A4: [#]X1 = the carrier of X1 by PRE_TOPC:12;
then [#]X1 is Subset of X by BORSUK_1:35;
then reconsider C = [#]X1 as Subset of X;
C is closed by A4,BORSUK_1:def 14;
hence B is closed by A3,TOPS_1:35;
end;
hence thesis by Th7,BORSUK_1:def 14;
end;
theorem
for X being non empty TopSpace, X1 being closed non empty SubSpace of X,
X2 being non empty SubSpace of X st
the carrier of X1 c= the carrier of X2 holds
X1 is closed non empty SubSpace of X2
proof let X be non empty TopSpace, X1 be closed non empty SubSpace of X,
X2 be non empty SubSpace of X;
assume the carrier of X1 c= the carrier of X2;
then reconsider B = the carrier of X1 as Subset of X2;
now let C be Subset of X2; assume A1: C = the carrier of X1;
then C is Subset of X by BORSUK_1:35;
then reconsider A = C as Subset of X;
A2: A is closed by A1,Th11;
[#]X2 = the carrier of X2 by PRE_TOPC:12;
then A /\ [#]X2 = C by XBOOLE_1:28;
hence C is closed by A2,PRE_TOPC:43;
end;
then B is closed;
hence thesis by Th4,Th11;
end;
theorem Th15:
for X be non empty TopSpace, A0 being non empty Subset of X st A0 is closed
ex X0 being strict closed non empty SubSpace of X st A0 = the carrier of X0
proof let X be non empty TopSpace, A0 be non empty Subset of X such that
A1: A0 is closed;
consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by Th10;
reconsider Y0 = X0 as strict closed non empty SubSpace of X by A1,A2,Th11;
take Y0;
thus thesis by A2;
end;
definition let X be TopStruct;
let IT be SubSpace of X;
attr IT is open means
:Def1: for A being Subset of X st A = the carrier of IT holds A is open;
end;
Lm5:
for T being TopStruct holds
the TopStruct of T is SubSpace of T
proof let T be TopStruct;
set S = the TopStruct of T;
[#]S = the carrier of S by PRE_TOPC:12;
hence [#]S c= [#]T by PRE_TOPC:12;
let P be Subset of S;
hereby assume
A1: P in the topology of S;
reconsider Q = P as Subset of T;
take Q;
thus Q in the topology of T by A1;
thus P = Q /\ [#]S by PRE_TOPC:15;
end;
given Q being Subset of T such that
A2: Q in the topology of T and
A3: P = Q /\ [#]S;
thus P in the topology of S by A2,A3,PRE_TOPC:15;
end;
definition let X be TopSpace;
cluster strict open SubSpace of X;
existence
proof
reconsider Y = the TopStruct of X as strict SubSpace of X by Lm5;
take Y;
Y is open
proof let A be Subset of X;
assume A = the carrier of Y;
then A = [#]X by PRE_TOPC:12;
hence A is open;
end;
hence thesis;
end;
end;
definition let X be non empty TopSpace;
cluster strict open non empty SubSpace of X;
existence
proof
X|[#]X is open
proof let A be Subset of X;
assume A = the carrier of X|[#]X;
then A = [#](X|[#]X) by PRE_TOPC:12
.= [#] X by PRE_TOPC:def 10;
hence A is open;
end;
hence thesis;
end;
end;
::Properties of Open Subspaces.
theorem Th16:
for X0 being SubSpace of X, A being Subset of X
st A = the carrier of X0 holds
X0 is open SubSpace of X iff A is open
proof let X0 be SubSpace of X, A be Subset of X;
assume A1: A = the carrier of X0;
hence X0 is open SubSpace of X implies A is open by Def1;
thus A is open implies X0 is open SubSpace of X
proof assume A is open;
then for B be Subset of X
holds B = the carrier of X0 implies B is open by A1;
hence thesis by Def1;
end;
end;
theorem
for X0 being open SubSpace of X, A being Subset of X,
B being Subset of X0 st
A = B holds B is open iff A is open
proof
let X0 be open SubSpace of X, A be Subset of X,
B be Subset of X0 such that
A1: A = B;
the carrier of X0 is Subset of X by Th1;
then reconsider C = the carrier of X0 as Subset of X;
C is open by Th16;
hence thesis by A1,Th9;
end;
theorem
for X1 being open SubSpace of X,
X2 being open SubSpace of X1 holds
X2 is open SubSpace of X
proof let X1 be open SubSpace of X,
X2 be open SubSpace of X1;
now let B be Subset of X;
A1: the carrier of X2 c= the carrier of X1 by BORSUK_1:35;
assume A2: B = the carrier of X2;
then reconsider BB = B as Subset of X1 by A1;
BB is open by A2,Def1;
then A3: ex A being Subset of X st A is open & A /\ [#]X1 = BB
by TOPS_2:32;
A4: [#]X1 = the carrier of X1 by PRE_TOPC:12;
then [#]X1 is Subset of X by BORSUK_1:35;
then reconsider C = [#]X1 as Subset of X;
C is open by A4,Def1;
hence B is open by A3,TOPS_1:38;
end;
hence thesis by Def1,Th7;
end;
theorem
for X be non empty TopSpace, X1 being open SubSpace of X,
X2 being non empty SubSpace of X st
the carrier of X1 c= the carrier of X2 holds
X1 is open SubSpace of X2
proof let X be non empty TopSpace, X1 be open SubSpace of X,
X2 be non empty SubSpace of X;
assume the carrier of X1 c= the carrier of X2;
then reconsider B = the carrier of X1 as Subset of X2;
now let C be Subset of X2; assume A1: C = the carrier of X1;
then C is Subset of X by BORSUK_1:35;
then reconsider A = C as Subset of X;
A2: A is open by A1,Th16;
[#]X2 = the carrier of X2 by PRE_TOPC:12;
then A /\ [#]X2 = C by XBOOLE_1:28;
hence C is open by A2,TOPS_2:32;
end;
then B is open;
hence thesis by Th4,Th16;
end;
theorem Th20:
for X be non empty TopSpace, A0 being non empty Subset of X st A0 is open
ex X0 being strict open non empty SubSpace of X st A0 = the carrier of X0
proof let X be non empty TopSpace, A0 be non empty Subset of X such that
A1: A0 is open;
consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by Th10;
reconsider Y0 = X0 as strict open non empty SubSpace of X by A1,A2,Th16;
take Y0;
thus thesis by A2;
end;
begin
::2. Operations on Subspaces of Topological Spaces.
reserve X for non empty TopSpace;
definition let X be non empty TopStruct;
let X1, X2 be non empty SubSpace of X;
func X1 union X2 -> strict non empty SubSpace of X means
:Def2: the carrier of it = (the carrier of X1) \/ (the carrier of X2);
existence
proof
reconsider A1 = the carrier of X1,
A2 = the carrier of X2 as Subset of X by Th1;
set A = A1 \/ A2;
reconsider A as non empty Subset of X by XBOOLE_1:15;
take X|A;
thus the carrier of (X|A) = [#](X|A) by PRE_TOPC:12
.= (the carrier of X1) \/ (the carrier of X2) by PRE_TOPC:def 10;
end;
uniqueness by Th5;
commutativity;
end;
reserve X1, X2, X3 for non empty SubSpace of X;
::Properties of the Union of two Subspaces.
theorem
(X1 union X2) union X3 = X1 union (X2 union X3)
proof
the carrier of (X1 union X2) union X3 =
(the carrier of X1 union X2) \/ (the carrier of X3) by Def2
.= ((the carrier of X1) \/ (the carrier of X2)) \/ (the carrier of X3)
by Def2
.= (the carrier of X1) \/ ((the carrier of X2) \/ (the carrier of X3))
by XBOOLE_1:
4
.= (the carrier of X1) \/ (the carrier of X2 union X3) by Def2
.= the carrier of X1 union (X2 union X3) by Def2;
hence thesis by Th5;
end;
theorem Th22:
X1 is SubSpace of X1 union X2
proof
set A1 = the carrier of X1, A2 = the carrier of X2,
A = the carrier of X1 union X2;
A = A1 \/ A2 by Def2;
then A1 c= A & A2 c= A by XBOOLE_1:7;
hence thesis by Th4;
end;
theorem
for X1,X2 being non empty SubSpace of X holds
X1 is SubSpace of X2 iff X1 union X2 = the TopStruct of X2
proof let X1,X2 be non empty SubSpace of X;
set A1 = the carrier of X1, A2 = the carrier of X2;
thus X1 is SubSpace of X2 iff X1 union X2 = the TopStruct of X2
proof
thus X1 is SubSpace of X2 implies X1 union X2 = the TopStruct of X2
proof assume X1 is SubSpace of X2;
then A1 c= A2 by BORSUK_1:35;
then A1 \/ A2 = the carrier of the TopStruct of X2 &
the TopStruct of X2 is strict SubSpace of X by Lm4,XBOOLE_1:12;
hence thesis by Def2;
end;
assume X1 union X2 = the TopStruct of X2;
then A1 \/ A2 = A2 by Def2;
then A1 c= A2 by XBOOLE_1:7;
hence X1 is SubSpace of X2 by Th4;
end;
end;
theorem
for X1, X2 being closed non empty SubSpace of X holds
X1 union X2 is closed SubSpace of X
proof let X1, X2 be closed non empty SubSpace of X;
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X
;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X
;
the carrier of X1 union X2 is Subset of X by Th1;
then reconsider A = the carrier of X1 union X2 as Subset of X
;
A1 is closed & A2 is closed by Th11;
then A1 \/ A2 is closed by TOPS_1:36;
then A is closed by Def2;
hence thesis by Th11;
end;
theorem
for X1, X2 being open non empty SubSpace of X holds
X1 union X2 is open SubSpace of X
proof let X1, X2 be open non empty SubSpace of X;
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X
;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X
;
the carrier of X1 union X2 is Subset of X by Th1;
then reconsider A = the carrier of X1 union X2 as Subset of X
;
A1 is open & A2 is open by Th16;
then A1 \/ A2 is open by TOPS_1:37;
then A is open by Def2;
hence thesis by Th16;
end;
definition let X be TopStruct; let X1, X2 be SubSpace of X;
pred X1 misses X2 means
:Def3: the carrier of X1 misses the carrier of X2;
correctness;
symmetry;
antonym X1 meets X2;
end;
definition let X be non empty TopStruct; let X1, X2 be non empty SubSpace of X;
assume A1: X1 meets X2;
canceled;
func X1 meet X2 -> strict non empty SubSpace of X means
:Def5: the carrier of it = (the carrier of X1) /\ (the carrier of X2);
existence
proof
reconsider A1 = the carrier of X1, A2 = the carrier of X2
as Subset of X by Th1;
set A = A1 /\ A2;
A1 meets A2 by A1,Def3;
then reconsider A as non empty Subset of X
by XBOOLE_0:def 7;
take X|A;
thus the carrier of (X|A) = [#](X|A) by PRE_TOPC:12
.= (the carrier of X1) /\ (the carrier of X2) by PRE_TOPC:def 10;
end;
uniqueness by Th5;
end;
reserve X1, X2, X3 for non empty SubSpace of X;
::Properties of the Meet of two Subspaces.
canceled 3;
theorem Th29:
(X1 meets X2 implies X1 meet X2 = X2 meet X1) &
((X1 meets X2 & (X1 meet X2) meets X3 or X2 meets X3 & X1 meets (X2 meet X3))
implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3))
proof
thus X1 meets X2 implies X1 meet X2 = X2 meet X1
proof assume
A1: X1 meets X2;
then the carrier of X1 meet X2 =(the carrier of X2) /\ (the carrier of X1)
by Def5
.= the carrier of X2 meet X1 by A1,Def5;
hence thesis by Th5;
end;
now assume A2:
X1 meets X2 & (X1 meet X2) meets X3 or X2 meets X3 & X1 meets (X2 meet X3);
A3: now assume A4: X1 meets X2 & (X1 meet X2) meets X3;
then (the carrier of X1 meet X2) meets (the carrier of X3) by Def3;
then (the carrier of X1 meet X2) /\ (the carrier of X3) <> {}
by XBOOLE_0:def 7;
then ((the carrier of X1) /\ (the carrier of X2)) /\
(the carrier of X3) <> {} by A4,Def5;
then A5: (the carrier of X1) /\ ((the carrier of X2) /\ (the carrier of X3)) <>
{}
by XBOOLE_1:
16;
then (the carrier of X2) /\ (the carrier of X3) <> {};
then A6: (the carrier of X2) meets (the carrier of X3) by XBOOLE_0:def
7;
then X2 meets X3 by Def3;
then (the carrier of X1) /\ (the carrier of X2 meet X3) <> {}
by A5,Def5;
then (the carrier of X1) meets (the carrier of X2 meet X3)
by XBOOLE_0:def 7;
hence X1 meets X2 & (X1 meet X2) meets X3
& X2 meets X3 & X1 meets (X2 meet X3) by A4,A6,Def3;
end;
A7: now assume A8: X2 meets X3 & X1 meets (X2 meet X3);
then (the carrier of X1) meets (the carrier of X2 meet X3) by Def3;
then (the carrier of X1) /\ (the carrier of X2 meet X3) <> {}
by XBOOLE_0:def 7;
then (the carrier of X1) /\ ((the carrier of X2) /\
(the carrier of X3)) <> {} by A8,Def5;
then A9: ((the carrier of X1) /\ (the carrier of X2)) /\ (the carrier of X3) <>
{}
by XBOOLE_1:16;
then (the carrier of X1) /\ (the carrier of X2) <> {};
then A10: (the carrier of X1) meets (the carrier of X2) by XBOOLE_0:def 7;
then X1 meets X2 by Def3;
then (the carrier of X1 meet X2) /\ (the carrier of X3) <> {}
by A9,Def5;
then (the carrier of X1 meet X2) meets (the carrier of X3)
by XBOOLE_0:def 7;
hence X1 meets X2 & (X1 meet X2) meets X3
& X2 meets X3 & X1 meets (X2 meet X3) by A8,A10,Def3;
end;
then the carrier of (X1 meet X2) meet X3 =
(the carrier of X1 meet X2) /\ (the carrier of X3) by A2,Def5
.= ((the carrier of X1) /\ (the carrier of X2)) /\ (the carrier of X3)
by A2,A7,Def5
.= (the carrier of X1) /\ ((the carrier of X2) /\ (the carrier of X3))
by XBOOLE_1:16
.= (the carrier of X1) /\ (the carrier of X2 meet X3) by A2,A3,Def5
.= the carrier of X1 meet (X2 meet X3) by A2,A3,Def5;
hence (X1 meet X2) meet X3 = X1 meet (X2 meet X3) by Th5;
end;
hence thesis;
end;
theorem Th30:
X1 meets X2 implies
X1 meet X2 is SubSpace of X1 & X1 meet X2 is SubSpace of X2
proof assume X1 meets X2;
then the carrier of X1 meet X2 = (the carrier of X1) /\ (the carrier of X2)
by Def5;
then the carrier of X1 meet X2 c= the carrier of X1
& the carrier of X1 meet X2 c= the carrier of X2 by XBOOLE_1:17;
hence thesis by Th4;
end;
theorem
for X1,X2 being non empty SubSpace of X holds
X1 meets X2 implies
(X1 is SubSpace of X2 iff X1 meet X2 = the TopStruct of X1) &
(X2 is SubSpace of X1 iff X1 meet X2 = the TopStruct of X2)
proof let X1,X2 be non empty SubSpace of X;
assume A1: X1 meets X2;
set A1 = the carrier of X1, A2 = the carrier of X2;
thus X1 is SubSpace of X2 iff X1 meet X2 = the TopStruct of X1
proof
thus X1 is SubSpace of X2 implies X1 meet X2 = the TopStruct of X1
proof assume X1 is SubSpace of X2;
then A1 c= A2 by BORSUK_1:35;
then A1 /\ A2 = the carrier of the TopStruct of X1 &
the TopStruct of X1 is strict SubSpace of X by Lm4,XBOOLE_1:28;
hence thesis by A1,Def5;
end;
assume X1 meet X2 = the TopStruct of X1;
then A1 /\ A2 = A1 by A1,Def5;
then A1 c= A2 by XBOOLE_1:17;
hence X1 is SubSpace of X2 by Th4;
end;
thus X2 is SubSpace of X1 iff X1 meet X2 = the TopStruct of X2
proof
thus X2 is SubSpace of X1 implies X1 meet X2 = the TopStruct of X2
proof assume X2 is SubSpace of X1;
then A2 c= A1 by BORSUK_1:35;
then A1 /\ A2 = the carrier of the TopStruct of X2 &
the TopStruct of X2 is strict SubSpace of X by Lm4,XBOOLE_1:28;
hence thesis by A1,Def5;
end;
assume X1 meet X2 = the TopStruct of X2;
then A1 /\ A2 = A2 by A1,Def5;
then A2 c= A1 by XBOOLE_1:17;
hence X2 is SubSpace of X1 by Th4;
end;
end;
theorem
for X1, X2 being closed non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is closed SubSpace of X
proof let X1, X2 be closed non empty SubSpace of X such that A1: X1 meets X2;
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X
;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X
;
the carrier of X1 meet X2 is Subset of X by Th1;
then reconsider A = the carrier of X1 meet X2 as Subset of X
;
A1 is closed & A2 is closed by Th11;
then A1 /\ A2 is closed by TOPS_1:35;
then A is closed by A1,Def5;
hence thesis by Th11;
end;
theorem
for X1, X2 being open non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is open SubSpace of X
proof let X1, X2 be open non empty SubSpace of X such that A1: X1 meets X2;
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X
;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X
;
the carrier of X1 meet X2 is Subset of X by Th1;
then reconsider A = the carrier of X1 meet X2 as Subset of X
;
A1 is open & A2 is open by Th16;
then A1 /\ A2 is open by TOPS_1:38;
then A is open by A1,Def5;
hence thesis by Th16;
end;
::Connections between the Union and the Meet.
theorem
X1 meets X2 implies
X1 meet X2 is SubSpace of X1 union X2
proof assume X1 meets X2;
then A1: X1 meet X2 is SubSpace of X1 by Th30;
X1 is SubSpace of X1 union X2 by Th22;
hence thesis by A1,Th7;
end;
theorem
for Y being non empty SubSpace of X st
X1 meets Y & Y meets X2 holds
(X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) &
Y meet (X1 union X2) = (Y meet X1) union (Y meet X2)
proof let Y be non empty SubSpace of X;
assume A1: X1 meets Y & Y meets X2;
X1 is SubSpace of X1 union X2 by Th22;
then the carrier of X1 c= the carrier of X1 union X2 by Th4;
then (the carrier of X1) /\ (the carrier of Y) c=
(the carrier of X1 union X2) /\ (the carrier of Y) &
(the carrier of X1) meets (the carrier of Y) by A1,Def3,XBOOLE_1:26;
then (the carrier of X1) /\ (the carrier of Y) c=
(the carrier of X1 union X2) /\ (the carrier of Y) &
(the carrier of X1) /\ (the carrier of Y) <> {} by XBOOLE_0:def 7;
then (the carrier of X1 union X2) /\ (the carrier of Y) <> {} by XBOOLE_1:3;
then (the carrier of X1 union X2) meets (the carrier of Y) by XBOOLE_0:def 7
;
then A2: (X1 union X2) meets Y by Def3;
thus (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y)
proof
the carrier of (X1 union X2) meet Y =
(the carrier of X1 union X2) /\ (the carrier of Y) by A2,Def5
.= ((the carrier of X1) \/ (the carrier of X2)) /\ (the carrier of Y)
by Def2
.= ((the carrier of X1) /\ (the carrier of Y)) \/
((the carrier of X2) /\ (the carrier of Y)) by XBOOLE_1:23
.= (the carrier of X1 meet Y) \/
((the carrier of X2) /\ (the carrier of Y)) by A1,Def5
.= (the carrier of X1 meet Y) \/ (the carrier of X2 meet Y) by A1,Def5
.= the carrier of (X1 meet Y) union (X2 meet Y) by Def2;
hence thesis by Th5;
end;
hence Y meet (X1 union X2) = (X1 meet Y) union (X2 meet Y) by A2,Th29
.= (Y meet X1) union (X2 meet Y) by A1,Th29
.= (Y meet X1) union (Y meet X2) by A1,Th29;
end;
theorem
for Y being non empty SubSpace of X holds X1 meets X2 implies
(X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) &
Y union (X1 meet X2) = (Y union X1) meet (Y union X2)
proof let Y be non empty SubSpace of X;
assume A1: X1 meets X2;
Y is SubSpace of X1 union Y & Y is SubSpace of X2 union Y by Th22;
then the carrier of Y c= the carrier of X1 union Y &
the carrier of Y c= the carrier of X2 union Y by Th4;
then the carrier of Y c=
(the carrier of X1 union Y) /\ (the carrier of X2 union Y) &
the carrier of Y <> {} by XBOOLE_1:19;
then (the carrier of X1 union Y) /\ (the carrier of X2 union Y) <> {}
by XBOOLE_1:3;
then (the carrier of X1 union Y) meets (the carrier of X2 union Y)
by XBOOLE_0:def 7;
then A2: (X1 union Y) meets (X2 union Y) by Def3;
thus (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y)
proof
the carrier of (X1 meet X2) union Y =
(the carrier of X1 meet X2) \/ (the carrier of Y) by Def2
.= ((the carrier of X1) /\ (the carrier of X2)) \/ (the carrier of Y)
by A1,Def5
.= ((the carrier of X1) \/ (the carrier of Y)) /\
((the carrier of X2) \/ (the carrier of Y)) by XBOOLE_1:24
.= (the carrier of X1 union Y) /\
((the carrier of X2) \/ (the carrier of Y)) by Def2
.= (the carrier of X1 union Y) /\ (the carrier of X2 union Y) by Def2
.= the carrier of (X1 union Y) meet (X2 union Y) by A2,Def5;
hence thesis by Th5;
end;
hence Y union (X1 meet X2) = (Y union X1) meet (Y union X2);
end;
begin
::3. Separated and Weakly Separated Subsets of Topological Spaces.
definition let X be TopStruct, A1, A2 be Subset of X;
redefine ::for the previous definition see CONNSP_1:def 1
pred A1,A2 are_separated;
antonym A1,A2 are_not_separated;
end;
reserve X for TopSpace;
reserve A1, A2 for Subset of X;
::Properties of Separated Subsets of Topological Spaces.
theorem Th37:
for A1,A2 being Subset of X holds
A1,A2 are_separated implies A1 misses A2 by CONNSP_1:2;
theorem Th38:
A1 is closed & A2 is closed implies (A1 misses A2 iff A1,A2 are_separated)
proof assume A1: A1 is closed & A2 is closed;
thus A1 misses A2 implies A1,A2 are_separated
proof assume A2: A1 misses A2;
Cl A1 = A1 & Cl A2 = A2 by A1,PRE_TOPC:52;
hence thesis by A2,CONNSP_1:def 1;
end;
thus A1,A2 are_separated implies A1 misses A2 by CONNSP_1:2;
end;
theorem Th39:
A1 \/ A2 is closed & A1,A2 are_separated implies A1 is closed & A2 is closed
proof assume A1: A1 \/ A2 is closed;
A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7;
then Cl A1 c= A1 \/ A2 & Cl A2 c= A1 \/ A2 by A1,TOPS_1:31;
then A2: Cl A1 \ A2 c= A1 & Cl A2 \ A1 c= A2 by XBOOLE_1:43;
assume A1,A2 are_separated;
then Cl A1 misses A2 & Cl A2 misses A1 by CONNSP_1:def 1;
then Cl A2 c= A2 & Cl A1 c= A1 & A1 c= Cl A1 & A2 c= Cl A2
by A2,PRE_TOPC:48,XBOOLE_1:83;
hence thesis by XBOOLE_0:def 10;
end;
theorem Th40:
A1 misses A2 & A1 is open implies A1 misses Cl A2
proof assume A1:A1 misses A2;
thus A1 is open implies A1 misses Cl A2
proof assume A1 is open;
then A2 c= A1` & A1` is closed by A1,PRE_TOPC:21,TOPS_1:30;
then Cl A2 c= A1` by TOPS_1:31;
then Cl A2 misses A1`` by TOPS_1:20;
then Cl A2 /\ A1`` = {} by XBOOLE_0:def 7;
then Cl A2 /\ A1 = {};
hence thesis by XBOOLE_0:def 7;
end;
end;
theorem Th41:
A1 is open & A2 is open implies (A1 misses A2 iff A1,A2 are_separated)
proof assume A1: A1 is open & A2 is open;
thus A1 misses A2 implies A1,A2 are_separated
proof assume A1 misses A2;
then A1 misses Cl A2 & Cl A1 misses A2 by A1,Th40;
hence thesis by CONNSP_1:def 1;
end;
thus A1,A2 are_separated implies A1 misses A2 by CONNSP_1:2;
end;
theorem Th42:
A1 \/ A2 is open & A1,A2 are_separated implies A1 is open & A2 is open
proof assume A1: A1 \/ A2 is open;
A2: A1 c= Cl A1 & A2 c= Cl A2 by PRE_TOPC:48;
assume A1,A2 are_separated;
then A2 misses Cl A1 & A1 misses Cl A2 by CONNSP_1:def 1;
then A3: A2 c= (Cl A1)` & A1 c= (Cl A2)` by PRE_TOPC:21;
A4: (A1 \/ A2) /\ (Cl A1)` = (A1 \/ A2) \ Cl A1 by SUBSET_1:32
.= (A1 \ Cl A1) \/ (A2 \ Cl A1) by XBOOLE_1:42
.= {} \/ (A2 \ Cl A1) by A2,XBOOLE_1:37
.= A2 /\ (Cl A1)` by SUBSET_1:32
.= A2 by A3,XBOOLE_1:28;
(A1 \/ A2) /\ (Cl A2)` = (A1 \/ A2) \ Cl A2 by SUBSET_1:32
.= (A1 \ Cl A2) \/ (A2 \ Cl A2) by XBOOLE_1:42
.= (A1 \ Cl A2) \/ {} by A2,XBOOLE_1:37
.= A1 /\ (Cl A2)` by SUBSET_1:32
.= A1 by A3,XBOOLE_1:28;
hence thesis by A1,A4,TOPS_1:38;
end;
::A Restriction Theorem for Separated Subsets (see also CONNSP_1:8).
reserve A1,A2 for Subset of X;
theorem Th43:
for C being Subset of X holds
A1,A2 are_separated implies
A1 /\ C,A2 /\ C are_separated
proof let C be Subset of X;
assume A1: A1,A2 are_separated;
A1 /\ C c= A1 & A2 /\ C c= A2 by XBOOLE_1:17;
hence thesis by A1,CONNSP_1:8;
end;
theorem Th44:
for B being Subset of X holds
A1,B are_separated or A2,B are_separated implies A1 /\ A2,B are_separated
proof let B be Subset of X;
thus
A1,B are_separated or A2,B are_separated implies A1 /\ A2,B are_separated
proof assume A1: A1,B are_separated or A2,B are_separated;
A2: now assume A3: A1,B are_separated;
A1 /\ A2 c= A1 by XBOOLE_1:17;
hence A1 /\ A2,B are_separated by A3,CONNSP_1:8;
end;
now assume A4: A2,B are_separated;
A1 /\ A2 c= A2 by XBOOLE_1:17;
hence A1 /\ A2,B are_separated by A4,CONNSP_1:8;
end;
hence thesis by A1,A2;
end;
end;
theorem Th45:
for B being Subset of X holds
A1,B are_separated & A2,B are_separated iff A1 \/ A2,B are_separated
proof let B be Subset of X;
thus A1,B are_separated & A2,B are_separated iff A1 \/ A2,B are_separated
proof
thus
A1,B are_separated & A2,B are_separated implies A1 \/ A2,B
are_separated
by CONNSP_1:9;
thus
A1 \/ A2,B are_separated implies A1,B are_separated & A2,B
are_separated
proof assume A1: A1 \/ A2,B are_separated;
A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7;
hence thesis by A1,CONNSP_1:8;
end;
end;
end;
theorem Th46:
A1,A2 are_separated iff
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
proof
thus A1,A2 are_separated implies
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
proof
set C1 = Cl A1, C2 = Cl A2;
assume A1: A1,A2 are_separated;
take C1,C2;
thus thesis by A1,CONNSP_1:def 1,PRE_TOPC:48;
end;
given C1, C2 being Subset of X such that
A2: A1 c= C1 & A2 c= C2 and A3: C1 misses A2 & C2 misses A1 and
A4: C1 is closed & C2 is closed;
Cl A1 c= C1 & Cl A2 c= C2 & A2 misses C1 & A1 misses C2
by A2,A3,A4,TOPS_1:31;
then Cl A1 misses A2 & A1 misses Cl A2 by XBOOLE_1:63;
hence A1,A2 are_separated by CONNSP_1:def 1;
end;
::First Characterization of Separated Subsets of Topological Spaces.
theorem Th47:
A1,A2 are_separated iff
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed
proof
thus A1,A2 are_separated implies
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed
proof assume A1,A2 are_separated;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
A3: C1 is closed & C2 is closed by Th46;
take C1,C2;
A1 misses C2 & A2 misses C1 & C1 /\ C2 c= C1 & C1 /\ C2 c= C2
by A2,XBOOLE_1:17;
then C1 /\ C2 misses A1 & C1 /\ C2 misses A2 by XBOOLE_1:63;
hence thesis by A1,A3,XBOOLE_1:70;
end;
given C1, C2 being Subset of X such that
A4: A1 c= C1 & A2 c= C2 and A5: C1 /\ C2 misses A1 \/ A2 and
A6: C1 is closed & C2 is closed;
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
proof
take C1,C2;
A7: now assume C1 meets A2;
then A8: C1 /\ A2 <> {} by XBOOLE_0:def 7;
C1 /\ A2 c= C1 /\ C2 & C1 /\ A2 c= A2 & A2 c= A1 \/
A2 by A4,XBOOLE_1:7,17,26;
then C1 /\ A2 c= (C1 /\ C2) /\ A2 & (C1 /\ C2) /\ A2 c= (C1 /\ C2) /\
(A1 \/ A2)
by XBOOLE_1:19,
26;
then C1 /\ A2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:1;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A8,XBOOLE_1:3;
hence contradiction by A5,XBOOLE_0:def 7;
end;
now assume C2 meets A1;
then A9: A1 /\ C2 <> {} by XBOOLE_0:def 7;
A1 /\ C2 c= C1 /\ C2 & A1 /\ C2 c= A1 & A1 c= A1 \/
A2 by A4,XBOOLE_1:7,17,26;
then A1 /\ C2 c= (C1 /\ C2) /\ A1 & (C1 /\ C2) /\ A1 c= (C1 /\ C2) /\
(A1 \/ A2)
by XBOOLE_1:19,
26;
then A1 /\ C2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:1;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A9,XBOOLE_1:3;
hence contradiction by A5,XBOOLE_0:def 7;
end;
hence thesis by A4,A6,A7;
end;
hence A1,A2 are_separated by Th46;
end;
theorem Th48:
A1,A2 are_separated iff
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 misses A2 & C2 misses A1 & C1 is open & C2 is open
proof
thus A1,A2 are_separated implies
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 misses A2 & C2 misses A1 & C1 is open & C2 is open
proof assume A1,A2 are_separated;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
A3: C1 is closed & C2 is closed by Th46;
take C2`,C1`;
thus thesis by A1,A2,A3,PRE_TOPC:21,TOPS_1:20,29;
end;
given C1, C2 being Subset of X such that
A4: A1 c= C1 & A2 c= C2 and A5: C1 misses A2 & C2 misses A1 and
A6: C1 is open & C2 is open;
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
proof
take C2`,C1`;
thus thesis by A4,A5,A6,PRE_TOPC:21,TOPS_1:20,30;
end;
hence A1,A2 are_separated by Th46;
end;
::Second Characterization of Separated Subsets of Topological Spaces.
theorem Th49:
A1,A2 are_separated iff
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open
proof
thus A1,A2 are_separated implies
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open
proof assume A1,A2 are_separated;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
A3: C1 is open & C2 is open by Th48;
take C1,C2;
A1 misses C2 & A2 misses C1 & C1 /\ C2 c= C1 & C1 /\ C2 c= C2
by A2,XBOOLE_1:17;
then C1 /\ C2 misses A1 & C1 /\ C2 misses A2 by XBOOLE_1:63;
hence thesis by A1,A3,XBOOLE_1:70;
end;
given C1, C2 being Subset of X such that
A4: A1 c= C1 & A2 c= C2 and A5: C1 /\ C2 misses A1 \/ A2 and
A6: C1 is open & C2 is open;
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 misses A2 & C2 misses A1 & C1 is open & C2 is open
proof
take C1,C2;
A7: now assume C1 meets A2;
then A8: C1 /\ A2 <> {} by XBOOLE_0:def 7;
C1 /\ A2 c= C1 /\ C2 & C1 /\ A2 c= A2 & A2 c= A1 \/
A2 by A4,XBOOLE_1:7,17,26;
then C1 /\ A2 c= (C1 /\ C2) /\ A2 & (C1 /\ C2) /\ A2 c= (C1 /\ C2) /\
(A1 \/ A2) by XBOOLE_1:19,26;
then C1 /\ A2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:1;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A8,XBOOLE_1:3;
hence contradiction by A5,XBOOLE_0:def 7;
end;
now assume C2 meets A1;
then A9: A1 /\ C2 <> {} by XBOOLE_0:def 7;
A1 /\ C2 c= C1 /\ C2 & A1 /\ C2 c= A1 & A1 c= A1 \/
A2 by A4,XBOOLE_1:7,17,26;
then A1 /\ C2 c= (C1 /\ C2) /\ A1 & (C1 /\ C2) /\ A1 c= (C1 /\ C2) /\
(A1 \/ A2) by XBOOLE_1:19,26;
then A1 /\ C2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:1;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A9,XBOOLE_1:3;
hence contradiction by A5,XBOOLE_0:def 7;
end;
hence thesis by A4,A6,A7;
end;
hence A1,A2 are_separated by Th48;
end;
definition let X be TopStruct, A1, A2 be Subset of X;
canceled;
pred A1,A2 are_weakly_separated means
:Def7: A1 \ A2,A2 \ A1 are_separated;
symmetry;
antonym A1,A2 are_not_weakly_separated;
end;
reserve X for TopSpace, A1, A2 for Subset of X;
::Properties of Weakly Separated Subsets of Topological Spaces.
canceled;
theorem Th51:
A1 misses A2 & A1,A2 are_weakly_separated iff A1,A2 are_separated
proof
thus A1 misses A2 & A1,A2 are_weakly_separated implies A1,A2 are_separated
proof
assume A1: A1 misses A2 & A1,A2 are_weakly_separated;
then A1 \ A2 = A1 & A2 \ A1 = A2 by XBOOLE_1:83;
hence A1,A2 are_separated by A1,Def7;
end;
assume A2: A1,A2 are_separated;
then A1 misses A2 by CONNSP_1:2;
then A1 \ A2 = A1 & A2 \ A1 = A2 by XBOOLE_1:83;
hence A1 misses A2 & A1,A2 are_weakly_separated by A2,Def7,CONNSP_1:2;
end;
theorem Th52:
A1 c= A2 implies A1,A2 are_weakly_separated
proof assume A1: A1 c= A2;
now assume A1 c= A2;
then A2: A1 \ A2 = {} & {}X = {} by XBOOLE_1:37;
then Cl(A1 \ A2) = {} by PRE_TOPC:52;
then Cl(A1 \ A2) /\ (A2 \ A1) = {} & (A1 \ A2) /\ Cl(A2 \ A1) = {}
by A2;
then Cl(A1 \ A2) misses (A2 \ A1) & (A1 \ A2) misses Cl(A2 \ A1)
by XBOOLE_0:def 7;
then A1 \ A2,A2 \ A1 are_separated by CONNSP_1:def 1;
hence thesis by Def7;
end;
hence thesis by A1;
end;
theorem Th53:
for A1,A2 being Subset of X holds
A1 is closed & A2 is closed implies A1,A2 are_weakly_separated
proof
let A1,A2 be Subset of X;
assume A1: A1 is closed & A2 is closed;
A1 \ A2 c= A1 & A2 \ A1 c= A2 by XBOOLE_1:36;
then Cl(A1 \ A2) c= A1 & Cl(A2 \ A1) c= A2 by A1,TOPS_1:31;
then Cl(A1 \ A2) \ A1 = {} & Cl(A2 \ A1) \ A2 = {} by XBOOLE_1:37;
then Cl(A1 \ A2) misses (A2 \ A1) &
(A1 \ A2) misses Cl(A2 \ A1) by Lm1;
then A1 \ A2,A2 \ A1 are_separated by CONNSP_1:def 1;
hence A1,A2 are_weakly_separated by Def7;
end;
theorem Th54:
for A1,A2 being Subset of X holds
A1 is open & A2 is open implies A1,A2 are_weakly_separated
proof
let A1,A2 be Subset of X;
assume A1: A1 is open & A2 is open;
A2 misses (A1 \ A2) & (A2 \ A1) misses A1 by XBOOLE_1:79;
then A2 misses Cl(A1 \ A2) & Cl(A2 \ A1) misses A1 by A1,Th40;
then Cl(A1 \ A2) misses (A2 \ A1) &
(A1 \ A2) misses Cl(A2 \ A1) by Lm2;
then A1 \ A2,A2 \ A1 are_separated by CONNSP_1:def 1;
hence A1,A2 are_weakly_separated by Def7;
end;
::Extension Theorems for Weakly Separated Subsets.
theorem Th55:
for C being Subset of X holds
A1,A2 are_weakly_separated implies
A1 \/ C,A2 \/ C are_weakly_separated
proof let C be Subset of X;
assume A1,A2 are_weakly_separated;
then A1: A1 \ A2,A2 \ A1 are_separated by Def7;
A2: (A1 \/ C) \ (A2 \/ C) = (A1 \ (A2 \/ C)) \/ (C \ (A2 \/ C)) by XBOOLE_1
:42
.= (A1 \ (A2 \/ C)) \/ {} by XBOOLE_1:46
.= (A1 \ A2) /\ (A1 \ C) by XBOOLE_1:53;
(A2 \/ C) \ (A1 \/ C) = (A2 \ (A1 \/ C)) \/ (C \ (A1 \/ C)) by XBOOLE_1:
42
.= (A2 \ (A1 \/ C)) \/ {} by XBOOLE_1:46
.= (A2 \ A1) /\ (A2 \ C) by XBOOLE_1:53;
then (A1 \/ C) \ (A2 \/ C) c= A1 \ A2 & (A2 \/ C) \ (A1 \/ C) c= A2 \ A1
by A2,XBOOLE_1:17;
then (A1 \/ C) \ (A2 \/ C),(A2 \/ C) \ (A1 \/ C) are_separated
by A1,CONNSP_1:8;
hence thesis by Def7;
end;
theorem Th56:
for B1, B2 being Subset of X st B1 c= A2 & B2 c= A1 holds
A1,A2 are_weakly_separated implies
A1 \/ B1,A2 \/ B2 are_weakly_separated
proof let B1, B2 be Subset of X such that
A1: B1 c= A2 & B2 c= A1;
assume A1,A2 are_weakly_separated;
then A2: A1 \ A2,A2 \ A1 are_separated by Def7;
A3: A2 c= A2 \/ B2 & A1 c= A1 \/ B1 by XBOOLE_1:7;
then B1 c= A2 \/ B2 & B2 c= A1 \/ B1 by A1,XBOOLE_1:1;
then A4: B1 \ (A2 \/ B2) = {} & B2 \ (A1 \/ B1) = {} by XBOOLE_1:37;
(A1 \/ B1) \ (A2 \/ B2) = (A1 \ (A2 \/ B2)) \/ (B1 \ (A2 \/ B2)) &
(A2 \/ B2) \ (A1 \/ B1) = (A2 \ (A1 \/ B1)) \/ (B2 \ (A1 \/
B1)) by XBOOLE_1:42;
then (A1 \/ B1) \ (A2 \/ B2) c= A1 \ A2 &
(A2 \/ B2) \ (A1 \/ B1) c= A2 \ A1 by A3,A4,XBOOLE_1:34;
then (A1 \/ B1) \ (A2 \/ B2),(A2 \/ B2) \ (A1 \/ B1) are_separated
by A2,CONNSP_1:8;
hence thesis by Def7;
end;
theorem Th57:
for B being Subset of X holds
A1,B are_weakly_separated & A2,B are_weakly_separated
implies A1 /\ A2,B are_weakly_separated
proof let B be Subset of X;
thus A1,B are_weakly_separated & A2,B are_weakly_separated implies
A1 /\ A2,B are_weakly_separated
proof assume A1,B are_weakly_separated & A2,B are_weakly_separated;
then A1 \ B,B \ A1 are_separated & A2 \ B,B \ A2 are_separated by Def7;
then (A1 \ B) /\ (A2 \ B),B \ A1 are_separated &
(A1 \ B) /\ (A2 \ B),B \ A2 are_separated by Th44;
then (A1 \ B) /\ (A2 \ B),(B \ A1) \/ (B \ A2) are_separated by Th45;
then (A1 /\ A2) \ B,(B \ A1) \/ (B \ A2) are_separated by Lm3;
then (A1 /\ A2) \ B,B \ (A1 /\ A2) are_separated by XBOOLE_1:54;
hence thesis by Def7;
end;
end;
theorem Th58:
for B being Subset of X holds
A1,B are_weakly_separated & A2,B are_weakly_separated
implies A1 \/ A2,B are_weakly_separated
proof let B be Subset of X;
thus A1,B are_weakly_separated & A2,B are_weakly_separated implies
A1 \/ A2,B are_weakly_separated
proof assume A1,B are_weakly_separated & A2,B are_weakly_separated;
then A1 \ B,B \ A1 are_separated & A2 \ B,B \ A2 are_separated by Def7;
then A1 \ B,(B \ A1) /\ (B \ A2) are_separated &
A2 \ B,(B \ A1) /\ (B \ A2) are_separated by Th44;
then (A1 \ B) \/ (A2 \ B),(B \ A1) /\ (B \ A2) are_separated by Th45;
then (A1 \/ A2) \ B,(B \ A1) /\ (B \ A2) are_separated by XBOOLE_1:42;
then (A1 \/ A2) \ B,B \ (A1 \/ A2) are_separated by XBOOLE_1:53;
hence thesis by Def7;
end;
end;
::First Characterization of Weakly Separated Subsets of Topological Spaces.
theorem Th59:
A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X
st C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
A2 &
the carrier of X = (C1 \/ C2) \/ C & C1 is closed & C2 is closed & C is open
proof
set B1 = A1 \ A2, B2 = A2 \ A1;
A1: (A1 \/ A2)` misses (A1 \/ A2) & (B1 \/ B2)` misses (B1 \/ B2)
by PRE_TOPC:26;
thus A1,A2 are_weakly_separated implies
ex C1, C2, C being Subset of X st
C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
A2 &
the carrier of X = (C1 \/ C2) \/ C & C1 is closed & C2 is closed &
C is open
proof assume A1,A2 are_weakly_separated;
then B1,B2 are_separated by Def7;
then consider C1, C2 being Subset of X such that
A2: B1 c= C1 & B2 c= C2 and A3: C1 misses B2 & C2 misses B1 and
A4: C1 is closed & C2 is closed by Th46;
take C1,C2;
take C = (C1 \/ C2)`;
A5: C1 \/ C2 is closed by A4,TOPS_1:36;
[#]X = C \/ C` by PRE_TOPC:18;
then A6: the carrier of X = C \/ C` by PRE_TOPC:12;
C1 /\ B2 = {} & C2 /\ B1 = {} by A3,XBOOLE_0:def 7;
then C1 /\ A2 \ C1 /\ A1 = {} & C2 /\ A1 \ C2 /\ A2 = {} by XBOOLE_1:50;
then A7: C1 /\ A2 c= C1 /\ A1 & C2 /\ A1 c= C2 /\ A2 by XBOOLE_1:37;
C1 /\ (A1 \/ A2) = C1 /\ A1 \/ C1 /\ A2 & C2 /\ (A1 \/ A2) = C2 /\ A1
\/
C2 /\ A2 by XBOOLE_1:23;
then A8:
C1 /\ (A1 \/ A2) = C1 /\ A1 & C2 /\ (A1 \/ A2) = C2 /\ A2 by A7,XBOOLE_1:12;
B1 \/ B2 c= C1 \/ C2 by A2,XBOOLE_1:13;
then C c= (B1 \/ B2)`by PRE_TOPC:19;
then C c= (A1 \+\ A2)` by XBOOLE_0:def 6;
then C c= ((A1 \/ A2) \ A1 /\ A2)` by XBOOLE_1:101;
then C c= (A1 \/ A2)` \/ (A1 /\ A2) by SUBSET_1:33;
then C /\ (A1 \/ A2) c= ((A1 \/ A2)` \/ (A1 /\ A2)) /\ (A1 \/
A2) by XBOOLE_1:26;
then C /\ (A1 \/ A2) c= (A1 \/ A2)` /\ (A1 \/ A2) \/ (A1 /\ A2) /\ (A1 \/
A2) by XBOOLE_1:23;
then C /\ (A1 \/ A2) c= {}X \/ (A1 /\ A2) /\ (A1 \/ A2)
by A1,XBOOLE_0:def 7;
then C /\ (A1 \/ A2) c= (A1 /\ A2) /\ (A1 \/ A2) &
(A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:17;
hence thesis by A4,A5,A6,A8,TOPS_1:29,XBOOLE_1:1,17;
end;
given C1, C2, C being Subset of X such that A9:
C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
A2 and
A10: the carrier of X = (C1 \/ C2) \/ C and
A11: C1 is closed & C2 is closed & C is open;
ex C1 being Subset of X, C2 being Subset of X st B1 c= C1 & B2 c= C2 &
C1 /\ C2 misses B1 \/ B2 & C1 is closed & C2 is closed
proof
take C1,C2;
A1 /\ A2 c= A1 & A1 /\ A2 c= A2 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:1;
then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 &
C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:8;
then (C \/ C1) /\ (A1 \/ A2) c= A1 & (C2 \/ C) /\ (A1 \/ A2) c= A2 &
A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7,23;
then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) &
B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by XBOOLE_1:35;
then A12: B2 c= (A1 \/ A2) \ (C \/ C1) &
B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A1 \/ A2 c= [#]X & [#]X = the carrier of X by PRE_TOPC:12,14;
then A1 \/ A2 c= (C \/ C1) \/ C2 & A1 \/ A2 c= (C2 \/ C) \/
C1 by A10,XBOOLE_1:4;
then A13:
(A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:
43;
(C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A9,XBOOLE_1:27
;
then (C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then (C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2)) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2) = {} by XBOOLE_1:37;
then (C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2)) = {} by XBOOLE_1:49;
then (C1 /\ C2) /\ (B1 \/ B2) = {} by XBOOLE_1:55;
hence thesis by A11,A12,A13,XBOOLE_0:def 7,XBOOLE_1:1;
end;
then B1,B2 are_separated by Th47;
hence A1,A2 are_weakly_separated by Def7;
end;
reserve X for non empty TopSpace, A1, A2 for Subset of X;
theorem Th60:
A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies
ex C1, C2 being non empty Subset of X st
C1 is closed & C2 is closed & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/
A2) c= A2 &
(A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/
C)
proof assume A1: A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
set B1 = A1 \ A2, B2 = A2 \ A1;
consider C1, C2, C being Subset of X such that
A2: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 &
C /\ (A1 \/ A2) c= A1 /\ A2 and
A3: the carrier of X = (C1 \/ C2) \/ C and
A4: C1 is closed & C2 is closed & C is open by A1,Th59;
A1 /\ A2 c= A1 & A1 /\ A2 c= A2 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 by A2,XBOOLE_1:1;
then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 &
C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A2,XBOOLE_1:8;
then (C \/ C1) /\ (A1 \/ A2) c= A1 & (C2 \/ C) /\ (A1 \/ A2) c= A2 &
A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7,23;
then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) &
B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by XBOOLE_1:35;
then A5: B2 c= (A1 \/ A2) \ (C \/ C1) &
B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A1 \/ A2 c= [#]X & [#]X = the carrier of X by PRE_TOPC:12,14;
then A1 \/ A2 c= (C \/ C1) \/ C2 & A1 \/ A2 c= (C2 \/ C) \/
C1 by A3,XBOOLE_1:4;
then (A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/
C) c= C1 by XBOOLE_1:43;
then A6:
B2 c= C2 & B1 c= C1 & B1 <> {} & B2 <> {} by A1,A5,XBOOLE_1:1,37;
then reconsider D1 = C1 as non empty Subset of X by XBOOLE_1:3;
reconsider D2 = C2 as non empty Subset of X by A6,XBOOLE_1:3;
take D1,D2;
now assume A7: not A1 \/ A2 c= C1 \/ C2;
thus ex C being non empty Subset of X st
the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\
A2 & C is open
proof
reconsider C0 = C as non empty Subset of X by A3,A7;
take C0;
thus thesis by A2,A3,A4;
end;
end;
hence thesis by A2,A4;
end;
theorem Th61:
A1 \/ A2 = the carrier of X implies
(A1,A2 are_weakly_separated iff
ex C1, C2, C being Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
C1 is closed & C2 is closed & C is open)
proof assume A1: A1 \/ A2 = the carrier of X;
then A2: [#]X = A1 \/ A2 by PRE_TOPC:12;
thus A1,A2 are_weakly_separated implies
ex C1, C2, C being Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
C1 is closed & C2 is closed & C is open
proof assume A1,A2 are_weakly_separated;
then consider C1, C2, C being Subset of X such that
A3: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 &
C /\ (A1 \/ A2) c= A1 /\ A2 and
A4: the carrier of X = (C1 \/ C2) \/ C and
A5: C1 is closed & C2 is closed & C is open by Th59;
take C1,C2,C;
thus thesis by A1,A2,A3,A4,A5,PRE_TOPC:15;
end;
given C1, C2, C being Subset of X such that
A6: A1 \/ A2 = (C1 \/ C2) \/ C and A7: C1 c= A1 & C2 c= A2 & C c= A1 /\
A2 and
A8: C1 is closed & C2 is closed & C is open;
ex C1, C2, C being Subset of X st
C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
A2 &
the carrier of X = (C1 \/ C2) \/
C & C1 is closed & C2 is closed & C is open
proof
take C1,C2,C;
thus thesis by A1,A2,A6,A7,A8,PRE_TOPC:15;
end;
hence A1,A2 are_weakly_separated by Th59;
end;
theorem Th62:
A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated &
not A1 c= A2 & not A2 c= A1 implies
ex C1, C2 being non empty Subset of X st
C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 &
(A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open)
proof assume A1: A1 \/ A2 = the carrier of X;
assume A2: A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
A3: [#]X = A1 \/ A2 by A1,PRE_TOPC:12;
consider C1, C2 being non empty Subset of X such that
A4: C1 is closed & C2 is closed and
A5: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 and
A6: A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2)
\/ C by A2,Th60;
take C1,C2;
now assume not A1 \/ A2 = C1 \/ C2;
then consider C being non empty Subset of X such that
A7: C is open and
A8: C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C
by A1,A6,XBOOLE_0:def 10;
thus ex C being non empty Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
proof
take C;
thus thesis by A1,A3,A7,A8,PRE_TOPC:15;
end;
end;
hence thesis by A3,A4,A5,PRE_TOPC:15;
end;
::Second Characterization of Weakly Separated Subsets of Topological Spaces.
theorem Th63:
A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X
st C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
A2 &
the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed
proof
set B1 = A1 \ A2, B2 = A2 \ A1;
A1: (A1 \/ A2)` misses (A1 \/ A2) & (B1 \/ B2)` misses (B1 \/ B2)
by PRE_TOPC:26;
thus A1,A2 are_weakly_separated implies
ex C1, C2, C being Subset of X st
C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
A2 &
the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed
proof assume A1,A2 are_weakly_separated;
then B1,B2 are_separated by Def7;
then consider C1, C2 being Subset of X such that
A2: B1 c= C1 & B2 c= C2 and A3: C1 misses B2 & C2 misses B1 and
A4: C1 is open & C2 is open by Th48;
take C1,C2;
take C = (C1 \/ C2)`;
A5: C1 \/ C2 is open by A4,TOPS_1:37;
[#]X = C` \/ C by PRE_TOPC:18;
then A6: the carrier of X = C` \/ C by PRE_TOPC:12;
C1 /\ B2 = {} & C2 /\ B1 = {} by A3,XBOOLE_0:def 7;
then C1 /\ A2 \ C1 /\ A1 = {} & C2 /\ A1 \ C2 /\ A2 = {} by XBOOLE_1:50;
then A7: C1 /\ A2 c= C1 /\ A1 & C2 /\ A1 c= C2 /\ A2 by XBOOLE_1:37;
C1 /\ (A1 \/ A2) = C1 /\ A1 \/ C1 /\ A2 & C2 /\ (A1 \/ A2) = C2 /\ A1
\/
C2 /\ A2
by XBOOLE_1:
23;
then A8:
C1 /\ (A1 \/ A2) = C1 /\ A1 & C2 /\ (A1 \/ A2) = C2 /\ A2 by A7,XBOOLE_1:12;
B1 \/ B2 c= C1 \/ C2 by A2,XBOOLE_1:13;
then C c= (B1 \/ B2)`by PRE_TOPC:19;
then C c= (A1 \+\ A2)` by XBOOLE_0:def 6;
then C c= ((A1 \/ A2) \ A1 /\ A2)` by XBOOLE_1:101;
then C c= (A1 \/ A2)` \/ (A1 /\ A2) by SUBSET_1:33;
then C /\ (A1 \/ A2) c= ((A1 \/ A2)` \/ (A1 /\ A2)) /\ (A1 \/
A2) by XBOOLE_1:26;
then C /\ (A1 \/ A2) c= (A1 \/ A2)` /\ (A1 \/ A2) \/ (A1 /\ A2) /\ (A1 \/
A2) by XBOOLE_1:23;
then C /\ (A1 \/ A2) c= {}X \/ (A1 /\ A2) /\ (A1 \/ A2)
by A1,XBOOLE_0:def 7;
then C /\ (A1 \/ A2) c= (A1 /\ A2) /\ (A1 \/ A2) &
(A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:17;
hence thesis by A4,A5,A6,A8,TOPS_1:30,XBOOLE_1:1,17;
end;
given C1, C2, C being Subset of X such that A9:
C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
A2 and
A10: the carrier of X = (C1 \/ C2) \/ C and
A11: C1 is open & C2 is open & C is closed;
ex C1, C2 being Subset of X st B1 c= C1 & B2 c= C2 &
C1 /\ C2 misses B1 \/ B2 & C1 is open & C2 is open
proof
take C1,C2;
A1 /\ A2 c= A1 & A1 /\ A2 c= A2 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:1;
then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 &
C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:8;
then (C \/ C1) /\ (A1 \/ A2) c= A1 & (C2 \/ C) /\ (A1 \/ A2) c= A2 &
A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7,23;
then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) &
B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by XBOOLE_1:35;
then A12: B2 c= (A1 \/ A2) \ (C \/ C1) &
B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A1 \/ A2 c= [#]X & [#]X = the carrier of X by PRE_TOPC:12,14;
then A1 \/ A2 c= (C \/ C1) \/ C2 & A1 \/ A2 c= (C2 \/ C) \/
C1 by A10,XBOOLE_1:4;
then A13:
(A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/
C) c= C1 by XBOOLE_1:43;
(C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A9,XBOOLE_1:27
;
then (C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then (C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2)) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2) = {} by XBOOLE_1:37;
then (C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2)) = {} by XBOOLE_1:49;
then (C1 /\ C2) /\ (B1 \/ B2) = {} by XBOOLE_1:55;
hence thesis by A11,A12,A13,XBOOLE_0:def 7,XBOOLE_1:1;
end;
then B1,B2 are_separated by Th49;
hence A1,A2 are_weakly_separated by Def7;
end;
theorem Th64:
A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies
ex C1, C2 being non empty Subset of X st
C1 is open & C2 is open & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 &
(A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X
st C is closed &
C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C)
proof assume A1: A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
set B1 = A1 \ A2, B2 = A2 \ A1;
consider C1, C2, C being Subset of X such that
A2: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
A2 and
A3: the carrier of X = (C1 \/ C2) \/ C and
A4: C1 is open & C2 is open & C is closed by A1,Th63;
A1 /\ A2 c= A1 & A1 /\ A2 c= A2 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 by A2,XBOOLE_1:1;
then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 &
C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A2,XBOOLE_1:8;
then (C \/ C1) /\ (A1 \/ A2) c= A1 & (C2 \/ C) /\ (A1 \/ A2) c= A2 &
A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7,23;
then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) &
B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by XBOOLE_1:35;
then A5: B2 c= (A1 \/ A2) \ (C \/ C1) &
B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A1 \/ A2 c= [#]X & [#]X = the carrier of X by PRE_TOPC:12,14;
then A1 \/ A2 c= (C \/ C1) \/ C2 & A1 \/ A2 c= (C2 \/ C) \/
C1 by A3,XBOOLE_1:4;
then (A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/
C) c= C1 by XBOOLE_1:43;
then A6:
B2 c= C2 & B1 c= C1 & B1 <> {} & B2 <> {} by A1,A5,XBOOLE_1:1,37;
then reconsider D1 = C1 as non empty Subset of X by XBOOLE_1:3;
reconsider D2 = C2 as non empty Subset of X by A6,XBOOLE_1:3;
take D1,D2;
now assume A7: not A1 \/ A2 c= C1 \/ C2;
thus ex C being non empty Subset of X st
the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\
A2 & C is closed
proof
reconsider C0 = C as non empty Subset of X by A3,A7;
take C0;
thus thesis by A2,A3,A4;
end;
end;
hence thesis by A2,A4;
end;
theorem Th65:
A1 \/ A2 = the carrier of X implies
(A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
C1 is open & C2 is open & C is closed)
proof assume A1: A1 \/ A2 = the carrier of X;
X is SubSpace of X by Th2;
then reconsider D = the carrier of X as Subset of X by Th1;
A2: D = [#]X by PRE_TOPC:12;
thus A1,A2 are_weakly_separated implies
ex C1, C2, C being Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
C1 is open & C2 is open & C is closed
proof assume A1,A2 are_weakly_separated;
then consider C1, C2, C being Subset of X such that
A3: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 &
C /\ (A1 \/ A2) c= A1 /\ A2 and
A4: the carrier of X = (C1 \/ C2) \/ C and
A5: C1 is open & C2 is open & C is closed by Th63;
take C1,C2,C;
thus thesis by A1,A2,A3,A4,A5,PRE_TOPC:15;
end;
given C1, C2, C being Subset of X such that
A6: A1 \/ A2 = (C1 \/ C2) \/ C and A7: C1 c= A1 & C2 c= A2 & C c= A1 /\
A2 and
A8: C1 is open & C2 is open & C is closed;
ex C1, C2, C being Subset of X st
C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
A2 &
the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed
proof
take C1,C2,C;
thus thesis by A1,A2,A6,A7,A8,PRE_TOPC:15;
end;
hence A1,A2 are_weakly_separated by Th63;
end;
theorem Th66:
A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated &
not A1 c= A2 & not A2 c= A1 implies
ex C1, C2 being non empty Subset of X st
C1 is open & C2 is open & C1 c= A1 & C2 c= A2 &
(A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed)
proof assume A1: A1 \/ A2 = the carrier of X;
assume A2: A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
A3: [#]X = A1 \/ A2 by A1,PRE_TOPC:12;
consider C1, C2 being non empty Subset of X such that
A4: C1 is open & C2 is open and
A5: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 and
A6: A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2)
\/ C
by A2,Th64;
take C1,C2;
now assume not A1 \/ A2 = C1 \/ C2;
then consider C being non empty Subset of X such that
A7: C is closed and
A8: C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C
by A1,A6,XBOOLE_0:def 10;
thus ex C being non empty Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
proof
take C;
thus thesis by A1,A3,A7,A8,PRE_TOPC:15;
end;
end;
hence thesis by A3,A4,A5,PRE_TOPC:15;
end;
::A Characterization of Separated Subsets by means of Weakly Separated ones.
theorem Th67:
A1,A2 are_separated iff ex B1, B2 being Subset of X st
B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2
proof
thus A1,A2 are_separated implies
ex B1, B2 being Subset of X st
B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2
proof assume A1,A2 are_separated;
then consider B1, B2 being Subset of X such that
A1: A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 and
A2: B1 is open & B2 is open by Th49;
take B1,B2;
thus thesis by A1,A2,Th54;
end;
given B1, B2 being Subset of X such that
A3: B1,B2 are_weakly_separated and
A4: A1 c= B1 & A2 c= B2 and
A5: B1 /\ B2 misses A1 \/ A2;
A1 /\ B2 c= A1 & A1 /\ B2 c= B1 /\ B2 & B1 /\ A2 c= A2 & B1 /\ A2 c= B1
/\
B2
by A4,XBOOLE_1:17,
26;
then A6: A1 /\ B2 c= (B1 /\ B2) /\ A1 & B1 /\ A2 c= (B1 /\ B2) /\
A2 by XBOOLE_1:19;
A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7;
then B1 /\ B2 misses A1 & B1 /\ B2 misses A2 by A5,XBOOLE_1:63;
then (B1 /\ B2) /\ A1 = {} & (B1 /\ B2) /\ A2 = {} by XBOOLE_0:def 7;
then A7: A1 /\ B2 = {} & B1 /\ A2 = {} by A6,XBOOLE_1:3;
A1 \ B2 c= B1 \ B2 & A2 \ B1 c= B2 \ B1 by A4,XBOOLE_1:33;
then A8: A1 \ A1 /\ B2 c= B1 \ B2 & A2 \ B1 /\ A2 c= B2 \ B1 by XBOOLE_1:47;
B1 \ B2,B2 \ B1 are_separated by A3,Def7;
hence A1,A2 are_separated by A7,A8,CONNSP_1:8;
end;
begin
::4. Separated and Weakly Separated Subspaces of Topological Spaces.
reserve X for non empty TopSpace;
definition let X be TopStruct; let X1, X2 be SubSpace of X;
pred X1,X2 are_separated means
:Def8: for A1, A2 being Subset of X st
A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_separated;
symmetry;
antonym X1,X2 are_not_separated;
end;
reserve X1, X2 for non empty SubSpace of X;
::Properties of Separated Subspaces of Topological Spaces.
theorem
X1,X2 are_separated implies X1 misses X2
proof
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then A1 misses A2 by Th37;
hence thesis by Def3;
end;
canceled;
theorem
for X1, X2 being closed non empty SubSpace of X holds
X1 misses X2 iff X1,X2 are_separated
proof let X1, X2 be closed non empty SubSpace of X;
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X;
A1: A1 is closed & A2 is closed by Th11;
thus X1 misses X2 implies X1,X2 are_separated
proof assume X1 misses X2;
then A1 misses A2 by Def3;
then for A1, A2 be Subset of X holds
A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_separated
by A1,Th38;
hence thesis by Def8;
end;
assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then A1 misses A2 by CONNSP_1:2;
hence X1 misses X2 by Def3;
end;
theorem
X = X1 union X2 & X1,X2 are_separated implies
X1 is closed SubSpace of X
proof assume
A1: X = X1 union X2;
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X;
A1 \/ A2 = the carrier of X by A1,Def2;
then A2: A1 \/ A2 = [#]X by PRE_TOPC:12;
assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then A1 is closed & A2 is closed by A2,CONNSP_1:5;
hence thesis by Th11;
end;
theorem
X1 union X2 is closed SubSpace of X & X1,X2 are_separated implies
X1 is closed SubSpace of X
proof
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X;
A1: A1 \/ A2 = the carrier of X1 union X2 by Def2;
assume X1 union X2 is closed SubSpace of X;
then A2: A1 \/ A2 is closed by A1,Th11;
assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then A1 is closed & A2 is closed by A2,Th39;
hence thesis by Th11;
end;
theorem
for X1, X2 being open non empty SubSpace of X holds
X1 misses X2 iff X1,X2 are_separated
proof let X1, X2 be open non empty SubSpace of X;
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X;
A1: A1 is open & A2 is open by Th16;
thus X1 misses X2 implies X1,X2 are_separated
proof
assume X1 misses X2;
then A1 misses A2 by Def3;
then for A1, A2 be Subset of X holds
A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_separated
by A1,Th41;
hence thesis by Def8;
end;
assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then A1 misses A2 by CONNSP_1:2;
hence X1 misses X2 by Def3;
end;
theorem
X = X1 union X2 & X1,X2 are_separated implies
X1 is open SubSpace of X
proof
assume A1: X = X1 union X2;
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X;
A1 \/ A2 = the carrier of X by A1,Def2;
then A2: A1 \/ A2 = [#]X by PRE_TOPC:12;
assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then A1 is open & A2 is open by A2,CONNSP_1:5;
hence thesis by Th16;
end;
theorem
X1 union X2 is open SubSpace of X & X1,X2 are_separated implies
X1 is open SubSpace of X
proof
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X;
A1: A1 \/ A2 = the carrier of X1 union X2 by Def2;
assume X1 union X2 is open SubSpace of X;
then A2: A1 \/ A2 is open by A1,Th16;
assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then A1 is open & A2 is open by A2,Th42;
hence thesis by Th16;
end;
::Restriction Theorems for Separated Subspaces.
theorem
for Y, X1, X2 being non empty SubSpace of X st X1 meets Y & X2 meets Y holds
X1,X2 are_separated implies
X1 meet Y,X2 meet Y are_separated & Y meet X1,Y meet X2 are_separated
proof let Y, X1, X2 be non empty SubSpace of X such that
A1: X1 meets Y & X2 meets Y;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider C = the carrier of Y as Subset of X by Th1;
assume A2: X1,X2 are_separated;
thus A3: X1 meet Y,X2 meet Y are_separated
proof
A4: A1,A2 are_separated by A2,Def8;
now let D1, D2 be Subset of X;
assume D1 = the carrier of X1 meet Y & D2 = the carrier of X2 meet Y;
then A1 /\ C = D1 & A2 /\ C = D2 by A1,Def5;
hence D1,D2 are_separated by A4,Th43;
end;
hence thesis by Def8;
end;
thus Y meet X1,Y meet X2 are_separated
proof
X1 meet Y,Y meet X2 are_separated by A1,A3,Th29;
hence thesis by A1,Th29;
end;
end;
theorem Th77:
for Y1, Y2 being SubSpace of X st
Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds
X1,X2 are_separated implies Y1,Y2 are_separated
proof let Y1, Y2 be SubSpace of X such that
A1: Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
assume A2: X1,X2 are_separated;
now let B1, B2 be Subset of X;
assume B1 = the carrier of Y1 & B2 = the carrier of Y2;
then A1,A2 are_separated & B1 c= A1 & B2 c= A2 by A1,A2,Def8,Th4;
hence B1,B2 are_separated by CONNSP_1:8;
end;
hence Y1,Y2 are_separated by Def8;
end;
theorem
for Y being non empty SubSpace of X st X1 meets X2 holds
X1,Y are_separated implies X1 meet X2,Y are_separated
proof let Y be non empty SubSpace of X;
assume X1 meets X2;
then A1: X1 meet X2 is SubSpace of X1 by Th30;
Y is SubSpace of Y by Th2;
hence thesis by A1,Th77;
end;
theorem
for Y being non empty SubSpace of X holds
X1,Y are_separated & X2,Y are_separated iff X1 union X2,Y are_separated
proof let Y be non empty SubSpace of X;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider C = the carrier of Y as Subset of X by Th1;
thus
X1,Y are_separated & X2,Y are_separated implies X1 union X2,Y
are_separated
proof assume X1,Y are_separated & X2,Y are_separated;
then A1: A1,C are_separated & A2,C are_separated by Def8;
now let D, C be Subset of X; assume
A2: D = the carrier of X1 union X2 & C = the carrier of Y;
then A1 \/ A2 = D by Def2;
hence D,C are_separated by A1,A2,Th45;
end;
hence thesis by Def8;
end;
assume A3: X1 union X2,Y are_separated;
X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2
& Y is SubSpace of Y by Th2,Th22;
hence thesis by A3,Th77;
end;
theorem
X1,X2 are_separated iff ex Y1, Y2 being closed non empty SubSpace of X st
X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1
proof
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
thus X1,X2 are_separated implies
ex Y1, Y2 being closed non empty SubSpace of X st
X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1
proof assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
A3: C1 is closed & C2 is closed by Th46;
A4: C1 is non empty & C2 is non empty by A1,XBOOLE_1:3;
then consider Y1 being strict closed non empty SubSpace of X such that
A5: C1 = the carrier of Y1 by A3,Th15;
consider Y2 being strict closed non empty SubSpace of X such that
A6: C2 = the carrier of Y2 by A3,A4,Th15;
take Y1,Y2;
thus thesis by A1,A2,A5,A6,Def3,Th4;
end;
given Y1, Y2 being closed non empty SubSpace of X such that
A7: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A8: Y1 misses X2 & Y2 misses X1;
now let A1, A2 be Subset of X such that
A9: A1 = the carrier of X1 & A2 = the carrier of X2;
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
proof
the carrier of Y1 is Subset of X by Th1;
then reconsider C1 = the carrier of Y1 as Subset of X;
the carrier of Y2 is Subset of X by Th1;
then reconsider C2 = the carrier of Y2 as Subset of X;
take C1,C2;
thus thesis by A7,A8,A9,Def3,Th4,Th11;
end;
hence A1,A2 are_separated by Th46;
end;
hence X1,X2 are_separated by Def8;
end;
::First Characterization of Separated Subspaces of Topological Spaces.
theorem
X1,X2 are_separated iff ex Y1, Y2 being closed non empty SubSpace of X st
X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
(Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
proof
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
thus X1,X2 are_separated implies
ex Y1, Y2 being closed non empty SubSpace of X st
X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
(Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
proof assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 and A2: C1 /\ C2 misses A1 \/ A2 and
A3: C1 is closed & C2 is closed by Th47;
A4: C1 is non empty & C2 is non empty by A1,XBOOLE_1:3;
then consider Y1 being strict closed non empty SubSpace of X such that
A5: C1 = the carrier of Y1 by A3,Th15;
consider Y2 being strict closed non empty SubSpace of X such that
A6: C2 = the carrier of Y2 by A3,A4,Th15;
take Y1,Y2;
now assume not Y1 misses Y2;
then A7: the carrier of Y1 meet Y2 = C1 /\ C2 by A5,A6,Def5;
the carrier of X1 union X2 = A1 \/ A2 by Def2;
hence Y1 meet Y2 misses X1 union X2 by A2,A7,Def3;
end;
hence thesis by A1,A5,A6,Th4;
end;
given Y1, Y2 being closed non empty SubSpace of X such that
A8: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A9: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
now let A1, A2 be Subset of X such that
A10: A1 = the carrier of X1 & A2 = the carrier of X2;
ex C1 being Subset of X, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed
proof
the carrier of Y1 is Subset of X by Th1;
then reconsider C1 = the carrier of Y1 as Subset of X;
the carrier of Y2 is Subset of X by Th1;
then reconsider C2 = the carrier of Y2 as Subset of X;
take C1,C2;
now per cases;
suppose Y1 misses Y2;
then C1 misses C2 by Def3;
then C1 /\ C2 = {} by XBOOLE_0:def 7;
hence C1 /\ C2 misses A1 \/ A2 by XBOOLE_1:65;
suppose A11: not Y1 misses Y2;
then the carrier of Y1 meet Y2 = C1 /\ C2 &
the carrier of X1 union X2 = A1 \/ A2 by A10,Def2,Def5;
hence C1 /\ C2 misses A1 \/ A2 by A9,A11,Def3;
end;
hence thesis by A8,A10,Th4,Th11;
end;
hence A1,A2 are_separated by Th47;
end;
hence X1,X2 are_separated by Def8;
end;
theorem
X1,X2 are_separated iff ex Y1, Y2 being open non empty SubSpace of X st
X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1
proof
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
thus X1,X2 are_separated implies
ex Y1,Y2 being open non empty SubSpace of X st
X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1
proof assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then consider C1 being Subset of X,
C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
A3: C1 is open & C2 is open by Th48;
A4: C1 is non empty & C2 is non empty by A1,XBOOLE_1:3;
then consider Y1 being strict open non empty SubSpace of X such that
A5: C1 = the carrier of Y1 by A3,Th20;
consider Y2 being strict open non empty SubSpace of X such that
A6: C2 = the carrier of Y2 by A3,A4,Th20;
take Y1,Y2;
thus thesis by A1,A2,A5,A6,Def3,Th4;
end;
given Y1, Y2 being open non empty SubSpace of X such that
A7: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A8: Y1 misses X2 & Y2 misses X1;
now let A1, A2 be Subset of X such that
A9: A1 = the carrier of X1 & A2 = the carrier of X2;
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 misses A2 & C2 misses A1 & C1 is open & C2 is open
proof
the carrier of Y1 is Subset of X by Th1;
then reconsider C1 = the carrier of Y1 as Subset of X;
the carrier of Y2 is Subset of X by Th1;
then reconsider C2 = the carrier of Y2 as Subset of X;
take C1,C2;
thus thesis by A7,A8,A9,Def3,Th4,Th16;
end;
hence A1,A2 are_separated by Th48;
end;
hence X1,X2 are_separated by Def8;
end;
::Second Characterization of Separated Subspaces of Topological Spaces.
theorem Th83:
X1,X2 are_separated iff ex Y1, Y2 being open non empty SubSpace of X st
X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
(Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
proof
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
thus X1,X2 are_separated implies
ex Y1, Y2 being open non empty SubSpace of X st
X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
(Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
proof assume X1,X2 are_separated;
then A1,A2 are_separated by Def8;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 and A2: C1 /\ C2 misses A1 \/ A2 and
A3: C1 is open & C2 is open by Th49;
A4: C1 is non empty & C2 is non empty by A1,XBOOLE_1:3;
then consider Y1 being strict open non empty SubSpace of X such that
A5: C1 = the carrier of Y1 by A3,Th20;
consider Y2 being strict open non empty SubSpace of X such that
A6: C2 = the carrier of Y2 by A3,A4,Th20;
take Y1,Y2;
now assume not Y1 misses Y2;
then A7: the carrier of Y1 meet Y2 = C1 /\ C2 by A5,A6,Def5;
the carrier of X1 union X2 = A1 \/ A2 by Def2;
hence Y1 meet Y2 misses X1 union X2 by A2,A7,Def3;
end;
hence thesis by A1,A5,A6,Th4;
end;
given Y1, Y2 being open non empty SubSpace of X such that
A8: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A9: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
now let A1, A2 be Subset of X such that
A10: A1 = the carrier of X1 & A2 = the carrier of X2;
ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open
proof
the carrier of Y1 is Subset of X by Th1;
then reconsider C1 = the carrier of Y1 as Subset of X;
the carrier of Y2 is Subset of X by Th1;
then reconsider C2 = the carrier of Y2 as Subset of X;
take C1,C2;
now per cases;
suppose Y1 misses Y2;
then C1 misses C2 by Def3;
then C1 /\ C2 = {} by XBOOLE_0:def 7;
hence C1 /\ C2 misses A1 \/ A2 by XBOOLE_1:65;
suppose A11: not Y1 misses Y2;
then the carrier of Y1 meet Y2 = C1 /\ C2 &
the carrier of X1 union X2 = A1 \/ A2 by A10,Def2,Def5;
hence C1 /\ C2 misses A1 \/ A2 by A9,A11,Def3;
end;
hence thesis by A8,A10,Th4,Th16;
end;
hence A1,A2 are_separated by Th49;
end;
hence X1,X2 are_separated by Def8;
end;
definition let X be TopStruct, X1, X2 be SubSpace of X;
pred X1,X2 are_weakly_separated means
:Def9: for A1, A2 being Subset of X st
A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated;
symmetry;
antonym X1,X2 are_not_weakly_separated;
end;
reserve X1, X2 for non empty SubSpace of X;
::Properties of Weakly Separated Subspaces of Topological Spaces.
canceled;
theorem Th85:
X1 misses X2 & X1,X2 are_weakly_separated iff X1,X2 are_separated
proof
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
thus X1 misses X2 & X1,X2 are_weakly_separated implies X1,X2 are_separated
proof
assume X1 misses X2 & X1,X2 are_weakly_separated;
then A1 misses A2 & A1,A2 are_weakly_separated by Def3,Def9;
then for A1, A2 be Subset of X holds
A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_separated
by Th51;
hence X1,X2 are_separated by Def8;
end;
assume X1,X2 are_separated;
then A1: A1,A2 are_separated by Def8;
then A1 misses A2 & A1,A2 are_weakly_separated by Th51;
hence X1 misses X2 by Def3;
for A1, A2 be Subset of X holds
A1 = the carrier of X1 & A2 = the carrier of X2 implies
A1,A2 are_weakly_separated by A1,Th51;
hence X1,X2 are_weakly_separated by Def9;
end;
theorem Th86:
X1 is SubSpace of X2 implies X1,X2 are_weakly_separated
proof assume A1: X1 is SubSpace of X2;
now assume A2: X1 is SubSpace of X2;
now let A1, A2 be Subset of X;
assume A1 = the carrier of X1 & A2 = the carrier of X2;
then A1 c= A2 by A2,Th4;
hence A1,A2 are_weakly_separated by Th52;
end;
hence thesis by Def9;
end;
hence thesis by A1;
end;
theorem Th87:
for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated
proof
let X1, X2 be closed SubSpace of X;
now let A1, A2 be Subset of X;
reconsider B1 = A1, B2 = A2 as Subset of X;
assume A1 = the carrier of X1 & A2 = the carrier of X2;
then B1 is closed & B2 is closed by Th11;
hence A1,A2 are_weakly_separated by Th53;
end;
hence thesis by Def9;
end;
theorem Th88:
for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated
proof
let X1, X2 be open SubSpace of X;
now let A1, A2 be Subset of X;
reconsider B1 = A1, B2 = A2 as Subset of X;
assume A1 = the carrier of X1 & A2 = the carrier of X2;
then B1 is open & B2 is open by Th16;
hence A1,A2 are_weakly_separated by Th54;
end;
hence thesis by Def9;
end;
::Extension Theorems for Weakly Separated Subspaces.
theorem
for Y being non empty SubSpace of X holds
X1,X2 are_weakly_separated implies
X1 union Y,X2 union Y are_weakly_separated
proof let Y be non empty SubSpace of X;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider C = the carrier of Y as Subset of X by Th1;
assume X1,X2 are_weakly_separated;
then A1: A1,A2 are_weakly_separated by Def9;
now let D1, D2 be Subset of X;
assume D1 = the carrier of X1 union Y & D2 = the carrier of X2 union Y;
then A1 \/ C = D1 & A2 \/ C = D2 by Def2;
hence D1,D2 are_weakly_separated by A1,Th55;
end;
hence thesis by Def9;
end;
theorem
for Y1, Y2 being non empty SubSpace of X st
Y1 is SubSpace of X2 & Y2 is SubSpace of X1 holds
X1,X2 are_weakly_separated implies
X1 union Y1,X2 union Y2 are_weakly_separated &
Y1 union X1,Y2 union X2 are_weakly_separated
proof
let Y1, Y2 be non empty SubSpace of X such that
A1: Y1 is SubSpace of X2 & Y2 is SubSpace of X1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider B1 = the carrier of Y1 as Subset of X by Th1;
reconsider B2 = the carrier of Y2 as Subset of X by Th1;
A2: B1 c= A2 & B2 c= A1 by A1,Th4;
assume X1,X2 are_weakly_separated;
then A3: A1,A2 are_weakly_separated by Def9;
thus X1 union Y1,X2 union Y2 are_weakly_separated
proof
now let D1, D2 be Subset of X;
assume D1 = the carrier of X1 union Y1 & D2 = the carrier of X2 union Y2;
then A1 \/ B1 = D1 & A2 \/ B2 = D2 by Def2;
hence D1,D2 are_weakly_separated by A2,A3,Th56;
end;
hence thesis by Def9;
end;
hence Y1 union X1,Y2 union X2 are_weakly_separated;
end;
theorem
for Y, X1, X2 being non empty SubSpace of X st X1 meets X2 holds
(X1,Y are_weakly_separated & X2,Y are_weakly_separated
implies X1 meet X2,Y are_weakly_separated)
& (Y,X1 are_weakly_separated & Y,X2 are_weakly_separated
implies Y,X1 meet X2 are_weakly_separated)
proof let Y, X1, X2 be non empty SubSpace of X such that A1: X1 meets X2;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider C = the carrier of Y as Subset of X by Th1;
thus X1,Y are_weakly_separated & X2,Y are_weakly_separated
implies X1 meet X2,Y are_weakly_separated
proof assume X1,Y are_weakly_separated & X2,Y are_weakly_separated;
then A2: A1,C are_weakly_separated & A2,C are_weakly_separated by Def9;
now let D, C be Subset of X; assume
A3: D = the carrier of X1 meet X2 & C = the carrier of Y;
then A1 /\ A2 = D by A1,Def5;
hence D,C are_weakly_separated by A2,A3,Th57;
end;
hence thesis by Def9;
end;
hence Y,X1 are_weakly_separated & Y,X2 are_weakly_separated
implies Y,X1 meet X2 are_weakly_separated;
end;
theorem
for Y being non empty SubSpace of X holds
(X1,Y are_weakly_separated & X2,Y are_weakly_separated
implies X1 union X2,Y are_weakly_separated)
& (Y,X1 are_weakly_separated & Y,X2 are_weakly_separated
implies Y,X1 union X2 are_weakly_separated)
proof let Y be non empty SubSpace of X;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider C = the carrier of Y as Subset of X by Th1;
thus X1,Y are_weakly_separated & X2,Y are_weakly_separated
implies X1 union X2,Y are_weakly_separated
proof assume X1,Y are_weakly_separated & X2,Y are_weakly_separated;
then A1: A1,C are_weakly_separated & A2,C are_weakly_separated by Def9;
now let D, C be Subset of X; assume
A2: D = the carrier of X1 union X2 & C = the carrier of Y;
then A1 \/ A2 = D by Def2;
hence D,C are_weakly_separated by A1,A2,Th58;
end;
hence thesis by Def9;
end;
hence Y,X1 are_weakly_separated & Y,X2 are_weakly_separated
implies Y,X1 union X2 are_weakly_separated;
end;
::First Characterization of Weakly Separated Subspaces of Topological Spaces.
theorem
for X being non empty TopSpace, X1,X2 being non empty SubSpace of X holds
X1 meets X2 implies (X1,X2 are_weakly_separated iff
(X1 is SubSpace of X2 or X2 is SubSpace of X1 or
ex Y1, Y2 being closed non empty SubSpace of X st
Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 &
(X1 union X2 is SubSpace of Y1 union Y2 or
ex Y being open non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2)))
proof let X be non empty TopSpace, X1,X2 be non empty SubSpace of X;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
A1: [#]X = the carrier of X by PRE_TOPC:12;
A2: X is SubSpace of X by Th2;
assume A3: X1 meets X2;
A4:now assume X1,X2 are_weakly_separated;
then A5: A1,A2 are_weakly_separated by Def9;
now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
then A6: not A1 c= A2 & not A2 c= A1 by Th4;
then consider C1, C2 being non empty Subset of X such that
A7: C1 is closed & C2 is closed and
A8: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 and
A9: A1 \/ A2 c= C1 \/ C2 or
ex C being non empty Subset of X st C is open &
C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C
by A5,Th60;
A10:now assume C1 misses (A1 \/ A2);
then A11: C1 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
now per cases;
suppose A1 \/ A2 c= C1 \/ C2;
then A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= {} \/ (C2 /\ (A1 \/ A2)) by A11,XBOOLE_1:23
.= C2 /\ (A1 \/ A2);
then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by A8,XBOOLE_1:7;
hence contradiction by A6,XBOOLE_1:1;
suppose not A1 \/ A2 c= C1 \/ C2;
then consider C being non empty Subset of X
such that
A12: C is open & C /\ (A1 \/ A2) c= A1 /\ A2 and
A13: the carrier of X = (C1 \/ C2) \/ C by A9;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,A13,PRE_TOPC:15
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A11,XBOOLE_1:23
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
then A1 \/ A2 c= A2 \/ A1 /\ A2 & A1 /\ A2 c= A2
by A8,A12,XBOOLE_1:13,17;
then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by XBOOLE_1:7,12;
hence contradiction by A6,XBOOLE_1:1;
end;
hence contradiction;
end;
A14:now assume C2 misses (A1 \/ A2);
then A15: C2 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
now per cases;
suppose A1 \/ A2 c= C1 \/ C2;
then A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ {} by A15,XBOOLE_1:23
.= C1 /\ (A1 \/ A2);
then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by A8,XBOOLE_1:7;
hence contradiction by A6,XBOOLE_1:1;
suppose not A1 \/ A2 c= C1 \/ C2;
then consider C being non empty Subset of X such that
A16: C is open & C /\ (A1 \/ A2) c= A1 /\ A2 and
A17: the carrier of X = (C1 \/ C2) \/ C by A9;
A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A1,A17,PRE_TOPC:15
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A15,XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
then A1 \/ A2 c= A1 \/ A1 /\ A2 & A1 /\ A2 c= A1
by A8,A16,XBOOLE_1:13,17;
then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by XBOOLE_1:7,12;
hence contradiction by A6,XBOOLE_1:1;
end;
hence contradiction;
end;
thus ex Y1, Y2 being closed non empty SubSpace of X st
Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 &
(X1 union X2 is SubSpace of Y1 union Y2 or
ex Y being open non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2)
proof
consider Y1 being strict closed non empty SubSpace of X such that
A18: C1 = the carrier of Y1 by A7,Th15;
consider Y2 being strict closed non empty SubSpace of X such that
A19: C2 = the carrier of Y2 by A7,Th15;
take Y1,Y2;
A20: the carrier of X1 union X2 = A1 \/ A2 &
the carrier of Y1 union Y2 = C1 \/ C2 by A18,A19,Def2;
then Y1 meets (X1 union X2) & Y2 meets (X1 union X2)
by A10,A14,A18,A19,Def3;
then A21: the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) &
the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2)
by A18,A19,A20,Def5;
now assume A22: not X1 union X2 is SubSpace of Y1 union Y2;
then A23: not A1 \/ A2 c= C1 \/ C2 by A20,Th4;
consider C being non empty Subset of X such that
A24: C is open & C /\ (A1 \/ A2) c= A1 /\ A2 &
the carrier of X = (C1 \/ C2) \/ C by A9,A20,A22,Th4;
thus ex Y being open non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2
proof
consider Y being strict open non empty SubSpace of X such that
A25: C = the carrier of Y by A24,Th20;
take Y;
A26: the carrier of X = (the carrier of Y1 union Y2) \/ C
by A18,A19,A24,Def2
.= the carrier of (Y1 union Y2) union Y by A25,Def2;
now assume C misses (A1 \/ A2);
then A27: C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,A24,PRE_TOPC:
15
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A27,XBOOLE_1:23
.= (C1 \/ C2) /\ (A1 \/ A2);
hence contradiction by A23,XBOOLE_1:17;
end;
then Y meets (X1 union X2) by A20,A25,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) &
the carrier of X1 meet X2 = A1 /\ A2 by A3,A20,A25,Def5;
hence thesis by A2,A24,A26,Th4,Th5;
end;
end;
hence thesis by A8,A21,Th4;
end;
end;
hence X1 is SubSpace of X2 or X2 is SubSpace of X1
or ex Y1, Y2 being closed non empty SubSpace of X st
Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 &
(X1 union X2 is SubSpace of Y1 union Y2
or ex Y being open non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2);
end;
now assume A28:
X1 is SubSpace of X2 or X2 is SubSpace of X1
or ex Y1, Y2 being closed non empty SubSpace of X st
Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 &
(X1 union X2 is SubSpace of Y1 union Y2
or ex Y being open non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2);
now assume A29: not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
then consider Y1, Y2 being closed non empty SubSpace of X such that
A30: Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 and
A31: X1 union X2 is SubSpace of Y1 union Y2 or
ex Y being open non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2 by A28;
the carrier of Y1 is Subset of X by Th1;
then reconsider C1 = the carrier of Y1 as Subset of X;
the carrier of Y2 is Subset of X by Th1;
then reconsider C2 = the carrier of Y2 as Subset of X;
A32: C1 is closed & C2 is closed by Th11;
A33: the carrier of X1 union X2 = A1 \/ A2 &
the carrier of Y1 union Y2 = C1 \/ C2 by Def2;
A34:now assume Y1 misses (X1 union X2);
then A35: C1 misses (A1 \/ A2) by A33,Def3;
now per cases;
suppose X1 union X2 is SubSpace of Y1 union Y2;
then A1 \/ A2 c= C1 \/ C2 by A33,Th4;
then A36: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ (C2 /\ (A1 \/ A2)) by A35,XBOOLE_0:def 7
.= C2 /\ (A1 \/ A2);
then C2 meets (A1 \/ A2) by A33,XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A33,Def3;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2)
by A33,Def5;
hence A1 \/ A2 c= A2 by A30,A36,Th4;
suppose not X1 union X2 is SubSpace of Y1 union Y2;
then consider Y being open non empty SubSpace of X such that
A37: the TopStruct of X = (Y1 union Y2) union Y and
A38: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A31;
reconsider C = the carrier of Y as Subset of X
by Th1;
the carrier of X = (C1 \/ C2) \/ C by A33,A37,Def2;
then A39:A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/
A2)) by XBOOLE_1:23
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A35,XBOOLE_0:def 7
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A40: now assume C2 /\ (A1 \/ A2) <> {};
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A33,Def3;
then A41: the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/
A2)
by A33,Def5;
then A42: C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
now per cases;
suppose C /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A2 by A30,A39,A41,Th4;
suppose C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A33,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/
A2)
& the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A38,Th4;
then A1 \/ A2 c= A2 \/ A1 /\ A2 & A1 /\ A2 c= A2
by A39,A42,XBOOLE_1:13,17;
hence A1 \/ A2 c= A2 by XBOOLE_1:12;
end;
hence A1 \/ A2 c= A2;
end;
now assume C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A33,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
& the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then A43: C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A2
by A38,Th4,XBOOLE_1:17;
then A44: C /\ (A1 \/ A2) c= A2 by XBOOLE_1:1;
now per cases;
suppose C2 /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A2 by A39,A43,XBOOLE_1:1;
suppose C2 /\ (A1 \/ A2) <> {};
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A33,Def3;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/
A2) by A33,Def5;
then C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
hence A1 \/ A2 c= A2 by A39,A44,XBOOLE_1:8;
end;
hence A1 \/ A2 c= A2;
end;
hence A1 \/ A2 c= A2 by A33,A39,A40;
end;
then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by XBOOLE_1:7;
then A1 c= A2 by XBOOLE_1:1;
hence contradiction by A29,Th4;
end;
now assume not Y2 meets (X1 union X2);
then A45: C2 misses (A1 \/ A2) by A33,Def3;
now per cases;
suppose X1 union X2 is SubSpace of Y1 union Y2;
then A1 \/ A2 c= C1 \/ C2 by A33,Th4;
then A46: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/
A2)) by XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ {} by A45,XBOOLE_0:def 7
.= C1 /\ (A1 \/ A2);
then C1 meets (A1 \/ A2) by A33,XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A33,Def3;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2)
by A33,Def5;
hence A1 \/ A2 c= A1 by A30,A46,Th4;
suppose not X1 union X2 is SubSpace of Y1 union Y2;
then consider Y being open non empty SubSpace of X such that
A47: the TopStruct of X = (Y1 union Y2) union Y and
A48: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A31;
reconsider C = the carrier of Y as Subset of X
by Th1;
the carrier of X = (C1 \/ C2) \/ C by A33,A47,Def2;
then A49:A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/
A2)) by XBOOLE_1:23
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A45,XBOOLE_0:def 7
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A50: now assume C1 /\ (A1 \/ A2) <> {};
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A33,Def3;
then A51: the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/
A2)
by A33,Def5;
then A52: C1 /\ (A1 \/ A2) c= A1 by A30,Th4;
now per cases;
suppose C /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A1 by A30,A49,A51,Th4;
suppose C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A33,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/
A2)
& the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A48,Th4;
then A1 \/ A2 c= A1 \/ A1 /\ A2 & A1 /\ A2 c= A1
by A49,A52,XBOOLE_1:13,17;
hence A1 \/ A2 c= A1 by XBOOLE_1:12;
end;
hence A1 \/ A2 c= A1;
end;
now assume C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A33,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
& the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then A53: C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A1
by A48,Th4,XBOOLE_1:17;
then A54: C /\ (A1 \/ A2) c= A1 by XBOOLE_1:1;
now per cases;
suppose C1 /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A1 by A49,A53,XBOOLE_1:1;
suppose C1 /\ (A1 \/ A2) <> {};
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A33,Def3;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/
A2) by A33,Def5;
then C1 /\ (A1 \/ A2) c= A1 by A30,Th4;
hence A1 \/ A2 c= A1 by A49,A54,XBOOLE_1:8;
end;
hence A1 \/ A2 c= A1;
end;
hence A1 \/ A2 c= A1 by A33,A49,A50;
end;
then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by XBOOLE_1:7;
then A2 c= A1 by XBOOLE_1:1;
hence contradiction by A29,Th4;
end;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) &
the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A33,A34,Def5;
then A55: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
now per cases;
suppose A56: A1 \/ A2 c= C1 \/ C2;
thus ex C being Subset of X
st the carrier of X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 & C is open
proof
take C = (C1 \/ C2)`;
A57: C1 \/ C2 is closed by A32,TOPS_1:36;
C misses (A1 \/ A2) by A56,TOPS_1:20;
then C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
hence thesis by A1,A57,PRE_TOPC:18,TOPS_1:29,XBOOLE_1:2;
end;
suppose A58: not A1 \/ A2 c= C1 \/ C2;
thus ex C being Subset of X
st the carrier of X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 & C is open
proof
consider Y being open non empty SubSpace of X such that
A59: the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2
by A31,A33,A58,Th4;
the carrier of Y is Subset of X by Th1;
then reconsider C = the carrier of Y as Subset of X;
A60: C is open by Th16;
now assume not Y meets (X1 union X2);
then A61: C misses (A1 \/ A2) by A33,Def3;
the carrier of X = (C1 \/ C2) \/ C by A33,A59,Def2;
then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC
:15
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/
A2)) by XBOOLE_1:23
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A61,XBOOLE_0:def 7
.= (C1 \/ C2) /\ (A1 \/ A2);
hence contradiction by A58,XBOOLE_1:17;
end;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) &
the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then A62: C /\ (A1 \/ A2) c= A1 /\ A2 by A59,Th4;
the carrier of X = (the carrier of Y1 union Y2) \/ C by A59,
Def2
.= (C1 \/ C2) \/ C by Def2;
hence thesis by A60,A62;
end;
end;
then for A1, A2 be Subset of X holds
A1 = the carrier of X1 & A2 = the carrier of X2 implies
A1,A2 are_weakly_separated by A32,A55,Th59;
hence X1,X2 are_weakly_separated by Def9;
end;
hence X1,X2 are_weakly_separated by Th86;
end;
hence thesis by A4;
end;
theorem
X = X1 union X2 & X1 meets X2 implies
(X1,X2 are_weakly_separated iff
(X1 is SubSpace of X2 or X2 is SubSpace of X1 or
ex Y1, Y2 being closed non empty SubSpace of X st
Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
(X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2)))
proof assume A1: X = X1 union X2;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
A2: A1 \/ A2 = the carrier of X by A1,Def2;
assume A3: X1 meets X2;
A4:now assume X1,X2 are_weakly_separated;
then A5: A1,A2 are_weakly_separated by Def9;
now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
then not A1 c= A2 & not A2 c= A1 by Th4;
then consider C1, C2 being non empty Subset of X such that
A6: C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 and
A7: A1 \/ A2 = C1 \/ C2 or
ex C being non empty Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
by A2,A5,Th62;
thus ex Y1, Y2 being closed non empty SubSpace of X
st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
(X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2)
proof
consider Y1 being strict closed non empty SubSpace of X such that
A8: C1 = the carrier of Y1 by A6,Th15;
consider Y2 being strict closed non empty SubSpace of X such that
A9: C2 = the carrier of Y2 by A6,Th15;
take Y1,Y2;
now assume X <> Y1 union Y2;
then consider C being non empty Subset of X such that
A10: A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
by A1,A2,A7,A8,A9,Def2;
thus ex Y being open non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2
proof
consider Y being strict open non empty SubSpace of X such that
A11: C = the carrier of Y by A10,Th20;
take Y;
A12: the carrier of X = (the carrier of Y1 union Y2) \/ C
by A2,A8,A9,A10,Def2
.= the carrier of (Y1 union Y2) union Y by A11,Def2;
C c= the carrier of X1 meet X2 by A3,A10,Def5;
hence thesis by A1,A11,A12,Th4,Th5;
end;
end;
hence thesis by A6,A8,A9,Th4;
end;
end;
hence X1 is SubSpace of X2 or X2 is SubSpace of X1
or ex Y1, Y2 being closed non empty SubSpace of X st
Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
(X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2);
end;
now assume A13:
X1 is SubSpace of X2 or X2 is SubSpace of X1
or (not X1 is SubSpace of X2 & not X2 is SubSpace of X1 implies
ex Y1, Y2 being closed non empty SubSpace of X st
Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
(X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2));
now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
then consider Y1, Y2 being closed non empty SubSpace of X
such that
A14: Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and
A15: X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 by A13;
the carrier of Y1 is Subset of X by Th1;
then reconsider C1 = the carrier of Y1 as Subset of X;
the carrier of Y2 is Subset of X by Th1;
then reconsider C2 = the carrier of Y2 as Subset of X;
A16: C1 is closed & C2 is closed by Th11;
A17: C1 c= A1 & C2 c= A2 by A14,Th4;
now per cases;
suppose A18: A1 \/ A2 = C1 \/ C2;
thus ex C being Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
proof
take {}X;
thus thesis by A18,XBOOLE_1:2;
end;
suppose A19: A1 \/ A2 <> C1 \/ C2;
thus ex C being Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
proof
consider Y being open non empty SubSpace of X such that
A20: X = (Y1 union Y2) union Y &
Y is SubSpace of X1 meet X2 by A2,A15,A19,Def2;
the carrier of Y is Subset of X by Th1;
then reconsider C = the carrier of Y as Subset of X;
A21: C is open by Th16;
A1 /\ A2 = the carrier of X1 meet X2 by A3,Def5;
then A22: C c= A1 /\ A2 by A20,Th4;
A1 \/ A2 = (the carrier of Y1 union Y2) \/ C by A2,A20,Def2
.= (C1 \/ C2) \/ C by Def2;
hence thesis by A21,A22;
end;
end;
then for A1, A2 be Subset of X holds
A1 = the carrier of X1 & A2 = the carrier of X2 implies
A1,A2 are_weakly_separated by A2,A16,A17,Th61;
hence X1,X2 are_weakly_separated by Def9;
end;
hence X1,X2 are_weakly_separated by Th86;
end;
hence thesis by A4;
end;
theorem
X = X1 union X2 & X1 misses X2 implies
(X1,X2 are_weakly_separated iff
X1 is closed SubSpace of X & X2 is closed SubSpace of X)
proof
assume A1: X = X1 union X2;
assume A2: X1 misses X2;
thus X1,X2 are_weakly_separated implies
X1 is closed SubSpace of X & X2 is closed SubSpace of X
proof
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X;
A1 \/ A2 = the carrier of X by A1,Def2;
then A3: A1 \/ A2 = [#]X by PRE_TOPC:12;
assume X1,X2 are_weakly_separated;
then X1,X2 are_separated by A2,Th85;
then A1,A2 are_separated by Def8;
then A1 is closed & A2 is closed by A3,CONNSP_1:5;
hence thesis by Th11;
end;
thus X1 is closed SubSpace of X & X2 is closed SubSpace of X implies
X1,X2 are_weakly_separated by Th87;
end;
::Second Characterization of Weakly Separated Subspaces of Topological Spaces.
theorem
for X being non empty TopSpace, X1,X2 being non empty SubSpace of X holds
X1 meets X2 implies (X1,X2 are_weakly_separated iff
(X1 is SubSpace of X2 or X2 is SubSpace of X1 or
ex Y1, Y2 being open non empty SubSpace of X st
Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 &
(X1 union X2 is SubSpace of Y1 union Y2 or
ex Y being closed non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2)))
proof let X be non empty TopSpace, X1,X2 be non empty SubSpace of X;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
A1: [#]X = the carrier of X by PRE_TOPC:12;
A2: X is SubSpace of X by Th2;
assume A3: X1 meets X2;
A4:now assume X1,X2 are_weakly_separated;
then A5: A1,A2 are_weakly_separated by Def9;
now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
then A6: not A1 c= A2 & not A2 c= A1 by Th4;
then consider C1, C2 being non empty Subset of X such that
A7: C1 is open & C2 is open and
A8: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 and
A9: A1 \/ A2 c= C1 \/ C2 or
ex C being non empty Subset of X st C is closed &
C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C
by A5,Th64;
A10:now assume C1 misses (A1 \/ A2);
then A11: C1 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
now per cases;
suppose A1 \/ A2 c= C1 \/ C2;
then A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= {} \/ (C2 /\ (A1 \/ A2)) by A11,XBOOLE_1:23
.= C2 /\ (A1 \/ A2);
then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by A8,XBOOLE_1:7;
hence contradiction by A6,XBOOLE_1:1;
suppose not A1 \/ A2 c= C1 \/ C2;
then consider C being non empty Subset of X such that
A12: C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 and
A13: the carrier of X = (C1 \/ C2) \/ C by A9;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,A13,PRE_TOPC:15
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A11,XBOOLE_1:23
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
then A1 \/ A2 c= A2 \/ A1 /\ A2 & A1 /\ A2 c= A2
by A8,A12,XBOOLE_1:13,17;
then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by XBOOLE_1:7,12
;
hence contradiction by A6,XBOOLE_1:1;
end;
hence contradiction;
end;
A14:now assume C2 misses (A1 \/ A2);
then A15: C2 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
now per cases;
suppose A1 \/ A2 c= C1 \/ C2;
then A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ {} by A15,XBOOLE_1:23
.= C1 /\ (A1 \/ A2);
then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by A8,XBOOLE_1:7;
hence contradiction by A6,XBOOLE_1:1;
suppose not A1 \/ A2 c= C1 \/ C2;
then consider C being non empty Subset of X such that
A16: C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 and
A17: the carrier of X = (C1 \/ C2) \/ C by A9;
A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A1,A17,PRE_TOPC:15
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A15,XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
then A1 \/ A2 c= A1 \/ A1 /\ A2 & A1 /\ A2 c= A1
by A8,A16,XBOOLE_1:13,17;
then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by XBOOLE_1:7,12
;
hence contradiction by A6,XBOOLE_1:1;
end;
hence contradiction;
end;
thus ex Y1, Y2 being open non empty SubSpace of X st
Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 &
(X1 union X2 is SubSpace of Y1 union Y2 or
ex Y being closed non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2)
proof
consider Y1 being strict open non empty SubSpace of X such that
A18: C1 = the carrier of Y1 by A7,Th20;
consider Y2 being strict open non empty SubSpace of X such that
A19: C2 = the carrier of Y2 by A7,Th20;
take Y1,Y2;
A20: the carrier of X1 union X2 = A1 \/ A2 &
the carrier of Y1 union Y2 = C1 \/ C2 by A18,A19,Def2;
then Y1 meets (X1 union X2) & Y2 meets (X1 union X2)
by A10,A14,A18,A19,Def3;
then A21: the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) &
the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2)
by A18,A19,A20,Def5;
now assume A22:not X1 union X2 is SubSpace of Y1 union Y2;
then A23: not A1 \/ A2 c= C1 \/ C2 by A20,Th4;
consider C being non empty Subset of X such that
A24: C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 &
the carrier of X = (C1 \/ C2) \/ C by A9,A20,A22,Th4;
thus ex Y being closed non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2
proof
consider Y being strict closed non empty SubSpace of X such that
A25: C = the carrier of Y by A24,Th15;
take Y;
A26: the carrier of X = (the carrier of Y1 union Y2) \/ C
by A18,A19,A24,Def2
.= the carrier of (Y1 union Y2) union Y by A25,Def2;
now assume C misses (A1 \/ A2);
then A27: C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,A24,PRE_TOPC:
15
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A27,XBOOLE_1:23
.= (C1 \/ C2) /\ (A1 \/ A2);
hence contradiction by A23,XBOOLE_1:17;
end;
then Y meets (X1 union X2) by A20,A25,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) &
the carrier of X1 meet X2 = A1 /\ A2 by A3,A20,A25,Def5;
hence thesis by A2,A24,A26,Th4,Th5;
end;
end;
hence thesis by A8,A21,Th4;
end;
end;
hence X1 is SubSpace of X2 or X2 is SubSpace of X1
or ex Y1, Y2 being open non empty SubSpace of X st
Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 &
(X1 union X2 is SubSpace of Y1 union Y2
or ex Y being closed non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2);
end;
now assume A28:
X1 is SubSpace of X2 or X2 is SubSpace of X1
or ex Y1, Y2 being open non empty SubSpace of X st
Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 &
(X1 union X2 is SubSpace of Y1 union Y2
or ex Y being closed non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2);
now assume A29: not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
then consider Y1, Y2 being open non empty SubSpace of X
such that
A30: Y1 meet (X1 union X2) is SubSpace of X1 &
Y2 meet (X1 union X2) is SubSpace of X2 and
A31: X1 union X2 is SubSpace of Y1 union Y2 or
ex Y being closed non empty SubSpace of X st
the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2 by A28;
the carrier of Y1 is Subset of X by Th1;
then reconsider C1 = the carrier of Y1 as Subset of X;
the carrier of Y2 is Subset of X by Th1;
then reconsider C2 = the carrier of Y2 as Subset of X;
A32: C1 is open & C2 is open by Th16;
A33: the carrier of X1 union X2 = A1 \/ A2 &
the carrier of Y1 union Y2 = C1 \/ C2 by Def2;
A34:now assume Y1 misses (X1 union X2);
then A35: C1 misses (A1 \/ A2) by A33,Def3;
now per cases;
suppose X1 union X2 is SubSpace of Y1 union Y2;
then A1 \/ A2 c= C1 \/ C2 by A33,Th4;
then A36: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/
A2)) by XBOOLE_1:23
.= {} \/ (C2 /\ (A1 \/ A2)) by A35,XBOOLE_0:def 7
.= C2 /\ (A1 \/ A2);
then C2 meets (A1 \/ A2) by A33,XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A33,Def3;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2)
by A33,Def5;
hence A1 \/ A2 c= A2 by A30,A36,Th4;
suppose not X1 union X2 is SubSpace of Y1 union Y2;
then consider Y being closed non empty SubSpace of X such that
A37: the TopStruct of X = (Y1 union Y2) union Y and
A38: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A31;
reconsider C = the carrier of Y as Subset of X
by Th1;
the carrier of X = (C1 \/ C2) \/ C by A33,A37,Def2;
then A39:A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/
A2)) by XBOOLE_1:23
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A35,XBOOLE_0:def 7
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A40: now assume C2 /\ (A1 \/ A2) <> {};
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A33,Def3;
then A41: the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/
A2)
by A33,Def5;
then A42: C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
now per cases;
suppose C /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A2 by A30,A39,A41,Th4;
suppose C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A33,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/
A2)
& the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A38,Th4;
then A1 \/ A2 c= A2 \/ A1 /\ A2 & A1 /\ A2 c= A2
by A39,A42,XBOOLE_1:13,17;
hence A1 \/ A2 c= A2 by XBOOLE_1:12;
end;
hence A1 \/ A2 c= A2;
end;
now assume C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A33,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
& the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then A43: C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A2
by A38,Th4,XBOOLE_1:17;
then A44: C /\ (A1 \/ A2) c= A2 by XBOOLE_1:1;
now per cases;
suppose C2 /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A2 by A39,A43,XBOOLE_1:1;
suppose C2 /\ (A1 \/ A2) <> {};
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A33,Def3;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/
A2) by A33,Def5;
then C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
hence A1 \/ A2 c= A2 by A39,A44,XBOOLE_1:8;
end;
hence A1 \/ A2 c= A2;
end;
hence A1 \/ A2 c= A2 by A33,A39,A40;
end;
then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by XBOOLE_1:7;
then A1 c= A2 by XBOOLE_1:1;
hence contradiction by A29,Th4;
end;
now assume not Y2 meets (X1 union X2);
then A45: C2 misses (A1 \/ A2) by A33,Def3;
now per cases;
suppose X1 union X2 is SubSpace of Y1 union Y2;
then A1 \/ A2 c= C1 \/ C2 by A33,Th4;
then A46: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/
A2)) by XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ {} by A45,XBOOLE_0:def 7
.= C1 /\ (A1 \/ A2);
then C1 meets (A1 \/ A2) by A33,XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A33,Def3;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2)
by A33,Def5;
hence A1 \/ A2 c= A1 by A30,A46,Th4;
suppose not X1 union X2 is SubSpace of Y1 union Y2;
then consider Y being closed non empty SubSpace of X such that
A47: the TopStruct of X = (Y1 union Y2) union Y and
A48: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A31;
reconsider C = the carrier of Y as Subset of X
by Th1;
the carrier of X = (C1 \/ C2) \/ C by A33,A47,Def2;
then A49:A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/
A2)) by XBOOLE_1:23
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A45,XBOOLE_0:def 7
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A50: now assume C1 /\ (A1 \/ A2) <> {};
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A33,Def3;
then A51: the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/
A2)
by A33,Def5;
then A52: C1 /\ (A1 \/ A2) c= A1 by A30,Th4;
now per cases;
suppose C /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A1 by A30,A49,A51,Th4;
suppose C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A33,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/
A2)
& the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A48,Th4;
then A1 \/ A2 c= A1 \/ A1 /\ A2 & A1 /\ A2 c= A1
by A49,A52,XBOOLE_1:13,17;
hence A1 \/ A2 c= A1 by XBOOLE_1:12;
end;
hence A1 \/ A2 c= A1;
end;
now assume C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A33,Def3;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
& the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then A53: C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A1
by A48,Th4,XBOOLE_1:17;
then A54: C /\ (A1 \/ A2) c= A1 by XBOOLE_1:1;
now per cases;
suppose C1 /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A1 by A49,A53,XBOOLE_1:1;
suppose C1 /\ (A1 \/ A2) <> {};
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A33,Def3;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/
A2) by A33,Def5;
then C1 /\ (A1 \/ A2) c= A1 by A30,Th4;
hence A1 \/ A2 c= A1 by A49,A54,XBOOLE_1:8;
end;
hence A1 \/ A2 c= A1;
end;
hence A1 \/ A2 c= A1 by A33,A49,A50;
end;
then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by XBOOLE_1:7;
then A2 c= A1 by XBOOLE_1:1;
hence contradiction by A29,Th4;
end;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) &
the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A33,A34,Def5;
then A55: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
now per cases;
suppose A56: A1 \/ A2 c= C1 \/ C2;
thus ex C being Subset of X
st the carrier of X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed
proof
take C = (C1 \/ C2)`;
A57: C1 \/ C2 is open by A32,TOPS_1:37;
C misses (A1 \/ A2) by A56,TOPS_1:20;
then C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
hence thesis by A1,A57,PRE_TOPC:18,TOPS_1:30,XBOOLE_1:2;
end;
suppose A58: not A1 \/ A2 c= C1 \/ C2;
thus ex C being Subset of X
st the carrier of X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed
proof
consider Y being closed non empty SubSpace of X such that
A59: the TopStruct of X = (Y1 union Y2) union Y &
Y meet (X1 union X2) is SubSpace of X1 meet X2
by A31,A33,A58,Th4;
the carrier of Y is Subset of X by Th1;
then reconsider C = the carrier of Y as Subset of X
;
A60: C is closed by Th11;
now assume not Y meets (X1 union X2);
then A61: C misses (A1 \/ A2) by A33,Def3;
the carrier of X = (C1 \/ C2) \/ C by A33,A59,Def2;
then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/
A2)) by XBOOLE_1:23
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A61,XBOOLE_0:def 7
.= (C1 \/ C2) /\ (A1 \/ A2);
hence contradiction by A58,XBOOLE_1:17;
end;
then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) &
the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
then A62: C /\ (A1 \/ A2) c= A1 /\ A2 by A59,Th4;
the carrier of X = (the carrier of Y1 union Y2) \/ C by A59,
Def2
.= (C1 \/ C2) \/ C by Def2;
hence thesis by A60,A62;
end;
end;
then for A1, A2 be Subset of X holds
A1 = the carrier of X1 & A2 = the carrier of X2 implies
A1,A2 are_weakly_separated by A32,A55,Th63;
hence X1,X2 are_weakly_separated by Def9;
end;
hence X1,X2 are_weakly_separated by Th86;
end;
hence thesis by A4;
end;
theorem
X = X1 union X2 & X1 meets X2 implies
(X1,X2 are_weakly_separated iff
(X1 is SubSpace of X2 or X2 is SubSpace of X1 or
ex Y1, Y2 being open non empty SubSpace of X st
Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
(X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2)))
proof
assume A1: X = X1 union X2;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
A2: A1 \/ A2 = the carrier of X by A1,Def2;
assume A3: X1 meets X2;
A4:now assume X1,X2 are_weakly_separated;
then A5: A1,A2 are_weakly_separated by Def9;
now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
then not A1 c= A2 & not A2 c= A1 by Th4;
then consider C1, C2 being non empty Subset of X such that
A6: C1 is open & C2 is open & C1 c= A1 & C2 c= A2 and
A7: A1 \/ A2 = C1 \/ C2 or
ex C being non empty Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
by A2,A5,Th66;
thus ex Y1, Y2 being open non empty SubSpace of X
st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
(X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2)
proof
consider Y1 being strict open non empty SubSpace of X such that
A8: C1 = the carrier of Y1 by A6,Th20;
consider Y2 being strict open non empty SubSpace of X such that
A9: C2 = the carrier of Y2 by A6,Th20;
take Y1,Y2;
now assume X <> Y1 union Y2;
then consider C being non empty Subset of X such that
A10: A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
by A1,A2,A7,A8,A9,Def2;
thus ex Y being closed non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2
proof
consider Y being strict closed non empty SubSpace of X such that
A11: C = the carrier of Y by A10,Th15;
take Y;
A12: the carrier of X = (the carrier of Y1 union Y2) \/ C
by A2,A8,A9,A10,Def2
.= the carrier of (Y1 union Y2) union Y by A11,Def2;
C c= the carrier of X1 meet X2 by A3,A10,Def5;
hence thesis by A1,A11,A12,Th4,Th5;
end;
end;
hence thesis by A6,A8,A9,Th4;
end;
end;
hence X1 is SubSpace of X2 or X2 is SubSpace of X1 or
ex Y1, Y2 being open non empty SubSpace of X st
Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
(X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2);
end;
now assume A13:
X1 is SubSpace of X2 or X2 is SubSpace of X1 or
ex Y1, Y2 being open non empty SubSpace of X st
Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
(X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2);
now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
then consider Y1, Y2 being open non empty SubSpace of X such that
A14: Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and
A15: X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 by A13;
the carrier of Y1 is Subset of X by Th1;
then reconsider C1 = the carrier of Y1 as Subset of X;
the carrier of Y2 is Subset of X by Th1;
then reconsider C2 = the carrier of Y2 as Subset of X;
A16: C1 is open & C2 is open by Th16;
A17: C1 c= A1 & C2 c= A2 by A14,Th4;
now per cases;
suppose A18: A1 \/ A2 = C1 \/ C2;
thus ex C being Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
proof
take {}X;
thus thesis by A18,XBOOLE_1:2;
end;
suppose A19: A1 \/ A2 <> C1 \/ C2;
thus ex C being Subset of X st
A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
proof
consider Y being closed non empty SubSpace of X such that
A20: X = (Y1 union Y2) union Y &
Y is SubSpace of X1 meet X2 by A2,A15,A19,Def2;
the carrier of Y is Subset of X by Th1;
then reconsider C = the carrier of Y as Subset of X
;
A21: C is closed by Th11;
A1 /\ A2 = the carrier of X1 meet X2 by A3,Def5;
then A22: C c= A1 /\ A2 by A20,Th4;
A1 \/ A2 = (the carrier of Y1 union Y2) \/ C by A2,A20,Def2
.= (C1 \/ C2) \/ C by Def2;
hence thesis by A21,A22;
end;
end;
then for A1, A2 be Subset of X holds
A1 = the carrier of X1 & A2 = the carrier of X2 implies
A1,A2 are_weakly_separated by A2,A16,A17,Th65;
hence X1,X2 are_weakly_separated by Def9;
end;
hence X1,X2 are_weakly_separated by Th86;
end;
hence thesis by A4;
end;
theorem
X = X1 union X2 & X1 misses X2 implies
(X1,X2 are_weakly_separated iff
X1 is open SubSpace of X & X2 is open SubSpace of X)
proof
assume A1: X = X1 union X2;
assume A2: X1 misses X2;
thus X1,X2 are_weakly_separated implies
X1 is open SubSpace of X & X2 is open SubSpace of X
proof
the carrier of X1 is Subset of X by Th1;
then reconsider A1 = the carrier of X1 as Subset of X;
the carrier of X2 is Subset of X by Th1;
then reconsider A2 = the carrier of X2 as Subset of X;
A1 \/ A2 = the carrier of X by A1,Def2;
then A3: A1 \/ A2 = [#]X by PRE_TOPC:12;
assume X1,X2 are_weakly_separated;
then X1,X2 are_separated by A2,Th85;
then A1,A2 are_separated by Def8;
then A1 is open & A2 is open by A3,CONNSP_1:5;
hence thesis by Th16;
end;
thus X1 is open SubSpace of X & X2 is open SubSpace of X implies
X1,X2 are_weakly_separated by Th88;
end;
::A Characterization of Separated Subspaces by means of Weakly Separated ones.
theorem
X1,X2 are_separated iff ex Y1, Y2 being non empty SubSpace of X st
Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
(Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
proof
thus X1,X2 are_separated implies ex Y1, Y2 being non empty SubSpace of X st
Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2
& (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
proof assume X1,X2 are_separated;
then consider Y1, Y2 being open non empty SubSpace of X
such that A1: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A2: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 by Th83;
take Y1,Y2;
thus thesis by A1,A2,Th88;
end;
given Y1, Y2 being non empty SubSpace of X such that
A3: Y1,Y2 are_weakly_separated and
A4: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A5: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
now let A1, A2 be Subset of X such that
A6: A1 = the carrier of X1 & A2 = the carrier of X2;
now per cases;
suppose Y1 misses Y2;
then Y1,Y2 are_separated by A3,Th85;
then A7: C1,C2 are_separated & A1 c= C1 & A2 c= C2 by A4,A6,Def8,Th4;
thus A1,A2 are_separated by A7,CONNSP_1:8;
suppose A8: not Y1 misses Y2;
ex B1, B2 being Subset of X st
B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/
A2
proof
take C1,C2;
the carrier of Y1 meet Y2 = C1 /\ C2 &
the carrier of X1 union X2 = A1 \/ A2 by A6,A8,Def2,Def5;
hence thesis by A3,A4,A5,A6,A8,Def3,Def9,Th4;
end;
hence A1,A2 are_separated by Th67;
end;
hence A1,A2 are_separated;
end;
hence X1,X2 are_separated by Def8;
end;