Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### 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