:: TSEP_2 semantic presentation

theorem Th1: :: TSEP_2:1

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

proof end;

definition

let X be TopSpace;
let A1, A2 be Subset of X;
pred A1,A2 constitute_a_decomposition means :Def1: :: TSEP_2:def 1
( A1 misses A2 & A1 \/ A2 = the carrier of X );
symmetry ;

end;

:: deftheorem Def1 defines constitute_a_decomposition TSEP_2:def 1 :

notation

let X be TopSpace;
let A1, A2 be Subset of X;
antonym A1,A2 do_not_constitute_a_decomposition for A1,A2 constitute_a_decomposition ;

end;

theorem Th2: :: TSEP_2:2

for X being non empty TopSpace
for A1, A2 being Subset of X holds
( A1,A2 constitute_a_decomposition iff ( A1 misses A2 & A1 \/ A2 = [#] X ) )

proof end;

theorem :: TSEP_2:3

canceled;

theorem Th4: :: TSEP_2:4

for X being non empty TopSpace
for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 = A2 ` & A2 = A1 ` )

proof end;

theorem Th5: :: TSEP_2:5

for X being non empty TopSpace
for A1, A2 being Subset of X st ( A1 = A2 ` or A2 = A1 ` ) holds
A1,A2 constitute_a_decomposition

proof end;

theorem Th6: :: TSEP_2:6

for X being non empty TopSpace
for A being Subset of X holds A,A ` constitute_a_decomposition

proof end;

theorem :: TSEP_2:7

for X being non empty TopSpace holds {} X, [#] X constitute_a_decomposition

proof end;

theorem Th8: :: TSEP_2:8

for X being non empty TopSpace
for A being Subset of X holds A,A do_not_constitute_a_decomposition

proof end;

definition

let X be non empty TopSpace;
let A1, A2 be Subset of X;
:: original: constitute_a_decomposition
redefine pred A1,A2 constitute_a_decomposition ;
irreflexivity by Th8;

end;

theorem Th9: :: TSEP_2:9

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

proof end;

theorem Th10: :: TSEP_2:10

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

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 Th12: :: 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 open iff A2 is closed )

proof end;

theorem :: TSEP_2:13

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

theorem Th14: :: TSEP_2:14

for X being non empty TopSpace
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:15

for X being non empty TopSpace
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 Th14;

theorem Th16: :: TSEP_2:16

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

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: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,A2 are_separated holds
C1,C2 are_weakly_separated

proof end;

theorem Th19: :: 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 & A1 misses A2 & 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, 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:21

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 )

proof end;

theorem Th22: :: TSEP_2:22

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;

theorem Th23: :: TSEP_2:23

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 Th24: :: TSEP_2:24

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;

theorem Th25: :: TSEP_2:25

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 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 = A1 & B2 = A2 holds
( A1,A2 are_separated iff 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 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_separated holds
B1,B2 are_separated

proof end;

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 = A1 & B2 = A2 holds
( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )

proof end;

theorem Th29: :: TSEP_2:29

proof end;

definition

let X be non empty TopSpace;
let X1, X2 be SubSpace of X;
pred X1,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 ;

end;

:: deftheorem Def2 defines constitute_a_decomposition TSEP_2:def 2 :

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 Th30: :: TSEP_2:30

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

canceled;

theorem Th32: :: TSEP_2:32

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 by Th32;

end;

theorem :: TSEP_2:33

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

proof end;

theorem Th34: :: TSEP_2:34

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 Th35: :: TSEP_2:35

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

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

theorem Th37: :: TSEP_2:37

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

proof end;

theorem :: TSEP_2:38

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

theorem Th39: :: TSEP_2:39

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: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 & X1,X2 are_separated holds
Y1,Y2 are_weakly_separated

proof end;

theorem Th41: :: TSEP_2:41

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

proof end;

theorem :: TSEP_2:42

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

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 )

proof end;

theorem :: TSEP_2:44

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;

theorem :: TSEP_2:45

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 Th46: :: 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_separated iff Y1,Y2 are_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_separated holds
Y1,Y2 are_separated

proof end;

theorem :: TSEP_2:48

proof end;

theorem :: TSEP_2:49

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;