:: On a Duality Between Weakly Separated Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received November 9, 1992
:: Copyright (c) 1992-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, PRE_TOPC, SUBSET_1, STRUCT_0, TARSKI, TOPS_1, RCOMP_1,
TSEP_1, CONNSP_1, SETFAM_1, TSEP_2;
notations TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, STRUCT_0, TOPS_1, BORSUK_1,
CONNSP_1, TSEP_1;
constructors TOPS_1, CONNSP_1, BORSUK_1, TSEP_1;
registrations STRUCT_0, PRE_TOPC;
requirements BOOLE, SUBSET;
definitions BORSUK_1, TSEP_1, XBOOLE_0;
equalities XBOOLE_0, SUBSET_1, STRUCT_0;
expansions BORSUK_1, TSEP_1, XBOOLE_0;
theorems PRE_TOPC, TOPS_1, CONNSP_1, TSEP_1, TDLAT_1, TDLAT_3, SUBSET_1,
XBOOLE_1;
begin :: 1. Certain Set-Decompositions of a Topological Space.
reserve X for non empty 1-sorted;
theorem Th1:
for A, B being Subset of X holds ( A`) \ B` = B \ A
proof
let A, B be Subset of X;
A` \ B` = [#]X \ (A \/ B`) by XBOOLE_1:41;
then A` \ B` = ( A`) /\ B`` by XBOOLE_1:53;
hence thesis by SUBSET_1:13;
end;
:: Complemented Subsets.
definition
let X be 1-sorted, A1, A2 be Subset of X;
pred A1,A2 constitute_a_decomposition means
A1 misses A2 & A1 \/ A2 = the carrier of X;
symmetry;
end;
notation
let X be 1-sorted, A1, A2 be Subset of X;
antonym A1,A2 do_not_constitute_a_decomposition for A1,A2
constitute_a_decomposition;
end;
reserve A, A1, A2, B1, B2 for Subset of X;
theorem
A1,A2 constitute_a_decomposition iff A1 misses A2 & A1 \/ A2 = [#]X;
theorem Th3:
A1,A2 constitute_a_decomposition implies A1 = A2` & A2 = A1`
proof
assume
A1: A1,A2 constitute_a_decomposition;
then
A2: A1 misses A2;
then
A3: A1 c= A2` by SUBSET_1:23;
A4: A2 c= A1` by A2,SUBSET_1:23;
A5: A1 \/ A2 = [#]X by A1;
then A2` c= A1 by TDLAT_1:1;
hence A1 = A2` by A3;
A1` c= A2 by A5,TDLAT_1:1;
hence thesis by A4;
end;
theorem Th4:
A1 = A2` or A2 = A1` implies A1,A2 constitute_a_decomposition
proof
assume A1 = A2` or A2 = A1`;
then A1 misses A2 & A1 \/ A2 = [#]X by SUBSET_1:23,TDLAT_1:1;
hence thesis;
end;
theorem Th5:
A, A` constitute_a_decomposition
proof
A misses A` & A \/ A` = [#]X by PRE_TOPC:2,XBOOLE_1:79;
hence A, A` constitute_a_decomposition;
end;
theorem
{}X,[#]X constitute_a_decomposition
proof
[#]X = ({}X)`;
hence {}X,[#]X constitute_a_decomposition by Th5;
end;
theorem Th7:
A,A do_not_constitute_a_decomposition
proof
assume
A1: A,A constitute_a_decomposition;
per cases;
suppose
A2: A is non empty;
A = A` by A1,Th3;
then A misses A by SUBSET_1:23;
then A /\ A = {};
hence contradiction by A2;
end;
suppose
A is empty;
then {} = A \/ A .= the carrier of X by A1;
hence contradiction;
end;
end;
definition
let X be non empty 1-sorted, A1, A2 be Subset of X;
redefine pred A1,A2 constitute_a_decomposition;
irreflexivity by Th7;
end;
theorem Th8:
A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition
implies A1 = A2
proof
assume A1,A constitute_a_decomposition;
then
A1: A1 = A` by Th3;
assume A,A2 constitute_a_decomposition;
hence thesis by A1,Th3;
end;
reserve X for non empty TopSpace;
reserve A, A1, A2, B1, B2 for Subset of X;
theorem Th9:
A1,A2 constitute_a_decomposition implies (Cl A1),(Int A2)
constitute_a_decomposition & (Int A1),(Cl A2) constitute_a_decomposition
proof
assume
A1: A1,A2 constitute_a_decomposition;
Cl A1 = (Int A1`)` by TDLAT_3:1;
then Cl A1 = (Int A2)` by A1,Th3;
hence (Cl A1),(Int A2) constitute_a_decomposition by Th4;
Int A1 = (Cl A1`)` by TOPS_1:def 1;
then Int A1 = (Cl A2)` by A1,Th3;
hence (Int A1),(Cl A2) constitute_a_decomposition by Th4;
end;
theorem
(Cl A),(Int A`) constitute_a_decomposition &
(Cl A`),(Int A) constitute_a_decomposition &
(Int A),(Cl A`) constitute_a_decomposition &
(Int A`),(Cl A) constitute_a_decomposition
proof
A1: A, A` constitute_a_decomposition by Th5;
hence (Cl A),(Int A`) constitute_a_decomposition by Th9;
A2: A`,A constitute_a_decomposition by Th5;
hence (Cl A`),(Int A) constitute_a_decomposition by Th9;
thus (Int A),(Cl A`) constitute_a_decomposition by A2,Th9;
thus thesis by A1,Th9;
end;
theorem Th11:
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition
holds (A1 is open iff A2 is closed)
proof
let A1, A2 be Subset of X;
assume
A1: A1,A2 constitute_a_decomposition;
then A2 = A1` by Th3;
hence A1 is open implies A2 is closed by TOPS_1:4;
assume
A2: A2 is closed;
A1 = A2` by A1,Th3;
hence thesis by A2,TOPS_1:3;
end;
theorem
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
(A1 is closed iff A2 is open) by Th11;
reserve X for non empty 1-sorted;
reserve A, A1, A2, B1, B2 for Subset of X;
theorem Th13:
A1,A2 constitute_a_decomposition & B1,B2
constitute_a_decomposition implies (A1 /\ B1),(A2 \/ B2)
constitute_a_decomposition
proof
assume
A1: A1,A2 constitute_a_decomposition;
then A1 misses A2;
then
A2: A1 /\ A2 = {};
assume
A3: B1,B2 constitute_a_decomposition;
then
A4: B1 \/ B2 = [#]X;
B1 misses B2 by A3;
then
A5: B1 /\ B2 = {}X;
(A1 /\ B1) /\ (A2 \/ B2) =((B1 /\ A1) /\ A2) \/ ((A1 /\ B1) /\ B2) by
XBOOLE_1:23
.= (B1 /\ (A1 /\ A2)) \/ ((A1 /\ B1) /\ B2) by XBOOLE_1:16
.= (B1 /\ (A1 /\ A2)) \/ (A1 /\ (B1 /\ B2)) by XBOOLE_1:16
.= {}X by A5,A2;
then
A6: (A1 /\ B1) misses (A2 \/ B2);
(A1 /\ B1) \/ (A2 \/ B2) = (A1 \/ (A2 \/ B2)) /\ (B1 \/ (A2 \/ B2)) by
XBOOLE_1:24
.= ((A1 \/ A2) \/ B2) /\ (B1 \/ (B2 \/ A2)) by XBOOLE_1:4
.= ((A1 \/ A2) \/ B2) /\ ((B1 \/ B2) \/ A2) by XBOOLE_1:4
.= ([#]X \/ B2) /\ ([#]X \/ A2) by A1,A4
.= ([#]X \/ B2) /\ [#]X by XBOOLE_1:12
.= [#]X /\ [#]X by XBOOLE_1:12
.= [#]X;
hence thesis by A6;
end;
theorem
A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition
implies (A1 \/ B1),(A2 /\ B2) constitute_a_decomposition by Th13;
begin
:: 2. A Duality Between Pairs of Weakly Separated Subsets.
reserve X for non empty TopSpace,
A1, A2 for Subset of X;
theorem Th15:
for A1, A2, C1, C2 being Subset of X st A1,C1
constitute_a_decomposition & A2,C2 constitute_a_decomposition holds A1,A2
are_weakly_separated iff C1,C2 are_weakly_separated
proof
let A1, A2, C1, C2 be Subset of X;
assume A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition;
then
A1: C1 = A1` & C2 = A2` by Th3;
thus A1,A2 are_weakly_separated implies C1,C2 are_weakly_separated
proof
assume A1 \ A2,A2 \ A1 are_separated;
then C2 \ C1, C2` \ C1` are_separated by A1,Th1;
then C2 \ C1,C1 \ C2 are_separated by Th1;
hence thesis;
end;
assume C1,C2 are_weakly_separated;
then C1 \ C2,C2 \ C1 are_separated;
then C2` \ C1`,C2 \ C1 are_separated by Th1;
then A2 \ A1,A1 \ A2 are_separated by A1,Th1;
hence thesis;
end;
theorem
A1,A2 are_weakly_separated iff A1`, A2` are_weakly_separated
proof
A1, A1` constitute_a_decomposition & A2, A2` constitute_a_decomposition
by Th5;
hence thesis by Th15;
end;
theorem
for A1, A2, C1, C2 being Subset of X st A1,C1
constitute_a_decomposition & A2,C2 constitute_a_decomposition holds A1,A2
are_separated implies C1,C2 are_weakly_separated
proof
let A1, A2, C1, C2 be Subset of X;
assume
A1: A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition;
assume A1,A2 are_separated;
then A1,A2 are_weakly_separated by TSEP_1:46;
hence thesis by A1,Th15;
end;
theorem Th18:
for A1, A2, C1, C2 being Subset of X st A1,C1
constitute_a_decomposition & A2,C2 constitute_a_decomposition holds A1 misses
A2 & C1,C2 are_weakly_separated implies A1,A2 are_separated
proof
let A1, A2, C1, C2 be Subset of X;
assume
A1: A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition;
assume
A2: A1 /\ A2 = {};
assume C1,C2 are_weakly_separated;
then
A3: A1,A2 are_weakly_separated by A1,Th15;
A1 misses A2 by A2;
hence thesis by A3,TSEP_1:46;
end;
theorem
for A1, A2, C1, C2 being Subset of X st A1,C1
constitute_a_decomposition & A2,C2 constitute_a_decomposition holds C1 \/ C2 =
the carrier of X & C1,C2 are_weakly_separated implies A1,A2 are_separated
proof
let A1, A2, C1, C2 be Subset of X;
assume
A1: A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition;
assume C1 \/ C2 = the carrier of X;
then
A2: (C1 \/ C2)` = {}X by XBOOLE_1:37;
A1 = C1` & A2 = C2` by A1,Th3;
then A1 /\ A2 = {} by A2,XBOOLE_1:53;
then
A3: A1 misses A2;
assume C1,C2 are_weakly_separated;
hence thesis by A1,A3,Th18;
end;
theorem
A1,A2 constitute_a_decomposition implies (A1,A2 are_weakly_separated
iff A1,A2 are_separated)
by TSEP_1:46;
theorem Th21:
A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated
proof
A1: (A1 \/ A2) \ A1 = A2 \ A1 & (A1 \/ A2) \ A2 = A1 \ A2 by XBOOLE_1:40;
thus A1,A2 are_weakly_separated implies (A1 \/ A2) \ A1,(A1 \/ A2) \ A2
are_separated
by A1;
assume (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated;
hence thesis by A1;
end;
::An Enlargement Theorem for Subsets.
theorem Th22:
for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1
\/ C2 = A1 \/ A2 holds C1,C2 are_weakly_separated implies A1,A2
are_weakly_separated
proof
let A1, A2, C1, C2 be Subset of X;
assume C1 c= A1 & C2 c= A2;
then
A1: (A1 \/ A2) \ A1 c= (A1 \/ A2) \ C1 & (A1 \/ A2) \ A2 c= (A1 \/ A2) \ C2
by XBOOLE_1:34;
assume
A2: C1 \/ C2 = A1 \/ A2;
assume C1,C2 are_weakly_separated;
then (A1 \/ A2) \ C1,(A1 \/ A2) \ C2 are_separated by A2,Th21;
then (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated by A1,CONNSP_1:7;
hence thesis by Th21;
end;
theorem Th23:
A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated
proof
A1: A2 \ (A1 /\ A2) = A2 \ A1 by XBOOLE_1:47;
A2: A1 \ (A1 /\ A2) = A1 \ A2 by XBOOLE_1:47;
thus A1,A2 are_weakly_separated implies A1 \ (A1 /\ A2),A2 \ (A1 /\ A2)
are_separated
by A2,XBOOLE_1:47;
assume A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated;
hence thesis by A2,A1;
end;
::An Extenuation Theorem for Subsets.
theorem Th24:
for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1
/\ C2 = A1 /\ A2 holds A1,A2 are_weakly_separated implies C1,C2
are_weakly_separated
proof
let A1, A2, C1, C2 be Subset of X;
assume C1 c= A1 & C2 c= A2;
then
A1: C1 \ (C1 /\ C2) c= A1 \ (C1 /\ C2) & C2 \ (C1 /\ C2) c= A2 \ (C1 /\ C2)
by XBOOLE_1:33;
assume
A2: C1 /\ C2 = A1 /\ A2;
assume A1,A2 are_weakly_separated;
then A1 \ (C1 /\ C2),A2 \ (C1 /\ C2) are_separated by A2,Th23;
then C1 \ (C1 /\ C2),C2 \ (C1 /\ C2) are_separated by A1,CONNSP_1:7;
hence thesis by Th23;
end;
::Separated and Weakly Separated Subsets in Subspaces.
reserve X0 for non empty SubSpace of X,
B1, B2 for Subset of X0;
theorem Th25:
B1 = A1 & B2 = A2 implies (A1,A2 are_separated iff B1,B2 are_separated)
proof
assume that
A1: B1 = A1 and
A2: B2 = A2;
A3: Cl B2 = (Cl A2) /\ [#]X0 by A2,PRE_TOPC:17;
A4: Cl B1 = (Cl A1) /\ [#]X0 by A1,PRE_TOPC:17;
thus A1,A2 are_separated implies B1,B2 are_separated
proof
assume
A5: A1,A2 are_separated;
then A1 misses Cl A2 by CONNSP_1:def 1;
then A1 /\ Cl A2 = {};
then B1 /\ Cl B2 = {} /\ [#]X0 by A1,A3,XBOOLE_1:16;
then
A6: B1 misses Cl B2;
Cl A1 misses A2 by A5,CONNSP_1:def 1;
then Cl A1 /\ A2 = {};
then Cl B1 /\ B2 = {} /\ [#]X0 by A2,A4,XBOOLE_1:16;
then Cl B1 misses B2;
hence thesis by A6,CONNSP_1:def 1;
end;
thus B1,B2 are_separated implies A1,A2 are_separated
proof
assume
A7: B1,B2 are_separated;
then ((Cl A1) /\ [#]X0) misses A2 by A2,A4,CONNSP_1:def 1;
then ((Cl A1) /\ [#]X0) /\ A2 = {};
then
A8: (Cl A1 /\ A2) /\ [#]X0 = {} by XBOOLE_1:16;
A1 misses ((Cl A2) /\ [#]X0) by A1,A3,A7,CONNSP_1:def 1;
then A1 /\ ((Cl A2) /\ [#]X0) = {};
then
A9: (A1 /\ Cl A2) /\ [#]X0 = {} by XBOOLE_1:16;
A1 /\ Cl A2 c= A1 by XBOOLE_1:17;
then A1 /\ Cl A2 = {} by A1,A9,XBOOLE_1:1,28;
then
A10: A1 misses Cl A2;
Cl A1 /\ A2 c= A2 by XBOOLE_1:17;
then Cl A1 /\ A2 = {} by A2,A8,XBOOLE_1:1,28;
then Cl A1 misses A2;
hence thesis by A10,CONNSP_1:def 1;
end;
end;
theorem Th26:
B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2
implies (A1,A2 are_separated implies B1,B2 are_separated)
proof
assume
A1: B1 = (the carrier of X0) /\ A1;
then reconsider C1 = B1 as Subset of X;
assume
A2: B2 = (the carrier of X0) /\ A2;
then
A3: B2 c= A2 by XBOOLE_1:17;
reconsider C2 = B2 as Subset of X by A2;
assume
A4: A1,A2 are_separated;
B1 c= A1 by A1,XBOOLE_1:17;
then C1,C2 are_separated by A3,A4,CONNSP_1:7;
hence thesis by Th25;
end;
theorem Th27:
B1 = A1 & B2 = A2 implies (A1,A2 are_weakly_separated iff B1,B2
are_weakly_separated)
by Th25;
theorem Th28:
B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2
implies (A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated)
proof
assume B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2;
then
A1: B1 \ B2 = (the carrier of X0) /\ (A1 \ A2) & B2 \ B1 = (the carrier of
X0) /\ (A2 \ A1) by XBOOLE_1:50;
assume A1 \ A2,A2 \ A1 are_separated;
then B1 \ B2,B2 \ B1 are_separated by A1,Th26;
hence thesis;
end;
begin
:: 3. Certain Subspace-Decompositions of a Topological Space.
definition
let X be non empty TopSpace, X1, X2 be SubSpace of X;
pred X1,X2 constitute_a_decomposition means
for A1, A2 being Subset
of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds A1,A2
constitute_a_decomposition;
symmetry;
end;
notation
let X be non empty TopSpace, X1, X2 be SubSpace of X;
antonym X1,X2 do_not_constitute_a_decomposition for X1,X2
constitute_a_decomposition;
end;
reserve X0, X1, X2, Y1, Y2 for non empty SubSpace of X;
theorem Th29:
X1,X2 constitute_a_decomposition iff X1 misses X2 & the
TopStruct of X = X1 union X2
proof
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
thus X1,X2 constitute_a_decomposition implies X1 misses X2 & the TopStruct
of X = X1 union X2
proof
assume for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
carrier of X2 holds A1,A2 constitute_a_decomposition;
then
A1: A1,A2 constitute_a_decomposition;
then A1 misses A2;
hence X1 misses X2;
A1 \/ A2 = the carrier of X by A1;
then
A2: the carrier of X1 union X2 = the carrier of X by TSEP_1:def 2;
X is SubSpace of X by TSEP_1:2;
hence thesis by A2,TSEP_1:5;
end;
assume
A3: X1 misses X2;
assume the TopStruct of X = X1 union X2;
then for A1, A2 be Subset of X st
A1 = the carrier of X1 & A2 = the carrier of X2
holds A1,A2 constitute_a_decomposition by A3,TSEP_1:def 2;
hence thesis;
end;
theorem Th30:
X0,X0 do_not_constitute_a_decomposition
proof
reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
now
take A1 = A0, A2 = A0;
thus A1 = the carrier of X0 & A2 = the carrier of X0 & A1,A2
do_not_constitute_a_decomposition by Th7;
end;
hence thesis;
end;
definition
let X be non empty TopSpace, A1, A2 be non empty SubSpace of X;
redefine pred A1,A2 constitute_a_decomposition;
irreflexivity by Th30;
end;
theorem
X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition
implies the TopStruct of X1 = the TopStruct of X2
proof
reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier
of X2 as Subset of X by TSEP_1:1;
assume for A1, A0 being Subset of X st A1 = the carrier of X1 & A0 = the
carrier of X0 holds A1,A0 constitute_a_decomposition;
then
A1: A1,A0 constitute_a_decomposition;
assume for A0, A2 being Subset of X st A0 = the carrier of X0 & A2 = the
carrier of X2 holds A0,A2 constitute_a_decomposition;
then A0,A2 constitute_a_decomposition;
hence thesis by A1,Th8,TSEP_1:5;
end;
theorem Th32:
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1
constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds Y1 union Y2
= the TopStruct of X iff X1 misses X2
proof
let X1, X2, Y1, Y2 be non empty SubSpace of X;
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by
TSEP_1:1;
assume that
A1: X1,Y1 constitute_a_decomposition and
A2: X2,Y2 constitute_a_decomposition;
A3: A2,B2 constitute_a_decomposition by A2;
then
A4: A2 = B2` by Th3;
A5: A2 = B2` by A3,Th3;
A6: A1,B1 constitute_a_decomposition by A1;
then
A7: A1 = B1` by Th3;
thus Y1 union Y2 = the TopStruct of X implies X1 misses X2
proof
assume Y1 union Y2 = the TopStruct of X;
then B1 \/ B2 = the carrier of X by TSEP_1:def 2;
then (B1 \/ B2)` = {}X by XBOOLE_1:37;
then A1 /\ A2 = {} by A7,A5,XBOOLE_1:53;
then A1 misses A2;
hence thesis;
end;
assume X1 misses X2;
then A1 misses A2;
then
A8: A1 /\ A2 = {}X;
A1 = B1` by A6,Th3;
then (B1 \/ B2)` = {}X by A4,A8,XBOOLE_1:53;
then B1 \/ B2 = ({}X)`;
then
A9: the carrier of Y1 union Y2 = the carrier of X by TSEP_1:def 2;
X is SubSpace of X by TSEP_1:2;
hence thesis by A9,TSEP_1:5;
end;
theorem Th33:
X1,X2 constitute_a_decomposition implies (X1 is open iff X2 is closed)
proof
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
assume
A1: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
carrier of X2 holds A1,A2 constitute_a_decomposition;
thus X1 is open implies X2 is closed
proof
assume
A2: for A1 being Subset of X st A1 = the carrier of X1 holds A1 is open;
now
let A2 be Subset of X;
assume A2 = the carrier of X2;
then
A3: A1,A2 constitute_a_decomposition by A1;
A1 is open by A2;
hence A2 is closed by A3,Th11;
end;
hence thesis;
end;
assume
A4: for A2 being Subset of X st A2 = the carrier of X2 holds A2 is closed;
now
let A1 be Subset of X;
assume A1 = the carrier of X1;
then
A5: A1,A2 constitute_a_decomposition by A1;
A2 is closed by A4;
hence A1 is open by A5,Th11;
end;
hence thesis;
end;
theorem
X1,X2 constitute_a_decomposition implies (X1 is closed iff X2 is open)
by Th33;
theorem Th35:
X1 meets Y1 & X1,X2 constitute_a_decomposition & Y1,Y2
constitute_a_decomposition implies (X1 meet Y1),(X2 union Y2)
constitute_a_decomposition
proof
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by
TSEP_1:1;
assume
A1: X1 meets Y1;
assume for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
carrier of X2 holds A1,A2 constitute_a_decomposition;
then
A2: A1,A2 constitute_a_decomposition;
assume for B1, B2 being Subset of X st B1 = the carrier of Y1 & B2 = the
carrier of Y2 holds B1,B2 constitute_a_decomposition;
then
A3: B1,B2 constitute_a_decomposition;
now
let C, D be Subset of X;
assume C = the carrier of X1 meet Y1 & D = the carrier of X2 union Y2;
then C = A1 /\ B1 & D = A2 \/ B2 by A1,TSEP_1:def 2,def 4;
hence C,D constitute_a_decomposition by A2,A3,Th13;
end;
hence thesis;
end;
theorem
X2 meets Y2 & X1,X2 constitute_a_decomposition & Y1,Y2
constitute_a_decomposition implies (X1 union Y1),(X2 meet Y2)
constitute_a_decomposition by Th35;
begin
:: 4. A Duality Between Pairs of Weakly Separated Subspaces.
reserve X for non empty TopSpace;
theorem Th37:
for X1, X2, Y1, Y2 being SubSpace of X st X1,Y1
constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds X1,X2
are_weakly_separated implies Y1,Y2 are_weakly_separated
proof
let X1, X2, Y1, Y2 be SubSpace of X;
assume
A1: for A1, B1 being Subset of X st A1 = the carrier of X1 & B1 = the
carrier of Y1 holds A1,B1 constitute_a_decomposition;
assume
A2: for A2, B2 being Subset of X st A2 = the carrier of X2 & B2 = the
carrier of Y2 holds A2,B2 constitute_a_decomposition;
assume
A3: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
carrier of X2 holds A1,A2 are_weakly_separated;
now
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X
by TSEP_1:1;
let B1, B2 be Subset of X;
assume B1 = the carrier of Y1 & B2 = the carrier of Y2;
then
A4: A1,B1 constitute_a_decomposition & A2,B2 constitute_a_decomposition by A1
,A2;
A1,A2 are_weakly_separated by A3;
hence B1,B2 are_weakly_separated by A4,Th15;
end;
hence thesis;
end;
theorem
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1
constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds X1,X2
are_separated implies Y1,Y2 are_weakly_separated
by TSEP_1:78,Th37;
theorem Th39:
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1
constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds X1 misses
X2 & Y1,Y2 are_weakly_separated implies X1,X2 are_separated
by Th37,TSEP_1:78;
theorem
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1
constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds Y1 union Y2
= the TopStruct of X & Y1,Y2 are_weakly_separated implies X1,X2 are_separated
proof
let X1, X2, Y1, Y2 be non empty SubSpace of X;
assume
A1: X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition;
assume Y1 union Y2 = the TopStruct of X;
then
A2: X1 misses X2 by A1,Th32;
assume Y1,Y2 are_weakly_separated;
hence thesis by A1,A2,Th39;
end;
theorem
for X1, X2 being non empty SubSpace of X st X1,X2
constitute_a_decomposition holds (X1,X2 are_weakly_separated iff X1,X2
are_separated)
by Th29,TSEP_1:78;
::An Enlargement Theorem for Subspaces.
theorem
for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of
X1 & Y2 is SubSpace of X2 & Y1 union Y2 = X1 union X2 holds Y1,Y2
are_weakly_separated implies X1,X2 are_weakly_separated
proof
let X1, X2, Y1, Y2 be non empty SubSpace of X;
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
reconsider C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by
TSEP_1:1;
assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
then
A1: C1 c= A1 & C2 c= A2 by TSEP_1:4;
assume
A2: Y1 union Y2 = X1 union X2;
assume Y1,Y2 are_weakly_separated;
then
A3: C1,C2 are_weakly_separated;
now
let A1, A2 be Subset of X;
assume
A4: A1 = the carrier of X1 & A2 = the carrier of X2;
then A1 \/ A2 = the carrier of X1 union X2 by TSEP_1:def 2;
then A1 \/ A2 = C1 \/ C2 by A2,TSEP_1:def 2;
hence A1,A2 are_weakly_separated by A1,A3,A4,Th22;
end;
hence thesis;
end;
::An Extenuation Theorem for Subspaces.
theorem
for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of
X1 & Y2 is SubSpace of X2 & Y1 meets Y2 & Y1 meet Y2 = X1 meet X2 holds X1,X2
are_weakly_separated implies Y1,Y2 are_weakly_separated
proof
let X1, X2, Y1, Y2 be non empty SubSpace of X;
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
reconsider C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by
TSEP_1:1;
assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
then
A1: C1 c= A1 & C2 c= A2 by TSEP_1:4;
assume
A2: Y1 meets Y2;
assume
A3: Y1 meet Y2 = X1 meet X2;
assume X1,X2 are_weakly_separated;
then
A4: A1,A2 are_weakly_separated;
now
let C1, C2 be Subset of X;
assume
A5: C1 = the carrier of Y1 & C2 = the carrier of Y2;
then C1 meets C2 by A2;
then C1 /\ C2 <> {};
then A1 /\ A2 <> {} by A1,A5,XBOOLE_1:3,27;
then A1 meets A2;
then X1 meets X2;
then A1 /\ A2 = the carrier of X1 meet X2 by TSEP_1:def 4;
then A1 /\ A2 = C1 /\ C2 by A2,A3,A5,TSEP_1:def 4;
hence C1,C2 are_weakly_separated by A1,A4,A5,Th24;
end;
hence thesis;
end;
::Separated and Weakly Separated Subspaces in Subspaces.
reserve X0 for non empty SubSpace of X;
theorem Th44:
for X1, X2 being SubSpace of X, Y1, Y2 being SubSpace of X0 st
the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2
holds X1,X2 are_separated iff Y1,Y2 are_separated
proof
let X1, X2 be SubSpace of X, X01, X02 be SubSpace of X0;
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
reconsider B1 = the carrier of X01, B2 = the carrier of X02 as Subset of X0
by TSEP_1:1;
assume
A1: the carrier of X1 = the carrier of X01 & the carrier of X2 = the
carrier of X02;
thus X1,X2 are_separated implies X01,X02 are_separated
proof
assume X1,X2 are_separated;
then A1,A2 are_separated;
then for B1,B2 be Subset of X0 holds B1 = the carrier of X01 & B2 = the
carrier of X02 implies B1,B2 are_separated by A1,Th25;
hence thesis;
end;
thus X01,X02 are_separated implies X1,X2 are_separated
proof
assume X01,X02 are_separated;
then B1,B2 are_separated;
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,Th25;
hence thesis;
end;
end;
theorem
for X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 holds X1,
X2 are_separated implies Y1,Y2 are_separated
proof
let X1, X2 be non empty SubSpace of X;
assume
A1: X1 meets X0 & X2 meets X0;
let Y1, Y2 be SubSpace of X0;
assume
A2: Y1 = X1 meet X0 & Y2 = X2 meet X0;
assume X1,X2 are_separated;
then (X1 meet X0),(X2 meet X0) are_separated by A1,TSEP_1:70;
hence thesis by A2,Th44;
end;
theorem
for X1, X2 being SubSpace of X, Y1, Y2 being SubSpace of X0 st the
carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
X1,X2 are_weakly_separated iff Y1,Y2 are_weakly_separated
proof
let X1, X2 be SubSpace of X, X01, X02 be SubSpace of X0;
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider B1 = the carrier of X01 as Subset of X0 by TSEP_1:1;
reconsider B2 = the carrier of X02 as Subset of X0 by TSEP_1:1;
assume
A1: the carrier of X1 = the carrier of X01 & the carrier of X2 = the
carrier of X02;
thus X1,X2 are_weakly_separated implies X01,X02 are_weakly_separated
proof
assume X1,X2 are_weakly_separated;
then A1,A2 are_weakly_separated;
then for B1,B2 be Subset of X0 holds B1 = the carrier of X01 & B2 = the
carrier of X02 implies B1,B2 are_weakly_separated by A1,Th27;
hence thesis;
end;
thus X01,X02 are_weakly_separated implies X1,X2 are_weakly_separated
proof
assume X01,X02 are_weakly_separated;
then B1,B2 are_weakly_separated;
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 A1,Th27;
hence thesis;
end;
end;
theorem
for X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 holds X1,
X2 are_weakly_separated implies Y1,Y2 are_weakly_separated
proof
let X1, X2 be non empty SubSpace of X;
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
assume
A1: X1 meets X0 & X2 meets X0;
let Y1, Y2 be SubSpace of X0;
assume
A2: Y1 = X1 meet X0 & Y2 = X2 meet X0;
assume X1,X2 are_weakly_separated;
then
A3: A1,A2 are_weakly_separated;
now
let C1, C2 be Subset of X0;
assume C1 = the carrier of Y1 & C2 = the carrier of Y2;
then
C1 = (the carrier of X0) /\ A1 & C2 = (the carrier of X0) /\ A2 by A1,A2,
TSEP_1:def 4;
hence C1,C2 are_weakly_separated by A3,Th28;
end;
hence thesis;
end;