:: CONNSP_3 semantic presentation

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines skl CONNSP_3:def 1 :

theorem Th1: :: CONNSP_3:1

for b₁ being TopSpace
for b₂ being Subset of b₁ st ex b₃ being Subset of b₁ st
( b₃ is connected & b₂ c= b₃ ) holds
b₂ c= skl b₂

proof end;

theorem Th2: :: CONNSP_3:2

for b₁ being TopSpace
for b₂ being Subset of b₁ st ( for b₃ being Subset of b₁ holds
( not b₃ is connected or not b₂ c= b₃ ) ) holds
skl b₂ = {}

proof end;

theorem Th3: :: CONNSP_3:3

for b₁ being non empty TopSpace holds skl ({} b₁) = the carrier of b₁

proof end;

theorem Th4: :: CONNSP_3:4

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

proof end;

theorem Th5: :: CONNSP_3:5

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is connected & b₂ <> {} holds
skl b₂ is connected

proof end;

theorem Th6: :: CONNSP_3:6

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

proof end;

theorem Th7: :: CONNSP_3:7

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is_a_component_of b₁ holds
skl b₂ = b₂

proof end;

theorem Th8: :: CONNSP_3:8

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ holds
( b₂ is_a_component_of b₁ iff ex b₃ being Subset of b₁ st
( b₃ is connected & b₃ <> {} & b₂ = skl b₃ ) )

proof end;

theorem Th9: :: CONNSP_3:9

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is connected & b₂ <> {} holds
skl b₂ is_a_component_of b₁ by Th8;

theorem Th10: :: CONNSP_3:10

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is_a_component_of b₁ & b₃ is connected & b₃ c= b₂ & b₃ <> {} holds
b₂ = skl b₃

proof end;

theorem Th11: :: CONNSP_3:11

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is connected & b₂ <> {} holds
skl (skl b₂) = skl b₂

proof end;

theorem Th12: :: CONNSP_3:12

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is connected & b₃ is connected & b₂ <> {} & b₂ c= b₃ holds
skl b₂ = skl b₃

proof end;

theorem Th13: :: CONNSP_3:13

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is connected & b₃ is connected & b₂ <> {} & b₂ c= b₃ holds
b₃ c= skl b₂

proof end;

theorem Th14: :: CONNSP_3:14

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is connected & b₂ \/ b₃ is connected & b₂ <> {} holds
b₂ \/ b₃ c= skl b₂

proof end;

theorem Th15: :: CONNSP_3:15

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

proof end;

theorem Th16: :: CONNSP_3:16

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is connected & b₃ is connected & b₂ meets b₃ holds
( b₂ \/ b₃ c= skl b₂ & b₂ \/ b₃ c= skl b₃ & b₂ c= skl b₃ & b₃ c= skl b₂ )

proof end;

theorem Th17: :: CONNSP_3:17

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is connected & b₂ <> {} holds
Cl b₂ c= skl b₂

proof end;

theorem Th18: :: CONNSP_3:18

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is_a_component_of b₁ & b₃ is connected & b₃ <> {} & b₂ misses b₃ holds
b₂ misses skl b₃

proof end;

E14: now

let c₁ be TopStruct ;
{} c= bool the carrier of c₁ by XBOOLE_1:2;
then reconsider c₂ = {} as Subset-Family of c₁ ;
( ( for b₁ being Subset of c₁ st b₁ in c₂ holds
b₁ is_a_component_of c₁ ) & {} c₁ = union c₂ ) by ZFMISC_1:2;
hence ex b₁ being Subset-Family of c₁ st
( ( for b₂ being Subset of c₁ st b₂ in b₁ holds
b₂ is_a_component_of c₁ ) & {} c₁ = union b₁ ) ;

end;

definition

let c₁ be TopStruct ;
mode a_union_of_components of c₁ -> Subset of a₁ means :Def2: :: CONNSP_3:def 2
ex b₁ being Subset-Family of a₁ st
( ( for b₂ being Subset of a₁ st b₂ in b₁ holds
b₂ is_a_component_of a₁ ) & a₂ = union b₁ );
existence

proof end;

end;

