:: On a Duality Between Weakly Separated Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received November 9, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

theorem Th1: :: TSEP_2:1
for X being non empty 1-sorted
for A, B being Subset of X holds (A `) \ (B `) = B \ A
proofend;

:: Complemented Subsets.
definition
let X be 1-sorted ;
let A1, A2 be Subset of X;
predA1,A2 constitute_a_decomposition  means :Def1: :: TSEP_2:def 1
( A1 misses A2 & A1 \/ A2 = the carrier of X );
symmetry
 for A1, A2 being Subset of X st A1 misses A2 & A1 \/ A2 = the carrier of X holds
( A2 misses A1 & A2 \/ A1 = the carrier of X ) ;
end;

:: deftheorem Def1 defines constitute_a_decomposition TSEP_2:def_1_:_
 for X being 1-sorted
for A1, A2 being Subset of X holds
( A1,A2 constitute_a_decomposition iff ( A1 misses A2 & A1 \/ A2 = the carrier of X ) );

notation
let X be 1-sorted ;
let A1, A2 be Subset of X;
antonym A1,A2 do_not_constitute_a_decomposition for A1,A2 constitute_a_decomposition ;
end;

theorem :: TSEP_2:2
for X being non empty 1-sorted
for A1, A2 being Subset of X holds
( A1,A2 constitute_a_decomposition iff ( A1 misses A2 & A1 \/ A2 = [#] X ) ) by Def1;

theorem Th3: :: TSEP_2:3
for X being non empty 1-sorted
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 = A2 ` & A2 = A1 ` )
proofend;

theorem Th4: :: TSEP_2:4
for X being non empty 1-sorted
for A1, A2 being Subset of X st ( A1 = A2 ` or A2 = A1 ` ) holds
A1,A2 constitute_a_decomposition
proofend;

theorem Th5: :: TSEP_2:5
for X being non empty 1-sorted
for A being Subset of X holds A,A ` constitute_a_decomposition
proofend;

theorem :: TSEP_2:6
for X being non empty 1-sorted holds {} X, [#] X constitute_a_decomposition
proofend;

theorem Th7: :: TSEP_2:7
for X being non empty 1-sorted
for A being Subset of X holds A,A do_not_constitute_a_decomposition
proofend;

definition
let X be non empty 1-sorted ;
let A1, A2 be Subset of X;
:: original:constitute_a_decomposition
redefine predA1,A2 constitute_a_decomposition ;
irreflexivity
 for A1 being Subset of X holds (X,b1,b1) by Th7;
end;

theorem Th8: :: TSEP_2:8
for X being non empty 1-sorted
for A1, A, A2 being Subset of X st A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition holds
A1 = A2
proofend;

theorem Th9: :: TSEP_2:9
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition )
proofend;

theorem :: TSEP_2:10
for X being non empty TopSpace
for A being Subset of X holds
( 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 )
proofend;

theorem Th11: :: TSEP_2:11
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 is open iff A2 is closed )
proofend;

theorem :: TSEP_2:12
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 is closed iff A2 is open ) by Th11;

theorem Th13: :: TSEP_2:13
for X being non empty 1-sorted
for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds
A1 /\ B1,A2 \/ B2 constitute_a_decomposition
proofend;

theorem :: TSEP_2:14
for X being non empty 1-sorted
for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds
A1 \/ B1,A2 /\ B2 constitute_a_decomposition by Th13;

begin

theorem Th15: :: TSEP_2:15
for X being non empty TopSpace
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 )
proofend;

theorem :: TSEP_2:16
for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated )
proofend;

theorem :: TSEP_2:17
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1,A2 are_separated holds
C1,C2 are_weakly_separated
proofend;

theorem Th18: :: TSEP_2:18
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1 misses A2 & C1,C2 are_weakly_separated holds
A1,A2 are_separated
proofend;

theorem :: TSEP_2:19
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & C1 \/ C2 = the carrier of X & C1,C2 are_weakly_separated holds
A1,A2 are_separated
proofend;

theorem :: TSEP_2:20
for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1,A2 are_weakly_separated iff A1,A2 are_separated )
proofend;

theorem Th21: :: TSEP_2:21
for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )
proofend;

::An Enlargement Theorem for Subsets.
theorem Th22: :: TSEP_2:22
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 \/ C2 = A1 \/ A2 & C1,C2 are_weakly_separated holds
A1,A2 are_weakly_separated
proofend;

theorem Th23: :: TSEP_2:23
for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated )
proofend;

::An Extenuation Theorem for Subsets.
theorem Th24: :: TSEP_2:24
for X being non empty TopSpace
for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 /\ C2 = A1 /\ A2 & A1,A2 are_weakly_separated holds
C1,C2 are_weakly_separated
proofend;

theorem Th25: :: TSEP_2:25
for X being non empty TopSpace
for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
proofend;

theorem Th26: :: TSEP_2:26
for X being non empty TopSpace
for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_separated holds
B1,B2 are_separated
proofend;

theorem Th27: :: TSEP_2:27
for X being non empty TopSpace
for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
proofend;

theorem Th28: :: TSEP_2:28
for X being non empty TopSpace
for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds
B1,B2 are_weakly_separated
proofend;

begin

:: 3. Certain Subspace-Decompositions of a Topological Space.
definition
let X be non empty TopSpace;
let X1, X2 be SubSpace of X;
predX1,X2 constitute_a_decomposition  means :Def2: :: 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
 for X1, X2 being SubSpace of X st ( for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition ) holds
for A1, A2 being Subset of X st A1 = the carrier of X2 & A2 = the carrier of X1 holds
A1,A2 constitute_a_decomposition ;
end;

:: deftheorem Def2 defines constitute_a_decomposition TSEP_2:def_2_:_
 for X being non empty TopSpace
for X1, X2 being SubSpace of X holds
( X1,X2 constitute_a_decomposition iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition );

notation
let X be non empty TopSpace;
let X1, X2 be SubSpace of X;
antonym X1,X2 do_not_constitute_a_decomposition for X1,X2 constitute_a_decomposition ;
end;

theorem Th29: :: TSEP_2:29
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 constitute_a_decomposition iff ( X1 misses X2 & TopStruct(# the carrier of X, the topology of X #) = X1 union X2 ) )
proofend;

theorem Th30: :: TSEP_2:30
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds X0,X0 do_not_constitute_a_decomposition
proofend;

definition
let X be non empty TopSpace;
let A1, A2 be non empty SubSpace of X;
:: original:constitute_a_decomposition
redefine predA1,A2 constitute_a_decomposition ;
irreflexivity
 for A1 being non empty SubSpace of X holds (X,b1,b1) by Th30;
end;

theorem :: TSEP_2:31
for X being non empty TopSpace
for X1, X0, X2 being non empty SubSpace of X st X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proofend;

theorem Th32: :: TSEP_2:32
for X being non empty TopSpace
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 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 )
proofend;

theorem Th33: :: TSEP_2:33
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is open iff X2 is closed )
proofend;

theorem :: TSEP_2:34
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is closed iff X2 is open ) by Th33;

theorem Th35: :: TSEP_2:35
for X being non empty TopSpace
for X1, Y1, X2, Y2 being non empty SubSpace of X st X1 meets Y1 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition holds
X1 meet Y1,X2 union Y2 constitute_a_decomposition
proofend;

theorem :: TSEP_2:36
for X being non empty TopSpace
for X2, Y2, X1, Y1 being non empty SubSpace of X st X2 meets Y2 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition holds
X1 union Y1,X2 meet Y2 constitute_a_decomposition by Th35;

begin

theorem Th37: :: TSEP_2:37
for X being non empty TopSpace
for X1, X2, Y1, Y2 being SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
proofend;

theorem :: TSEP_2:38
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_separated holds
Y1,Y2 are_weakly_separated
proofend;

theorem Th39: :: TSEP_2:39
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1 misses X2 & Y1,Y2 are_weakly_separated holds
X1,X2 are_separated
proofend;

theorem :: TSEP_2:40
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) & Y1,Y2 are_weakly_separated holds
X1,X2 are_separated
proofend;

theorem :: TSEP_2:41
for X being non empty TopSpace
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 )
proofend;

::An Enlargement Theorem for Subspaces.
theorem :: TSEP_2:42
for X being non empty TopSpace
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 & Y1,Y2 are_weakly_separated holds
X1,X2 are_weakly_separated
proofend;

::An Extenuation Theorem for Subspaces.
theorem :: TSEP_2:43
for X being non empty TopSpace
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 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
proofend;

theorem Th44: :: TSEP_2:44
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for X1, X2 being SubSpace of X
for 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 )
proofend;

theorem :: TSEP_2:45
for X being non empty TopSpace
for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_separated holds
Y1,Y2 are_separated
proofend;

theorem :: TSEP_2:46
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for X1, X2 being SubSpace of X
for 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 )
proofend;

theorem :: TSEP_2:47
for X being non empty TopSpace
for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
proofend;