:: 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;