:: deftheorem Def2 defines a_union_of_components CONNSP_3:def 2 :

theorem Th19: :: CONNSP_3:19

for b₁ being non empty TopSpace holds {} b₁ is a_union_of_components of b₁

proof end;

theorem Th20: :: CONNSP_3:20

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ = the carrier of b₁ holds
b₂ is a_union_of_components of b₁

proof end;

theorem Th21: :: CONNSP_3:21

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

proof end;

theorem Th22: :: CONNSP_3:22

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is a_union_of_components of b₁ & b₃ is a_union_of_components of b₁ holds
( b₂ \/ b₃ is a_union_of_components of b₁ & b₂ /\ b₃ is a_union_of_components of b₁ )

proof end;

theorem Th23: :: CONNSP_3:23

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is a_union_of_components of b₁ ) holds
union b₂ is a_union_of_components of b₁

proof end;

theorem Th24: :: CONNSP_3:24

for b₁ being non empty TopSpace
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is a_union_of_components of b₁ ) holds
meet b₂ is a_union_of_components of b₁

proof end;

theorem Th25: :: CONNSP_3:25

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is a_union_of_components of b₁ & b₃ is a_union_of_components of b₁ holds
b₂ \ b₃ is a_union_of_components of b₁

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
let c₃ be Point of c₁;
assume E18: c₃ in c₂ ;
func Down c₃,c₂ -> Point of (a₁ | a₂) equals :Def3: :: CONNSP_3:def 3
a₃;
coherence

proof end;

end;

:: deftheorem Def3 defines Down CONNSP_3:def 3 :

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
let c₃ be Point of (c₁ | c₂);
assume E19: c₂ <> {} ;
func Up c₃ -> Point of a₁ equals :: CONNSP_3:def 4
a₃;
coherence

proof end;

end;

:: deftheorem Def4 defines Up CONNSP_3:def 4 :

definition

let c₁ be TopStruct ;
let c₂, c₃ be Subset of c₁;
func Down c₂,c₃ -> Subset of (a₁ | a₃) equals :: CONNSP_3:def 5
a₂ /\ a₃;
coherence

proof end;

end;

:: deftheorem Def5 defines Down CONNSP_3:def 5 :

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
let c₃ be Subset of (c₁ | c₂);
func Up c₃ -> Subset of a₁ equals :: CONNSP_3:def 6
a₃;
coherence

proof end;

end;

:: deftheorem Def6 defines Up CONNSP_3:def 6 :

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
let c₃ be Point of c₁;
assume E19: c₃ in c₂ ;
func skl c₃,c₂ -> Subset of a₁ means :Def7: :: CONNSP_3:def 7
for b₁ being Point of (a₁ | a₂) st b₁ = a₃ holds
a₄ = skl b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines skl CONNSP_3:def 7 :

theorem Th26: :: CONNSP_3:26

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

proof end;

theorem Th27: :: CONNSP_3:27

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₃ in b₂ holds
skl b₃,b₂ = skl (Down b₃,b₂)

proof end;

theorem Th28: :: CONNSP_3:28

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
Down b₂,b₃ = b₂ by XBOOLE_1:28;

theorem Th29: :: CONNSP_3:29

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open holds
Down b₂,b₃ is open

proof end;

theorem Th30: :: CONNSP_3:30

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
Cl (Down b₂,b₃) = (Cl b₂) /\ b₃

proof end;

theorem Th31: :: CONNSP_3:31

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset of (b₁ | b₂) holds Cl b₃ = (Cl (Up b₃)) /\ b₂

proof end;

theorem Th32: :: CONNSP_3:32

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
Cl (Down b₂,b₃) c= Cl b₂

proof end;

theorem Th33: :: CONNSP_3:33

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset of (b₁ | b₂) st b₃ c= b₂ holds
Down (Up b₃),b₂ = b₃ by Th28;

theorem Th34: :: CONNSP_3:34

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Subset of (b₁ | b₃) st b₂ = b₄ & b₄ is connected holds
b₂ is connected

proof end;

theorem Th35: :: CONNSP_3:35

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₃ in b₂ holds
skl b₃,b₂ is connected

proof end;