:: TSEP_2 semantic presentation

theorem Th1: :: TSEP_2:1

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ holds (b₂ ` ) \ (b₃ ` ) = b₃ \ b₂

proof end;

definition

let c₁ be TopSpace;
let c₂, c₃ be Subset of c₁;
pred c₂,c₃ constitute_a_decomposition means :Def1: :: TSEP_2:def 1
( a₂ misses a₃ & a₂ \/ a₃ = the carrier of a₁ );
symmetry ;

end;

:: deftheorem Def1 defines constitute_a_decomposition TSEP_2:def 1 :

notation

let c₁ be TopSpace;
let c₂, c₃ be Subset of c₁;
antonym c₂,c₃ do_not_constitute_a_decomposition for c₂,c₃ constitute_a_decomposition ;

end;

theorem Th2: :: TSEP_2:2

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ constitute_a_decomposition iff ( b₂ misses b₃ & b₂ \/ b₃ = [#] b₁ ) )

proof end;

theorem Th3: :: TSEP_2:3

canceled;

theorem Th4: :: TSEP_2:4

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ = b₃ ` & b₃ = b₂ ` )

proof end;

theorem Th5: :: TSEP_2:5

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st ( b₂ = b₃ ` or b₃ = b₂ ` ) holds
b₂,b₃ constitute_a_decomposition

proof end;

theorem Th6: :: TSEP_2:6

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds b₂,b₂ ` constitute_a_decomposition

proof end;

theorem Th7: :: TSEP_2:7

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

proof end;

theorem Th8: :: TSEP_2:8

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds b₂,b₂ do_not_constitute_a_decomposition

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be Subset of c₁;
redefine pred constitute_a_decomposition as c₂,c₃ constitute_a_decomposition ;
irreflexivity by Th8;

end;

theorem Th9: :: TSEP_2:9

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂,b₃ constitute_a_decomposition & b₃,b₄ constitute_a_decomposition holds
b₂ = b₄

proof end;

theorem Th10: :: TSEP_2:10

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( Cl b₂, Int b₃ constitute_a_decomposition & Int b₂, Cl b₃ constitute_a_decomposition )

proof end;

theorem Th11: :: TSEP_2:11

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( Cl b₂, Int (b₂ ` ) constitute_a_decomposition & Cl (b₂ ` ), Int b₂ constitute_a_decomposition & Int b₂, Cl (b₂ ` ) constitute_a_decomposition & Int (b₂ ` ), Cl b₂ constitute_a_decomposition )

proof end;

theorem Th12: :: TSEP_2:12

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is open iff b₃ is closed )

proof end;

theorem Th13: :: TSEP_2:13

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is closed iff b₃ is open ) by Th12;

theorem Th14: :: TSEP_2:14

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂,b₃ constitute_a_decomposition & b₄,b₅ constitute_a_decomposition holds
b₂ /\ b₄,b₃ \/ b₅ constitute_a_decomposition

proof end;

theorem Th15: :: TSEP_2:15

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂,b₃ constitute_a_decomposition & b₄,b₅ constitute_a_decomposition holds
b₂ \/ b₄,b₃ /\ b₅ constitute_a_decomposition by Th14;

theorem Th16: :: TSEP_2:16

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition holds
( b₂,b₃ are_weakly_separated iff b₄,b₅ are_weakly_separated )

proof end;

theorem Th17: :: TSEP_2:17

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_weakly_separated iff b₂ ` ,b₃ ` are_weakly_separated )

proof end;

theorem Th18: :: TSEP_2:18

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition & b₂,b₃ are_separated holds
b₄,b₅ are_weakly_separated

proof end;

theorem Th19: :: TSEP_2:19

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition & b₂ misses b₃ & b₄,b₅ are_weakly_separated holds
b₂,b₃ are_separated

proof end;

theorem Th20: :: TSEP_2:20

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition & b₄ \/ b₅ = the carrier of b₁ & b₄,b₅ are_weakly_separated holds
b₂,b₃ are_separated

proof end;

theorem Th21: :: TSEP_2:21

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂,b₃ are_weakly_separated iff b₂,b₃ are_separated )

proof end;

theorem Th22: :: TSEP_2:22

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_weakly_separated iff (b₂ \/ b₃) \ b₂,(b₂ \/ b₃) \ b₃ are_separated )

proof end;

theorem Th23: :: TSEP_2:23

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₄ c= b₂ & b₅ c= b₃ & b₄ \/ b₅ = b₂ \/ b₃ & b₄,b₅ are_weakly_separated holds
b₂,b₃ are_weakly_separated

proof end;

theorem Th24: :: TSEP_2:24

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂,b₃ are_weakly_separated iff b₂ \ (b₂ /\ b₃),b₃ \ (b₂ /\ b₃) are_separated )

proof end;

theorem Th25: :: TSEP_2:25

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₄ c= b₂ & b₅ c= b₃ & b₄ /\ b₅ = b₂ /\ b₃ & b₂,b₃ are_weakly_separated holds
b₄,b₅ are_weakly_separated

proof end;

theorem Th26: :: TSEP_2:26

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being non empty SubSpace of b₁
for b₅, b₆ being Subset of b₄ st b₅ = b₂ & b₆ = b₃ holds
( b₂,b₃ are_separated iff b₅,b₆ are_separated )

proof end;

theorem Th27: :: TSEP_2:27

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being non empty SubSpace of b₁
for b₅, b₆ being Subset of b₄ st b₅ = the carrier of b₄ /\ b₂ & b₆ = the carrier of b₄ /\ b₃ & b₂,b₃ are_separated holds
b₅,b₆ are_separated

proof end;

theorem Th28: :: TSEP_2:28

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being non empty SubSpace of b₁
for b₅, b₆ being Subset of b₄ st b₅ = b₂ & b₆ = b₃ holds
( b₂,b₃ are_weakly_separated iff b₅,b₆ are_weakly_separated )

proof end;

theorem Th29: :: TSEP_2:29

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be SubSpace of c₁;
pred c₂,c₃ constitute_a_decomposition means :Def2: :: TSEP_2:def 2
for b₁, b₂ being Subset of a₁ st b₁ = the carrier of a₂ & b₂ = the carrier of a₃ holds
b₁,b₂ constitute_a_decomposition ;
symmetry ;

end;

:: deftheorem Def2 defines constitute_a_decomposition TSEP_2:def 2 :

notation

let c₁ be non empty TopSpace;
let c₂, c₃ be SubSpace of c₁;
antonym c₂,c₃ do_not_constitute_a_decomposition for c₂,c₃ constitute_a_decomposition ;

end;

theorem Th30: :: TSEP_2:30

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ holds
( b₂,b₃ constitute_a_decomposition iff ( b₂ misses b₃ & TopStruct(# the carrier of b₁,the topology of b₁ #) = b₂ union b₃ ) )

proof end;

theorem Th31: :: TSEP_2:31

canceled;

theorem Th32: :: TSEP_2:32

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁ holds b₂,b₂ do_not_constitute_a_decomposition

proof end;

definition

let c₁ be non empty TopSpace;
let c₂, c₃ be non empty SubSpace of c₁;
redefine pred constitute_a_decomposition as c₂,c₃ constitute_a_decomposition ;
irreflexivity by Th32;

end;

theorem Th33: :: TSEP_2:33

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ st b₂,b₃ constitute_a_decomposition & b₃,b₄ constitute_a_decomposition holds
TopStruct(# the carrier of b₂,the topology of b₂ #) = TopStruct(# the carrier of b₄,the topology of b₄ #)

proof end;

theorem Th34: :: TSEP_2:34

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being non empty SubSpace of b₁ st b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition holds
( b₄ union b₅ = TopStruct(# the carrier of b₁,the topology of b₁ #) iff b₂ misses b₃ )

proof end;

theorem Th35: :: TSEP_2:35

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is open iff b₃ is closed )

proof end;

theorem Th36: :: TSEP_2:36

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂ is closed iff b₃ is open ) by Th35;

theorem Th37: :: TSEP_2:37

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being non empty SubSpace of b₁ st b₂ meets b₃ & b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition holds
b₂ meet b₃,b₄ union b₅ constitute_a_decomposition

proof end;

theorem Th38: :: TSEP_2:38

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being non empty SubSpace of b₁ st b₂ meets b₃ & b₄,b₂ constitute_a_decomposition & b₅,b₃ constitute_a_decomposition holds
b₄ union b₅,b₂ meet b₃ constitute_a_decomposition by Th37;

theorem Th39: :: TSEP_2:39

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being SubSpace of b₁ st b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition & b₂,b₃ are_weakly_separated holds
b₄,b₅ are_weakly_separated

proof end;

theorem Th40: :: TSEP_2:40

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being non empty SubSpace of b₁ st b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition & b₂,b₃ are_separated holds
b₄,b₅ are_weakly_separated

proof end;

theorem Th41: :: TSEP_2:41

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being non empty SubSpace of b₁ st b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition & b₂ misses b₃ & b₄,b₅ are_weakly_separated holds
b₂,b₃ are_separated

proof end;

theorem Th42: :: TSEP_2:42

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being non empty SubSpace of b₁ st b₂,b₄ constitute_a_decomposition & b₃,b₅ constitute_a_decomposition & b₄ union b₅ = TopStruct(# the carrier of b₁,the topology of b₁ #) & b₄,b₅ are_weakly_separated holds
b₂,b₃ are_separated

proof end;

theorem Th43: :: TSEP_2:43

for b₁ being non empty TopSpace
for b₂, b₃ being non empty SubSpace of b₁ st b₂,b₃ constitute_a_decomposition holds
( b₂,b₃ are_weakly_separated iff b₂,b₃ are_separated )

proof end;

theorem Th44: :: TSEP_2:44

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being non empty SubSpace of b₁ st b₄ is SubSpace of b₂ & b₅ is SubSpace of b₃ & b₄ union b₅ = b₂ union b₃ & b₄,b₅ are_weakly_separated holds
b₂,b₃ are_weakly_separated

proof end;

theorem Th45: :: TSEP_2:45

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being non empty SubSpace of b₁ st b₄ is SubSpace of b₂ & b₅ is SubSpace of b₃ & b₄ meets b₅ & b₄ meet b₅ = b₂ meet b₃ & b₂,b₃ are_weakly_separated holds
b₄,b₅ are_weakly_separated

proof end;

theorem Th46: :: TSEP_2:46

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃, b₄ being SubSpace of b₁
for b₅, b₆ being SubSpace of b₂ st the carrier of b₃ = the carrier of b₅ & the carrier of b₄ = the carrier of b₆ holds
( b₃,b₄ are_separated iff b₅,b₆ are_separated )

proof end;

theorem Th47: :: TSEP_2:47

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ st b₃ meets b₂ & b₄ meets b₂ holds
for b₅, b₆ being SubSpace of b₂ st b₅ = b₃ meet b₂ & b₆ = b₄ meet b₂ & b₃,b₄ are_separated holds
b₅,b₆ are_separated

proof end;

theorem Th48: :: TSEP_2:48

proof end;

theorem Th49: :: TSEP_2:49

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being non empty SubSpace of b₁ st b₃ meets b₂ & b₄ meets b₂ holds
for b₅, b₆ being SubSpace of b₂ st b₅ = b₃ meet b₂ & b₆ = b₄ meet b₂ & b₃,b₄ are_weakly_separated holds
b₅,b₆ are_weakly_separated

proof end;