:: On a Duality Between Weakly Separated Subspaces of Topological Spaces :: by Zbigniew Karno :: :: Received November 9, 1992 :: Copyright (c) 1992-2021 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; begin :: 1. Certain Set-Decompositions of a Topological Space. reserve X for non empty 1-sorted; theorem :: TSEP_2:1 for A, B being Subset of X holds ( A`) \ B` = B \ A; :: Complemented Subsets. definition let X be 1-sorted, A1, A2 be Subset of X; pred A1,A2 constitute_a_decomposition means :: TSEP_2:def 1 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 :: TSEP_2:2 A1,A2 constitute_a_decomposition iff A1 misses A2 & A1 \/ A2 = [#]X; theorem :: TSEP_2:3 A1,A2 constitute_a_decomposition implies A1 = A2` & A2 = A1`; theorem :: TSEP_2:4 A1 = A2` or A2 = A1` implies A1,A2 constitute_a_decomposition; theorem :: TSEP_2:5 A, A` constitute_a_decomposition; theorem :: TSEP_2:6 {}X,[#]X constitute_a_decomposition; theorem :: TSEP_2:7 A,A do_not_constitute_a_decomposition; definition let X be non empty 1-sorted, A1, A2 be Subset of X; redefine pred A1,A2 constitute_a_decomposition; irreflexivity; end; theorem :: TSEP_2:8 A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition implies A1 = A2; reserve X for non empty TopSpace; reserve A, A1, A2, B1, B2 for Subset of X; theorem :: TSEP_2:9 A1,A2 constitute_a_decomposition implies (Cl A1),(Int A2) constitute_a_decomposition & (Int A1),(Cl A2) constitute_a_decomposition; theorem :: TSEP_2:10 (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; theorem :: TSEP_2:11 for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds (A1 is open iff A2 is closed); theorem :: TSEP_2:12 for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds (A1 is closed iff A2 is open); reserve X for non empty 1-sorted; reserve A, A1, A2, B1, B2 for Subset of X; theorem :: TSEP_2:13 A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition implies (A1 /\ B1),(A2 \/ B2) constitute_a_decomposition; theorem :: TSEP_2:14 A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition implies (A1 \/ B1),(A2 /\ B2) constitute_a_decomposition; begin :: 2. A Duality Between Pairs of Weakly Separated Subsets. reserve X for non empty TopSpace, A1, A2 for Subset of X; theorem :: TSEP_2:15 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; theorem :: TSEP_2:16 A1,A2 are_weakly_separated iff A1`, A2` are_weakly_separated; theorem :: TSEP_2:17 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; theorem :: TSEP_2:18 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; theorem :: TSEP_2:19 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; theorem :: TSEP_2:20 A1,A2 constitute_a_decomposition implies (A1,A2 are_weakly_separated iff A1,A2 are_separated); theorem :: TSEP_2:21 A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated; ::An Enlargement Theorem for Subsets. theorem :: TSEP_2:22 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; theorem :: TSEP_2:23 A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated; ::An Extenuation Theorem for Subsets. theorem :: TSEP_2:24 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; ::Separated and Weakly Separated Subsets in Subspaces. reserve X0 for non empty SubSpace of X, B1, B2 for Subset of X0; theorem :: TSEP_2:25 B1 = A1 & B2 = A2 implies (A1,A2 are_separated iff B1,B2 are_separated); theorem :: TSEP_2:26 B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2 implies (A1,A2 are_separated implies B1,B2 are_separated); theorem :: TSEP_2:27 B1 = A1 & B2 = A2 implies (A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated); theorem :: TSEP_2:28 B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2 implies (A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated); 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 :: TSEP_2:def 2 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 :: TSEP_2:29 X1,X2 constitute_a_decomposition iff X1 misses X2 & the TopStruct of X = X1 union X2; theorem :: TSEP_2:30 X0,X0 do_not_constitute_a_decomposition; definition let X be non empty TopSpace, A1, A2 be non empty SubSpace of X; redefine pred A1,A2 constitute_a_decomposition; irreflexivity; end; theorem :: TSEP_2:31 X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition implies the TopStruct of X1 = the TopStruct of X2; theorem :: TSEP_2:32 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; theorem :: TSEP_2:33 X1,X2 constitute_a_decomposition implies (X1 is open iff X2 is closed); theorem :: TSEP_2:34 X1,X2 constitute_a_decomposition implies (X1 is closed iff X2 is open); theorem :: TSEP_2:35 X1 meets Y1 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition implies (X1 meet Y1),(X2 union Y2) constitute_a_decomposition; theorem :: TSEP_2:36 X2 meets Y2 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition implies (X1 union Y1),(X2 meet Y2) constitute_a_decomposition; begin :: 4. A Duality Between Pairs of Weakly Separated Subspaces. reserve X for non empty TopSpace; theorem :: TSEP_2:37 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; theorem :: TSEP_2:38 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; theorem :: TSEP_2:39 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; theorem :: TSEP_2:40 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 ; theorem :: TSEP_2:41 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); ::An Enlargement Theorem for Subspaces. theorem :: TSEP_2:42 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; ::An Extenuation Theorem for Subspaces. theorem :: TSEP_2:43 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; ::Separated and Weakly Separated Subspaces in Subspaces. reserve X0 for non empty SubSpace of X; theorem :: TSEP_2:44 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; theorem :: TSEP_2:45 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; theorem :: TSEP_2:46 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; theorem :: TSEP_2:47 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;