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

theorem Th1: :: TSEP_2:1

for X being non empty 1-sorted
for A, B being Subset of X holds (A `) \ (B `) = B \ A

proof end;

:: Complemented Subsets.

definition

let X be 1-sorted ;
let 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
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 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 ) ) ;

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 ` )

proof end;

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

proof end;

theorem Th5: :: TSEP_2:5

for X being non empty 1-sorted
for A being Subset of X holds A,A ` constitute_a_decomposition

proof end;

theorem :: TSEP_2:6

for X being non empty 1-sorted holds {} X, [#] X constitute_a_decomposition

proof end;

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

proof end;

definition

let X be non empty 1-sorted ;
let A1, A2 be Subset of X;
:: original: constitute_a_decomposition
redefine pred A1,A2 constitute_a_decomposition ;
irreflexivity
for A1 being Subset of X holds (X,b₁,b₁) by Th7;

end;

theorem Th8: :: TSEP_2:8

for X being non empty 1-sorted
for A, A1, A2 being Subset of X st A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition holds
A1 = A2

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

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;

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 )

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ) by TSEP_1:46;

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 )

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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 ) by Th25;

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

proof end;

:: 3. Certain Subspace-Decompositions of a Topological Space.

definition

let X be non empty TopSpace;
let 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
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 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 ) )

proof end;

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

proof end;

definition

let X be non empty TopSpace;
let A1, A2 be non empty SubSpace of X;
:: original: constitute_a_decomposition
redefine pred A1,A2 constitute_a_decomposition ;
irreflexivity
for A1 being non empty SubSpace of X holds (X,b₁,b₁) by Th30;

end;

theorem :: TSEP_2:31

for X being non empty TopSpace
for X0, X1, 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 #)

proof end;

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 )

proof end;

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 )

proof end;

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, X2, Y1, 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

proof end;

theorem :: TSEP_2:36

for X being non empty TopSpace
for X1, X2, Y1, Y2 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;

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

proof end;

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 by TSEP_1:78, Th37;

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 by Th37, TSEP_1:78;

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

proof end;

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 ) by Th29, TSEP_1:78;

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

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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 )

proof end;

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

proof end;