:: CONNSP_3 semantic presentation

definition

let GX be TopStruct ;
let V be Subset of GX;
func skl V -> Subset of GX means :Def1: :: CONNSP_3:def 1
ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) ) & union F = it );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines skl CONNSP_3:def 1 :

theorem Th1: :: CONNSP_3:1

for GX being TopSpace
for V being Subset of GX st ex A being Subset of GX st
( A is connected & V c= A ) holds
V c= skl V

proof end;

theorem :: CONNSP_3:2

for GX being TopSpace
for V being Subset of GX st ( for A being Subset of GX holds
( not A is connected or not V c= A ) ) holds
skl V = {}

proof end;

theorem Th3: :: CONNSP_3:3

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

proof end;

theorem :: CONNSP_3:4

for GX being non empty TopSpace
for V being Subset of GX st V is connected holds
skl V <> {}

proof end;

theorem Th5: :: CONNSP_3:5

for GX being TopSpace
for V being Subset of GX st V is connected & V <> {} holds
skl V is connected

proof end;

theorem Th6: :: CONNSP_3:6

for GX being non empty TopSpace
for V, C being Subset of GX st V is connected & C is connected & skl V c= C holds
C = skl V

proof end;

theorem Th7: :: CONNSP_3:7

for GX being non empty TopSpace
for A being Subset of GX st A is_a_component_of GX holds
skl A = A

proof end;

theorem Th8: :: CONNSP_3:8

for GX being non empty TopSpace
for A being Subset of GX holds
( A is_a_component_of GX iff ex V being Subset of GX st
( V is connected & V <> {} & A = skl V ) )

proof end;

theorem :: CONNSP_3:9

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

theorem Th10: :: CONNSP_3:10

for GX being non empty TopSpace
for A, V being Subset of GX st A is_a_component_of GX & V is connected & V c= A & V <> {} holds
A = skl V

proof end;

theorem Th11: :: CONNSP_3:11

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

proof end;

theorem Th12: :: CONNSP_3:12

for GX being non empty TopSpace
for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds
skl A = skl B

proof end;

theorem Th13: :: CONNSP_3:13

for GX being non empty TopSpace
for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds
B c= skl A

proof end;

theorem Th14: :: CONNSP_3:14

for GX being non empty TopSpace
for A, B being Subset of GX st A is connected & A \/ B is connected & A <> {} holds
A \/ B c= skl A

proof end;

theorem Th15: :: CONNSP_3:15

for GX being non empty TopSpace
for A being Subset of GX
for p being Point of GX st A is connected & p in A holds
skl p = skl A

proof end;

theorem :: CONNSP_3:16

for GX being non empty TopSpace
for A, B being Subset of GX st A is connected & B is connected & A meets B holds
( A \/ B c= skl A & A \/ B c= skl B & A c= skl B & B c= skl A )

proof end;

theorem :: CONNSP_3:17

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

proof end;

theorem :: CONNSP_3:18

for GX being non empty TopSpace
for A, B being Subset of GX st A is_a_component_of GX & B is connected & B <> {} & A misses B holds
A misses skl B

proof end;

Lm1: now

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

end;

definition

let GX be TopStruct ;
mode a_union_of_components of GX -> Subset of GX means :Def2: :: CONNSP_3:def 2
ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is_a_component_of GX ) & it = union F );
existence

proof end;

end;

:: deftheorem Def2 defines a_union_of_components CONNSP_3:def 2 :

theorem Th19: :: CONNSP_3:19

for GX being non empty TopSpace holds {} GX is a_union_of_components of GX

proof end;

theorem :: CONNSP_3:20

for GX being non empty TopSpace
for A being Subset of GX st A = the carrier of GX holds
A is a_union_of_components of GX

proof end;

theorem Th21: :: CONNSP_3:21

for GX being non empty TopSpace
for A being Subset of GX
for p being Point of GX st p in A & A is a_union_of_components of GX holds
skl p c= A

proof end;

theorem :: CONNSP_3:22

for GX being non empty TopSpace
for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds
( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX )

proof end;

theorem :: CONNSP_3:23

for GX being non empty TopSpace
for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) holds
union Fu is a_union_of_components of GX

proof end;

theorem :: CONNSP_3:24

for GX being non empty TopSpace
for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds
A is a_union_of_components of GX ) holds
meet Fu is a_union_of_components of GX

proof end;

theorem :: CONNSP_3:25

for GX being non empty TopSpace
for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds
A \ B is a_union_of_components of GX

proof end;

definition

let GX be TopStruct ;
let B be Subset of GX;
let p be Point of GX;
assume A1: p in B ;
func Down p,B -> Point of (GX | B) equals :Def3: :: CONNSP_3:def 3
p;
coherence

proof end;

end;

:: deftheorem Def3 defines Down CONNSP_3:def 3 :

definition

let GX be TopStruct ;
let B be Subset of GX;
let p be Point of (GX | B);
assume A1: B <> {} ;
func Up p -> Point of GX equals :: CONNSP_3:def 4
p;
coherence

proof end;

end;

:: deftheorem defines Up CONNSP_3:def 4 :

definition

let GX be TopStruct ;
let V, B be Subset of GX;
func Down V,B -> Subset of (GX | B) equals :: CONNSP_3:def 5
V /\ B;
coherence

proof end;

end;

:: deftheorem defines Down CONNSP_3:def 5 :

definition

let GX be TopStruct ;
let B be Subset of GX;
let V be Subset of (GX | B);
func Up V -> Subset of GX equals :: CONNSP_3:def 6
V;
coherence

proof end;

end;

:: deftheorem defines Up CONNSP_3:def 6 :

definition

let GX be TopStruct ;
let B be Subset of GX;
let p be Point of GX;
assume A1: p in B ;
func skl p,B -> Subset of GX means :Def7: :: CONNSP_3:def 7
for q being Point of (GX | B) st q = p holds
it = skl q;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines skl CONNSP_3:def 7 :

theorem :: CONNSP_3:26

for GX being non empty TopSpace
for B being Subset of GX
for p being Point of GX st p in B holds
p in skl p,B

proof end;

theorem Th27: :: CONNSP_3:27

for GX being non empty TopSpace
for B being Subset of GX
for p being Point of GX st p in B holds
skl p,B = skl (Down p,B)

proof end;

theorem Th28: :: CONNSP_3:28

for GX being non empty TopSpace
for V, B being Subset of GX st V c= B holds
Down V,B = V by XBOOLE_1:28;

theorem Th29: :: CONNSP_3:29

for GX being TopSpace
for V, B being Subset of GX st V is open holds
Down V,B is open

proof end;

theorem Th30: :: CONNSP_3:30

for GX being non empty TopSpace
for V, B being Subset of GX st V c= B holds
Cl (Down V,B) = (Cl V) /\ B

proof end;

theorem :: CONNSP_3:31

for GX being non empty TopSpace
for B being Subset of GX
for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B

proof end;

theorem :: CONNSP_3:32

for GX being non empty TopSpace
for V, B being Subset of GX st V c= B holds
Cl (Down V,B) c= Cl V

proof end;

theorem :: CONNSP_3:33

for GX being non empty TopSpace
for B being Subset of GX
for V being Subset of (GX | B) st V c= B holds
Down (Up V),B = V by Th28;

theorem Th34: :: CONNSP_3:34

for GX being TopSpace
for V, B being Subset of GX
for W being Subset of (GX | B) st V = W & W is connected holds
V is connected

proof end;

theorem :: CONNSP_3:35

for GX being non empty TopSpace
for B being Subset of GX
for p being Point of GX st p in B holds
skl p,B is connected

proof end;