:: CONNSP_1 semantic presentation

definition

let c₁ be TopStruct ;
let c₂, c₃ be Subset of c₁;
pred c₂,c₃ are_separated means :Def1: :: CONNSP_1:def 1
( Cl a₂ misses a₃ & a₂ misses Cl a₃ );
symmetry ;

end;

:: deftheorem Def1 defines are_separated CONNSP_1:def 1 :

theorem Th1: :: CONNSP_1:1

canceled;

theorem Th2: :: CONNSP_1:2

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₂,b₃ are_separated holds
b₂ misses b₃

proof end;

theorem Th3: :: CONNSP_1:3

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st [#] b₁ = b₂ \/ b₃ & b₂ is closed & b₃ is closed & b₂ misses b₃ holds
b₂,b₃ are_separated

proof end;

theorem Th4: :: CONNSP_1:4

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st [#] b₁ = b₂ \/ b₃ & b₂ is open & b₃ is open & b₂ misses b₃ holds
b₂,b₃ are_separated

proof end;

theorem Th5: :: CONNSP_1:5

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st [#] b₁ = b₂ \/ b₃ & b₂,b₃ are_separated holds
( b₂ is open & b₂ is closed & b₃ is open & b₃ is closed )

proof end;

theorem Th6: :: CONNSP_1:6

for b₁ being TopSpace
for b₂ being SubSpace of b₁
for b₃, b₄ being Subset of b₁
for b₅, b₆ being Subset of b₂ st b₅ = b₃ & b₆ = b₄ & b₅,b₆ are_separated holds
b₃,b₄ are_separated

proof end;

theorem Th7: :: CONNSP_1:7

for b₁ being TopSpace
for b₂ being SubSpace of b₁
for b₃, b₄ being Subset of b₁
for b₅, b₆ being Subset of b₂ st b₃ = b₅ & b₄ = b₆ & b₃ \/ b₄ c= [#] b₂ & b₃,b₄ are_separated holds
b₅,b₆ are_separated

proof end;

theorem Th8: :: CONNSP_1:8

for b₁ being TopStruct
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂,b₃ are_separated & b₄ c= b₂ & b₅ c= b₃ holds
b₄,b₅ are_separated

proof end;

theorem Th9: :: CONNSP_1:9

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂,b₃ are_separated & b₂,b₄ are_separated holds
b₂,b₃ \/ b₄ are_separated

proof end;

theorem Th10: :: CONNSP_1:10

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st ( ( b₂ is closed & b₃ is closed ) or ( b₂ is open & b₃ is open ) ) holds
b₂ \ b₃,b₃ \ b₂ are_separated

proof end;

definition

let c₁ be TopStruct ;
attr a₁ is connected means :Def2: :: CONNSP_1:def 2
for b₁, b₂ being Subset of a₁ st [#] a₁ = b₁ \/ b₂ & b₁,b₂ are_separated & not b₁ = {} a₁ holds
b₂ = {} a₁;

end;

:: deftheorem Def2 defines connected CONNSP_1:def 2 :

theorem Th11: :: CONNSP_1:11

for b₁ being TopSpace holds
( b₁ is connected iff for b₂, b₃ being Subset of b₁ st [#] b₁ = b₂ \/ b₃ & b₂ <> {} b₁ & b₃ <> {} b₁ & b₂ is closed & b₃ is closed holds
b₂ meets b₃ )

proof end;

theorem Th12: :: CONNSP_1:12

for b₁ being TopSpace holds
( b₁ is connected iff for b₂, b₃ being Subset of b₁ st [#] b₁ = b₂ \/ b₃ & b₂ <> {} b₁ & b₃ <> {} b₁ & b₂ is open & b₃ is open holds
b₂ meets b₃ )

proof end;

theorem Th13: :: CONNSP_1:13

for b₁ being TopSpace holds
( b₁ is connected iff for b₂ being Subset of b₁ st b₂ <> {} b₁ & b₂ <> [#] b₁ holds
Cl b₂ meets Cl (([#] b₁) \ b₂) )

proof end;

theorem Th14: :: CONNSP_1:14

for b₁ being TopSpace holds
( b₁ is connected iff for b₂ being Subset of b₁ st b₂ is open & b₂ is closed & not b₂ = {} b₁ holds
b₂ = [#] b₁ )

proof end;

theorem Th15: :: CONNSP_1:15

for b₁, b₂ being TopSpace
for b₃ being Function of b₁,b₂ st b₃ is continuous & b₃ .: ([#] b₁) = [#] b₂ & b₁ is connected holds
b₂ is connected

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is connected means :Def3: :: CONNSP_1:def 3
a₁ | a₂ is connected;

end;

:: deftheorem Def3 defines connected CONNSP_1:def 3 :

theorem Th16: :: CONNSP_1:16

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is connected iff for b₃, b₄ being Subset of b₁ st b₂ = b₃ \/ b₄ & b₃,b₄ are_separated & not b₃ = {} b₁ holds
b₄ = {} b₁ )

proof end;

theorem Th17: :: CONNSP_1:17

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is connected & b₂ c= b₃ \/ b₄ & b₃,b₄ are_separated & not b₂ c= b₃ holds
b₂ c= b₄

proof end;

theorem Th18: :: CONNSP_1:18

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is connected & b₃ is connected & not b₂,b₃ are_separated holds
b₂ \/ b₃ is connected

proof end;

theorem Th19: :: CONNSP_1:19

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is connected & b₂ c= b₃ & b₃ c= Cl b₂ holds
b₃ is connected

proof end;

theorem Th20: :: CONNSP_1:20

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is connected holds
Cl b₂ is connected

proof end;

theorem Th21: :: CONNSP_1:21

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₁ is connected & b₂ is connected & ([#] b₁) \ b₂ = b₃ \/ b₄ & b₃,b₄ are_separated holds
( b₂ \/ b₃ is connected & b₂ \/ b₄ is connected )

proof end;

theorem Th22: :: CONNSP_1:22

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st ([#] b₁) \ b₂ = b₃ \/ b₄ & b₃,b₄ are_separated & b₂ is closed holds
( b₂ \/ b₃ is closed & b₂ \/ b₄ is closed )

proof end;

theorem Th23: :: CONNSP_1:23

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is connected & b₂ meets b₃ & b₂ \ b₃ <> {} b₁ holds
b₂ meets Fr b₃

proof end;

theorem Th24: :: CONNSP_1:24

for b₁ being TopSpace
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
( b₃ is connected iff b₄ is connected )

proof end;

theorem Th25: :: CONNSP_1:25

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed & b₂ \/ b₃ is connected & b₂ /\ b₃ is connected holds
( b₂ is connected & b₃ is connected )

proof end;

theorem Th26: :: CONNSP_1:26

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is connected ) & ex b₃ being Subset of b₁ st
( b₃ <> {} b₁ & b₃ in b₂ & ( for b₄ being Subset of b₁ st b₄ in b₂ & b₄ <> b₃ holds
not b₃,b₄ are_separated ) ) holds
union b₂ is connected

proof end;

theorem Th27: :: CONNSP_1:27

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is connected ) & meet b₂ <> {} b₁ holds
union b₂ is connected

proof end;

theorem Th28: :: CONNSP_1:28

for b₁ being TopSpace holds
( [#] b₁ is connected iff b₁ is connected )

proof end;

theorem Th29: :: CONNSP_1:29

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds {b₂} is connected

proof end;

definition

let c₁ be TopStruct ;
let c₂, c₃ be Point of c₁;
pred c₂,c₃ are_joined means :Def4: :: CONNSP_1:def 4
ex b₁ being Subset of a₁ st
( b₁ is connected & a₂ in b₁ & a₃ in b₁ );

end;

:: deftheorem Def4 defines are_joined CONNSP_1:def 4 :

theorem Th30: :: CONNSP_1:30

for b₁ being non empty TopSpace st ex b₂ being Point of b₁ st
for b₃ being Point of b₁ holds b₂,b₃ are_joined holds
b₁ is connected

proof end;

theorem Th31: :: CONNSP_1:31

for b₁ being TopSpace holds
( ex b₂ being Point of b₁ st
for b₃ being Point of b₁ holds b₂,b₃ are_joined iff for b₂, b₃ being Point of b₁ holds b₂,b₃ are_joined )

proof end;

theorem Th32: :: CONNSP_1:32

for b₁ being non empty TopSpace st ( for b₂, b₃ being Point of b₁ holds b₂,b₃ are_joined ) holds
b₁ is connected

proof end;

theorem Th33: :: CONNSP_1:33

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Subset-Family of b₁ st ( for b₄ being Subset of b₁ holds
( b₄ in b₃ iff ( b₄ is connected & b₂ in b₄ ) ) ) holds
b₃ <> {}

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
pred c₂ is_a_component_of c₁ means :Def5: :: CONNSP_1:def 5
( a₂ is connected & ( for b₁ being Subset of a₁ st b₁ is connected & a₂ c= b₁ holds
a₂ = b₁ ) );

end;

:: deftheorem Def5 defines is_a_component_of CONNSP_1:def 5 :

theorem Th34: :: CONNSP_1:34

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is_a_component_of b₁ holds
b₂ <> {} b₁

proof end;

theorem Th35: :: CONNSP_1:35

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is_a_component_of b₁ holds
b₂ is closed

proof end;

theorem Th36: :: CONNSP_1:36

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is_a_component_of b₁ & b₃ is_a_component_of b₁ & not b₂ = b₃ holds
b₂,b₃ are_separated

proof end;

theorem Th37: :: CONNSP_1:37

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is_a_component_of b₁ & b₃ is_a_component_of b₁ & not b₂ = b₃ holds
b₂ misses b₃

proof end;

theorem Th38: :: CONNSP_1:38

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is connected holds
for b₃ being Subset of b₁ holds
( not b₃ is_a_component_of b₁ or b₂ misses b₃ or b₂ c= b₃ )

proof end;

definition

let c₁ be TopStruct ;
let c₂, c₃ be Subset of c₁;
pred c₃ is_a_component_of c₂ means :Def6: :: CONNSP_1:def 6
ex b₁ being Subset of (a₁ | a₂) st
( b₁ = a₃ & b₁ is_a_component_of a₁ | a₂ );

end;

:: deftheorem Def6 defines is_a_component_of CONNSP_1:def 6 :

theorem Th39: :: CONNSP_1:39

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₁ is connected & b₂ is connected & b₃ is_a_component_of ([#] b₁) \ b₂ holds
([#] b₁) \ b₃ is connected

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Point of c₁;
func skl c₂ -> Subset of a₁ means :Def7: :: CONNSP_1:def 7
ex b₁ being Subset-Family of a₁ st
( ( for b₂ being Subset of a₁ holds
( b₂ in b₁ iff ( b₂ is connected & a₂ in b₂ ) ) ) & union b₁ = a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines skl CONNSP_1:def 7 :

theorem Th40: :: CONNSP_1:40

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds b₂ in skl b₂

proof end;

theorem Th41: :: CONNSP_1:41

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds skl b₂ is connected

proof end;

theorem Th42: :: CONNSP_1:42

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ is connected & skl b₃ c= b₂ holds
b₂ = skl b₃

proof end;

theorem Th43: :: CONNSP_1:43

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is_a_component_of b₁ iff ex b₃ being Point of b₁ st b₂ = skl b₃ )

proof end;

theorem Th44: :: CONNSP_1:44

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ is_a_component_of b₁ & b₃ in b₂ holds
b₂ = skl b₃

proof end;

theorem Th45: :: CONNSP_1:45

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ = skl b₃ holds
for b₄ being Point of b₁ st b₄ in b₂ holds
skl b₄ = b₂

proof end;

theorem Th46: :: CONNSP_1:46

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ holds
( b₃ in b₂ iff b₃ is_a_component_of b₁ ) ) holds
b₂ is_a_cover_of b₁

proof end;