### The Mizar article:

### On a Duality Between Weakly Separated Subspaces of Topological Spaces

**by****Zbigniew Karno**

- Received November 9, 1992
Copyright (c) 1992 Association of Mizar Users

- MML identifier: TSEP_2
- [ MML identifier index ]

environ vocabulary PRE_TOPC, BOOLE, SUBSET_1, TOPS_1, TSEP_1, CONNSP_1, TARSKI, SETFAM_1, TSEP_2; notation TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, STRUCT_0, TOPS_1, BORSUK_1, TSEP_1; constructors CONNSP_1, TOPS_1, BORSUK_1, TSEP_1, MEMBERED; clusters PRE_TOPC, STRUCT_0, MEMBERED, ZFMISC_1; requirements BOOLE, SUBSET; definitions BORSUK_1, TSEP_1, XBOOLE_0; theorems PRE_TOPC, TOPS_1, CONNSP_1, BORSUK_1, TSEP_1, TDLAT_1, TDLAT_3, SUBSET_1, XBOOLE_0, XBOOLE_1; begin :: 1. Certain Set-Decompositions of a Topological Space. reserve X for non empty TopSpace; 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 PRE_TOPC:17; then A` \ B` = [#]X \ (A \/ B`) by XBOOLE_1:41; then A` \ B` = (A \/ B`)` by PRE_TOPC:17; then A` \ B` = (A \/ B`)`; then A` \ B` = ( A`) /\ B`` by SUBSET_1:29; then A` \ B` = B /\ A`; hence thesis by SUBSET_1:32; end; ::Complemented Subsets. definition let X be TopSpace, A1, A2 be Subset of X; pred A1,A2 constitute_a_decomposition means :Def1: A1 misses A2 & A1 \/ A2 = the carrier of X; symmetry; antonym A1,A2 do_not_constitute_a_decomposition; end; reserve A, A1, A2, B1, B2 for Subset of X; theorem Th2: A1,A2 constitute_a_decomposition iff A1 misses A2 & A1 \/ A2 = [#]X proof thus A1,A2 constitute_a_decomposition implies A1 misses A2 & A1 \/ A2 = [#]X proof assume A1 misses A2 & A1 \/ A2 = the carrier of X; hence thesis by PRE_TOPC:12; end; assume A1 misses A2 & A1 \/ A2 = [#]X; then A1 misses A2 & A1 \/ A2 = the carrier of X by PRE_TOPC:12; hence thesis by Def1; end; canceled; theorem Th4: A1,A2 constitute_a_decomposition implies A1 = A2` & A2 = A1` proof assume A1,A2 constitute_a_decomposition; then A1: A1 misses A2 & A1 \/ A2 = [#]X by Th2; then A2` c= A1 & A1 c= A2` by TDLAT_1:1,2; hence A1 = A2` by XBOOLE_0:def 10; A1` c= A2 & A2 c= A1` by A1,TDLAT_1:1,2; hence thesis by XBOOLE_0:def 10; end; theorem Th5: 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 TDLAT_1:1,2; hence thesis by Th2; end; theorem Th6: A, A` constitute_a_decomposition proof thus A, A` constitute_a_decomposition proof A misses A` & A \/ A` = [#]X by PRE_TOPC:18,26; hence thesis by Th2; end; end; theorem {}X,[#]X constitute_a_decomposition proof thus {}X,[#]X constitute_a_decomposition proof [#]X = ({}X)` by PRE_TOPC:27; hence thesis by Th6; end; end; theorem Th8: 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,Th4; then A misses A by PRE_TOPC:21; then A /\ A = {} by XBOOLE_0:def 7; hence contradiction by A2; suppose A is empty; then {} = A \/ A .= the carrier of X by A1,Def1; hence contradiction; end; definition let X be non empty TopSpace, A1, A2 be Subset of X; redefine pred A1,A2 constitute_a_decomposition; irreflexivity by Th8; end; theorem Th9: 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 Th4; assume A,A2 constitute_a_decomposition; hence thesis by A1,Th4; end; theorem Th10: 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; thus (Cl A1),(Int A2) constitute_a_decomposition proof Cl A1 = (Int A1`)` by TDLAT_3:2; then Cl A1 = (Int A2)` by A1,Th4; hence thesis by Th5; end; thus (Int A1),(Cl A2) constitute_a_decomposition proof Int A1 = (Cl A1`)` by TOPS_1:def 1; then Int A1 = (Cl A2)` by A1,Th4; hence thesis by Th5; end; 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 thus A1: (Cl A),(Int A`) constitute_a_decomposition proof A, A` constitute_a_decomposition by Th6; hence thesis by Th10; end; thus (Cl A`),(Int A) constitute_a_decomposition proof A`,A constitute_a_decomposition by Th6; hence thesis by Th10; end; hence (Int A),(Cl A`) constitute_a_decomposition; thus (Int A`),(Cl A) constitute_a_decomposition by A1; end; theorem Th12: 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,A2 constitute_a_decomposition; then A1: A1 = A2` & A2 = A1` by Th4; hence A1 is open implies A2 is closed by TOPS_1:30; assume A2 is closed; hence thesis by A1,TOPS_1:29; end; theorem for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds (A1 is closed iff A2 is open) by Th12; theorem Th14: 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; assume B1,B2 constitute_a_decomposition; then A2: B1 misses B2 & B1 \/ B2 = [#]X by Th2; then A3: B1 /\ B2 = {}X & B1 \/ B2 = [#]X by XBOOLE_0:def 7; A1 misses A2 by A1,Th2; then A4: A1 /\ A2 = {} by XBOOLE_0:def 7; (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 A3,A4; then A5: (A1 /\ B1) misses (A2 \/ B2) by XBOOLE_0:def 7; (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,A2,Th2 .= ([#]X \/ B2) /\ [#]X by TOPS_1:2 .= [#]X /\ [#]X by TOPS_1:2 .= [#]X; hence thesis by A5,Th2; end; theorem A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition implies (A1 \/ B1),(A2 /\ B2) constitute_a_decomposition by Th14; begin :: 2. A Duality Between Pairs of Weakly Separated Subsets. reserve X for non empty TopSpace, A1, A2 for Subset of X; theorem Th16: 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` & A1 = C1` & C2 = A2` & A2 = C2` by Th4; 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 by TSEP_1:def 7; end; assume C1,C2 are_weakly_separated; then C1 \ C2,C2 \ C1 are_separated by TSEP_1:def 7; then C2` \ C1`,C2 \ C1 are_separated by Th1; then A2 \ A1,A1 \ A2 are_separated by A1,Th1; hence thesis by TSEP_1:def 7; 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 Th6; hence thesis by Th16; 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:51; hence thesis by A1,Th16; end; theorem Th19: 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 A1 /\ A2 = {}; then A2: A1 misses A2 by XBOOLE_0:def 7; assume C1,C2 are_weakly_separated; then A1,A2 are_weakly_separated by A1,Th16; hence thesis by A2,TSEP_1:51; 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; then A1 = C1` & A2 = C2` by Th4; then A2: A1 = C1` & A2 = C2`; assume C1 \/ C2 = the carrier of X; then C1 \/ C2 = [#]X by PRE_TOPC:12; then (C1 \/ C2)` = {}X by TOPS_1:8; then (C1 \/ C2)` = {}X; then A1 /\ A2 = {} by A2,SUBSET_1:29; then A3: A1 misses A2 by XBOOLE_0:def 7; assume C1,C2 are_weakly_separated; hence thesis by A1,A3,Th19; end; theorem A1,A2 constitute_a_decomposition implies (A1,A2 are_weakly_separated iff A1,A2 are_separated) proof assume A1,A2 constitute_a_decomposition; then A1 misses A2 by Def1; hence A1,A2 are_weakly_separated iff A1,A2 are_separated by TSEP_1:51; end; theorem Th22: 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 proof assume A1 \ A2,A2 \ A1 are_separated; hence thesis by A1; end; assume (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated; hence thesis by A1,TSEP_1:def 7; end; ::An Enlargement Theorem for Subsets. theorem Th23: 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 A1: C1 c= A1 & C2 c= A2; assume A2: C1 \/ C2 = A1 \/ A2; assume C1,C2 are_weakly_separated; then A3: (A1 \/ A2) \ C1,(A1 \/ A2) \ C2 are_separated by A2,Th22; (A1 \/ A2) \ A1 c= (A1 \/ A2) \ C1 & (A1 \/ A2) \ A2 c= (A1 \/ A2) \ C2 by A1,XBOOLE_1:34; then (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated by A3,CONNSP_1:8; hence thesis by Th22; end; theorem Th24: A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated proof A1: A1 \ (A1 /\ A2) = A1 \ A2 & A2 \ (A1 /\ A2) = A2 \ A1 by XBOOLE_1:47; thus A1,A2 are_weakly_separated implies A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated proof assume A1 \ A2,A2 \ A1 are_separated; hence thesis by A1; end; assume A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated; hence thesis by A1,TSEP_1:def 7; end; ::An Extenuation Theorem for Subsets. theorem Th25: 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 A1: C1 c= A1 & C2 c= A2; assume A2: C1 /\ C2 = A1 /\ A2; assume A1,A2 are_weakly_separated; then A3: A1 \ (C1 /\ C2),A2 \ (C1 /\ C2) are_separated by A2,Th24; C1 \ (C1 /\ C2) c= A1 \ (C1 /\ C2) & C2 \ (C1 /\ C2) c= A2 \ (C1 /\ C2) by A1,XBOOLE_1:33; then C1 \ (C1 /\ C2),C2 \ (C1 /\ C2) are_separated by A3,CONNSP_1:8; hence thesis by Th24; end; ::Separated and Weakly Separated Subsets in Subspaces. reserve X0 for non empty SubSpace of X, B1, B2 for Subset of X0; theorem Th26: B1 = A1 & B2 = A2 implies (A1,A2 are_separated iff B1,B2 are_separated) proof assume A1: B1 = A1 & B2 = A2; then A2: Cl B1 = (Cl A1) /\ [#]X0 & Cl B2 = (Cl A2) /\ [#]X0 by PRE_TOPC:47; thus A1,A2 are_separated implies B1,B2 are_separated proof assume A1,A2 are_separated; then Cl A1 misses A2 & A1 misses Cl A2 by CONNSP_1:def 1; then Cl A1 /\ A2 = {} & A1 /\ Cl A2 = {} by XBOOLE_0:def 7; then Cl B1 /\ B2 = {} /\ [#]X0 & B1 /\ Cl B2 = {} /\ [#]X0 by A1,A2,XBOOLE_1:16; then Cl B1 misses B2 & B1 misses Cl B2 by XBOOLE_0:def 7; hence B1,B2 are_separated by CONNSP_1:def 1; end; thus B1,B2 are_separated implies A1,A2 are_separated proof assume B1,B2 are_separated; then ((Cl A1) /\ [#]X0) misses A2 & A1 misses ((Cl A2) /\ [#]X0) by A1,A2,CONNSP_1:def 1; then ((Cl A1) /\ [#]X0) /\ A2 = {} & A1 /\ ((Cl A2) /\ [#]X0) = {} by XBOOLE_0:def 7; then A3: (Cl A1 /\ A2) /\ [#]X0 = {} & (A1 /\ Cl A2) /\ [#]X0 = {} by XBOOLE_1:16; Cl A1 /\ A2 c= A2 & A1 /\ Cl A2 c= A1 & A2 c= [#]X0 & A1 c= [#]X0 by A1,PRE_TOPC:14,XBOOLE_1:17; then Cl A1 /\ A2 c= [#]X0 & A1 /\ Cl A2 c= [#]X0 by XBOOLE_1:1; then Cl A1 /\ A2 = {} & A1 /\ Cl A2 = {} by A3,XBOOLE_1:28; then Cl A1 misses A2 & A1 misses Cl A2 by XBOOLE_0:def 7; hence thesis by CONNSP_1:def 1; end; end; theorem Th27: B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2 implies (A1,A2 are_separated implies B1,B2 are_separated) proof reconsider A1' = A1, A2' = A2 as Subset of X; assume B1 = (the carrier of X0) /\ A1; then A1: B1 c= A1 by XBOOLE_1:17; then B1 is Subset of X by XBOOLE_1:1; then reconsider C1 = B1 as Subset of X; assume B2 = (the carrier of X0) /\ A2; then A2: B2 c= A2 by XBOOLE_1:17; then B2 is Subset of X by XBOOLE_1:1; then reconsider C2 = B2 as Subset of X; assume A1,A2 are_separated; then A1',A2' are_separated; then C1,C2 are_separated by A1,A2,CONNSP_1:8; hence thesis by Th26; end; theorem Th28: B1 = A1 & B2 = A2 implies (A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated) proof assume A1: B1 = A1 & B2 = A2; thus A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated proof assume A1,A2 are_weakly_separated; then A1 \ A2,A2 \ A1 are_separated by TSEP_1:def 7; then B1 \ B2,B2 \ B1 are_separated by A1,Th26; hence thesis by TSEP_1:def 7; end; thus B1,B2 are_weakly_separated implies A1,A2 are_weakly_separated proof assume B1,B2 are_weakly_separated; then B1 \ B2,B2 \ B1 are_separated by TSEP_1:def 7; then A1 \ A2,A2 \ A1 are_separated by A1,Th26; hence thesis by TSEP_1:def 7; end; end; theorem Th29: 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 A1: B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2; assume A2: A1 \ A2,A2 \ A1 are_separated; B1 \ B2 = (the carrier of X0) /\ (A1 \ A2) & B2 \ B1 = (the carrier of X0) /\ (A2 \ A1) by A1,XBOOLE_1:50; then B1 \ B2,B2 \ B1 are_separated by A2,Th27; hence thesis by TSEP_1:def 7; 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 :Def2: 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; antonym X1,X2 do_not_constitute_a_decomposition; end; reserve X0, X1, X2, Y1, Y2 for non empty SubSpace of X; theorem Th30: 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 by Def1; hence X1 misses X2 by TSEP_1:def 3; A1 \/ A2 = the carrier of X by A1,Def1; then the carrier of X1 union X2 = the carrier of X & X is SubSpace of X by TSEP_1:2,def 2; hence thesis by TSEP_1:5; end; assume A2: X1 misses X2; assume A3: the TopStruct of X = X1 union X2; now let A1, A2 be Subset of X; assume A4: A1 = the carrier of X1 & A2 = the carrier of X2; then A5:A1 misses A2 by A2,TSEP_1:def 3; A1 \/ A2 = the carrier of X by A3,A4,TSEP_1:def 2; hence A1,A2 constitute_a_decomposition by A5,Def1; end; hence X1,X2 constitute_a_decomposition by Def2; end; canceled; theorem Th32: 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 Th8; end; hence thesis by Def2; 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 Th32; end; theorem X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition implies the TopStruct of X1 = the TopStruct of X2 proof assume A1: for A1, A0 being Subset of X st A1 = the carrier of X1 & A0 = the carrier of X0 holds A1,A0 constitute_a_decomposition; assume A2: for A0, A2 being Subset of X st A0 = the carrier of X0 & A2 = the carrier of X2 holds A0,A2 constitute_a_decomposition; reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1; A1,A0 constitute_a_decomposition & A0,A2 constitute_a_decomposition by A1,A2; then A1 = A2 by Th9; hence thesis by TSEP_1:5; end; theorem Th34: 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 X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition; then A1,B1 constitute_a_decomposition & A2,B2 constitute_a_decomposition by Def2; then B1 = A1` & A1 = B1` & B2 = A2` & A2 = B2` by Th4; then A1: B1 = A1` & A1 = B1` & B2 = A2` & A2 = B2`; 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 PRE_TOPC:12; then (B1 \/ B2)` = {}X by TOPS_1:8; then (B1 \/ B2)` = {}X; then A1 /\ A2 = {} by A1,SUBSET_1:29; then A1 misses A2 by XBOOLE_0:def 7; hence thesis by TSEP_1:def 3; end; assume X1 misses X2; then A1 misses A2 by TSEP_1:def 3; then A1 /\ A2 = {}X by XBOOLE_0:def 7; then (B1 \/ B2)` = {}X by A1,SUBSET_1:29; then B1 \/ B2 = ({}X)`; then B1 \/ B2 = [#]X by PRE_TOPC:27; then B1 \/ B2 = the carrier of X by PRE_TOPC:12; then the carrier of Y1 union Y2 = the carrier of X & X is SubSpace of X by TSEP_1:2,def 2; hence thesis by TSEP_1:5; end; theorem Th35: X1,X2 constitute_a_decomposition implies (X1 is open iff X2 is closed) proof the carrier of X1 is Subset of X & the carrier of X2 is Subset of X by TSEP_1:1; then reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X; 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 A1,A2 constitute_a_decomposition & A1 is open by A1,A2; hence A2 is closed by Th12; end; hence thesis by BORSUK_1:def 14; end; assume A3: 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 A1,A2 constitute_a_decomposition & A2 is closed by A1,A3; hence A1 is open by Th12; end; hence thesis by TSEP_1:def 1; end; theorem X1,X2 constitute_a_decomposition implies (X1 is closed iff X2 is open) by Th35; theorem Th37: 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 5; hence C,D constitute_a_decomposition by A2,A3,Th14; end; hence thesis by Def2; 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 Th37; begin :: 4. A Duality Between Pairs of Weakly Separated Subspaces. reserve X for non empty TopSpace; theorem Th39: 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 let B1, B2 be Subset of X; reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1; assume B1 = the carrier of Y1 & B2 = the carrier of Y2; then A1,B1 constitute_a_decomposition & A2,B2 constitute_a_decomposition & A1,A2 are_weakly_separated by A1,A2,A3; hence B1,B2 are_weakly_separated by Th16; end; hence thesis by TSEP_1:def 9; 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 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 X1,X2 are_separated; then X1,X2 are_weakly_separated by TSEP_1:85; hence thesis by A1,Th39; end; theorem Th41: 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 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 A2: X1 misses X2; assume Y1,Y2 are_weakly_separated; then X1,X2 are_weakly_separated by A1,Th39; hence thesis by A2,TSEP_1:85; 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 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,Th34; assume Y1,Y2 are_weakly_separated; hence thesis by A1,A2,Th41; 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) proof let X1, X2 be non empty SubSpace of X; assume X1,X2 constitute_a_decomposition; then X1 misses X2 by Th30; hence X1,X2 are_weakly_separated iff X1,X2 are_separated by TSEP_1:85; end; ::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 by TSEP_1:def 9; 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,Th23; end; hence thesis by TSEP_1:def 9; 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; then A2: C1 /\ C2 c= A1 /\ A2 by XBOOLE_1:27; assume A3: Y1 meets Y2; assume A4: Y1 meet Y2 = X1 meet X2; assume X1,X2 are_weakly_separated; then A5: A1,A2 are_weakly_separated by TSEP_1:def 9; now let C1, C2 be Subset of X; assume A6: C1 = the carrier of Y1 & C2 = the carrier of Y2; then C1 meets C2 by A3,TSEP_1:def 3; then C1 /\ C2 <> {} by XBOOLE_0:def 7; then A1 /\ A2 <> {} by A2,A6,XBOOLE_1:3; then A1 meets A2 by XBOOLE_0:def 7; then X1 meets X2 by TSEP_1:def 3; then A1 /\ A2 = the carrier of X1 meet X2 by TSEP_1:def 5; then A1 /\ A2 = C1 /\ C2 by A3,A4,A6,TSEP_1:def 5; hence C1,C2 are_weakly_separated by A1,A5,A6,Th25; end; hence thesis by TSEP_1:def 9; end; ::Separated and Weakly Separated Subspaces in Subspaces. reserve X0 for non empty SubSpace of X; theorem Th46: 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; assume A1: the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02; 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; thus X1,X2 are_separated implies X01,X02 are_separated proof assume X1,X2 are_separated; then A1,A2 are_separated by TSEP_1:def 8; 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,Th26; hence thesis by TSEP_1:def 8; end; thus X01,X02 are_separated implies X1,X2 are_separated proof assume X01,X02 are_separated; then B1,B2 are_separated by TSEP_1:def 8; 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,Th26; hence thesis by TSEP_1:def 8; 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:76; hence thesis by A2,Th46; 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; assume A1: the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02; 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; 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 by TSEP_1:def 9; 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,Th28; hence thesis by TSEP_1:def 9; 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 by TSEP_1:def 9; 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,Th28; hence thesis by TSEP_1:def 9; 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 by TSEP_1:def 9; 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 5; hence C1,C2 are_weakly_separated by A3,Th29; end; hence thesis by TSEP_1:def 9; end;

Back to top