Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

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

**by****Zbigniew Karno**- Received November 9, 1992
- MML identifier: TSEP_2

- [ Mizar article, 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; begin :: 1. Certain Set-Decompositions of a Topological Space. reserve X for non empty TopSpace; theorem :: TSEP_2:1 for A, B being Subset of X holds ( A`) \ B` = B \ A; ::Complemented Subsets. definition let X be TopSpace, 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; antonym A1,A2 do_not_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; canceled; theorem :: TSEP_2:4 A1,A2 constitute_a_decomposition implies A1 = A2` & A2 = A1`; theorem :: TSEP_2:5 A1 = A2` or A2 = A1` implies A1,A2 constitute_a_decomposition; theorem :: TSEP_2:6 A, A` constitute_a_decomposition; theorem :: TSEP_2:7 {}X,[#]X constitute_a_decomposition; theorem :: TSEP_2:8 A,A do_not_constitute_a_decomposition; definition let X be non empty TopSpace, A1, A2 be Subset of X; redefine pred A1,A2 constitute_a_decomposition; irreflexivity; end; theorem :: TSEP_2:9 A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition implies A1 = A2; theorem :: TSEP_2:10 A1,A2 constitute_a_decomposition implies (Cl A1),(Int A2) constitute_a_decomposition & (Int A1),(Cl A2) constitute_a_decomposition; theorem :: TSEP_2:11 (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:12 for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds (A1 is open iff A2 is closed); theorem :: TSEP_2:13 for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds (A1 is closed iff A2 is open); theorem :: TSEP_2:14 A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition implies (A1 /\ B1),(A2 \/ B2) constitute_a_decomposition; theorem :: TSEP_2:15 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:16 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:17 A1,A2 are_weakly_separated iff A1`, A2` 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,A2 are_separated implies C1,C2 are_weakly_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 A1 misses A2 & C1,C2 are_weakly_separated implies A1,A2 are_separated; theorem :: TSEP_2:20 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:21 A1,A2 constitute_a_decomposition implies (A1,A2 are_weakly_separated iff A1,A2 are_separated); theorem :: TSEP_2:22 A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated; ::An Enlargement Theorem for Subsets. theorem :: TSEP_2:23 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:24 A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated; ::An Extenuation Theorem for Subsets. theorem :: TSEP_2:25 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:26 B1 = A1 & B2 = A2 implies (A1,A2 are_separated iff B1,B2 are_separated); theorem :: TSEP_2:27 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:28 B1 = A1 & B2 = A2 implies (A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated); theorem :: TSEP_2:29 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; antonym X1,X2 do_not_constitute_a_decomposition; end; reserve X0, X1, X2, Y1, Y2 for non empty SubSpace of X; theorem :: TSEP_2:30 X1,X2 constitute_a_decomposition iff X1 misses X2 & the TopStruct of X = X1 union X2; canceled; theorem :: TSEP_2:32 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:33 X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition implies the TopStruct of X1 = the TopStruct of X2; theorem :: TSEP_2:34 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:35 X1,X2 constitute_a_decomposition implies (X1 is open iff X2 is closed); theorem :: TSEP_2:36 X1,X2 constitute_a_decomposition implies (X1 is closed iff X2 is open); theorem :: TSEP_2:37 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:38 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:39 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:40 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:41 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:42 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:43 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:44 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:45 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: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_separated iff Y1,Y2 are_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_separated implies Y1,Y2 are_separated; theorem :: TSEP_2:48 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:49 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;

Back to top