:: CONNSP_1 semantic presentation

definition

let GX be TopStruct ;
let A, B be Subset of GX;
pred A,B are_separated means :Def1: :: CONNSP_1:def 1
( Cl A misses B & A misses Cl B );
symmetry ;

end;

:: deftheorem Def1 defines are_separated CONNSP_1:def 1 :

theorem :: CONNSP_1:1

canceled;

theorem Th2: :: CONNSP_1:2

for TS being TopStruct
for K, L being Subset of TS st K,L are_separated holds
K misses L

proof end;

theorem Th3: :: CONNSP_1:3

for TS being TopStruct
for K, L being Subset of TS st [#] TS = K \/ L & K is closed & L is closed & K misses L holds
K,L are_separated

proof end;

theorem Th4: :: CONNSP_1:4

for GX being TopSpace
for A, B being Subset of GX st [#] GX = A \/ B & A is open & B is open & A misses B holds
A,B are_separated

proof end;

theorem Th5: :: CONNSP_1:5

for GX being TopSpace
for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated holds
( A is open & A is closed & B is open & B is closed )

proof end;

theorem Th6: :: CONNSP_1:6

for GX being TopSpace
for X' being SubSpace of GX
for P1, Q1 being Subset of GX
for P, Q being Subset of X' st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated

proof end;

theorem Th7: :: CONNSP_1:7

for GX being TopSpace
for X' being SubSpace of GX
for P, Q being Subset of GX
for P1, Q1 being Subset of X' st P = P1 & Q = Q1 & P \/ Q c= [#] X' & P,Q are_separated holds
P1,Q1 are_separated

proof end;

theorem Th8: :: CONNSP_1:8

for TS being TopStruct
for K, L, K1, L1 being Subset of TS st K,L are_separated & K1 c= K & L1 c= L holds
K1,L1 are_separated

proof end;

theorem Th9: :: CONNSP_1:9

for GX being TopSpace
for A, B, C being Subset of GX st A,B are_separated & A,C are_separated holds
A,B \/ C are_separated

proof end;

theorem Th10: :: CONNSP_1:10

for TS being TopStruct
for K, L being Subset of TS st ( ( K is closed & L is closed ) or ( K is open & L is open ) ) holds
K \ L,L \ K are_separated

proof end;

definition

let GX be TopStruct ;
attr GX is connected means :Def2: :: CONNSP_1:def 2
for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated & not A = {} GX holds
B = {} GX;

end;

:: deftheorem Def2 defines connected CONNSP_1:def 2 :

theorem Th11: :: CONNSP_1:11

for GX being TopSpace holds
( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is closed & B is closed holds
A meets B )

proof end;

theorem :: CONNSP_1:12

for GX being TopSpace holds
( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds
A meets B )

proof end;

theorem Th13: :: CONNSP_1:13

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

proof end;

theorem :: CONNSP_1:14

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

proof end;

theorem :: CONNSP_1:15

for GX, GY being TopSpace
for F being Function of GX,GY st F is continuous & F .: ([#] GX) = [#] GY & GX is connected holds
GY is connected

proof end;

definition

let GX be TopStruct ;
let A be Subset of GX;
attr A is connected means :Def3: :: CONNSP_1:def 3
GX | A is connected;

end;

:: deftheorem Def3 defines connected CONNSP_1:def 3 :

theorem Th16: :: CONNSP_1:16

for GX being TopSpace
for A being Subset of GX holds
( A is connected iff for P, Q being Subset of GX st A = P \/ Q & P,Q are_separated & not P = {} GX holds
Q = {} GX )

proof end;

theorem Th17: :: CONNSP_1:17

for GX being TopSpace
for A, B, C being Subset of GX st A is connected & A c= B \/ C & B,C are_separated & not A c= B holds
A c= C

proof end;

theorem Th18: :: CONNSP_1:18

for GX being TopSpace
for A, B being Subset of GX st A is connected & B is connected & not A,B are_separated holds
A \/ B is connected

proof end;

theorem Th19: :: CONNSP_1:19

for GX being TopSpace
for C, A being Subset of GX st C is connected & C c= A & A c= Cl C holds
A is connected

proof end;

theorem Th20: :: CONNSP_1:20

for GX being TopSpace
for A being Subset of GX st A is connected holds
Cl A is connected

proof end;

theorem Th21: :: CONNSP_1:21

for GX being TopSpace
for A, B, C being Subset of GX st GX is connected & A is connected & ([#] GX) \ A = B \/ C & B,C are_separated holds
( A \/ B is connected & A \/ C is connected )

proof end;

theorem :: CONNSP_1:22

for GX being TopSpace
for A, B, C being Subset of GX st ([#] GX) \ A = B \/ C & B,C are_separated & A is closed holds
( A \/ B is closed & A \/ C is closed )

proof end;

theorem :: CONNSP_1:23

for GX being TopSpace
for C, A being Subset of GX st C is connected & C meets A & C \ A <> {} GX holds
C meets Fr A

proof end;

theorem Th24: :: CONNSP_1:24

for GX being TopSpace
for X' being SubSpace of GX
for A being Subset of GX
for B being Subset of X' st A = B holds
( A is connected iff B is connected )

proof end;

theorem :: CONNSP_1:25

for GX being TopSpace
for A, B being Subset of GX st A is closed & B is closed & A \/ B is connected & A /\ B is connected holds
( A is connected & B is connected )

proof end;

theorem Th26: :: CONNSP_1:26

for GX being TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is connected ) & ex A being Subset of GX st
( A <> {} GX & A in F & ( for B being Subset of GX st B in F & B <> A holds
not A,B are_separated ) ) holds
union F is connected

proof end;

theorem Th27: :: CONNSP_1:27

for GX being TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is connected ) & meet F <> {} GX holds
union F is connected

proof end;

theorem Th28: :: CONNSP_1:28

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

proof end;

theorem Th29: :: CONNSP_1:29

for GX being non empty TopSpace
for x being Point of GX holds {x} is connected

proof end;

definition

let GX be TopStruct ;
let x, y be Point of GX;
pred x,y are_joined means :Def4: :: CONNSP_1:def 4
ex C being Subset of GX st
( C is connected & x in C & y in C );

end;

:: deftheorem Def4 defines are_joined CONNSP_1:def 4 :

theorem Th30: :: CONNSP_1:30

for GX being non empty TopSpace st ex x being Point of GX st
for y being Point of GX holds x,y are_joined holds
GX is connected

proof end;

theorem Th31: :: CONNSP_1:31

for GX being TopSpace holds
( ex x being Point of GX st
for y being Point of GX holds x,y are_joined iff for x, y being Point of GX holds x,y are_joined )

proof end;

theorem :: CONNSP_1:32

for GX being non empty TopSpace st ( for x, y being Point of GX holds x,y are_joined ) holds
GX is connected

proof end;

theorem Th33: :: CONNSP_1:33

for GX being non empty TopSpace
for x being Point of GX
for F being Subset-Family of GX st ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) holds
F <> {}

proof end;

definition

let GX be TopStruct ;
let A be Subset of GX;
pred A is_a_component_of GX means :Def5: :: CONNSP_1:def 5
( A is connected & ( for B being Subset of GX 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 GX being non empty TopSpace
for A being Subset of GX st A is_a_component_of GX holds
A <> {} GX

proof end;

theorem :: CONNSP_1:35

for GX being TopSpace
for A being Subset of GX st A is_a_component_of GX holds
A is closed

proof end;

theorem Th36: :: CONNSP_1:36

for GX being TopSpace
for A, B being Subset of GX st A is_a_component_of GX & B is_a_component_of GX & not A = B holds
A,B are_separated

proof end;

theorem Th37: :: CONNSP_1:37

for GX being TopSpace
for A, B being Subset of GX st A is_a_component_of GX & B is_a_component_of GX & not A = B holds
A misses B

proof end;

theorem :: CONNSP_1:38

for GX being TopSpace
for C being Subset of GX st C is connected holds
for S being Subset of GX holds
( not S is_a_component_of GX or C misses S or C c= S )

proof end;

definition

let GX be TopStruct ;
let A, B be Subset of GX;
pred B is_a_component_of A means :Def6: :: CONNSP_1:def 6
ex B1 being Subset of (GX | A) st
( B1 = B & B1 is_a_component_of GX | A );

end;

:: deftheorem Def6 defines is_a_component_of CONNSP_1:def 6 :

theorem :: CONNSP_1:39

for GX being TopSpace
for A, C being Subset of GX st GX is connected & A is connected & C is_a_component_of ([#] GX) \ A holds
([#] GX) \ C is connected

proof end;

definition

let GX be TopStruct ;
let x be Point of GX;
func skl x -> Subset of GX means :Def7: :: CONNSP_1:def 7
ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = it );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines skl CONNSP_1:def 7 :

theorem Th40: :: CONNSP_1:40

for GX being non empty TopSpace
for x being Point of GX holds x in skl x

proof end;

theorem Th41: :: CONNSP_1:41

for GX being non empty TopSpace
for x being Point of GX holds skl x is connected

proof end;

theorem Th42: :: CONNSP_1:42

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

proof end;

theorem Th43: :: CONNSP_1:43

for GX being non empty TopSpace
for A being Subset of GX holds
( A is_a_component_of GX iff ex x being Point of GX st A = skl x )

proof end;

theorem :: CONNSP_1:44

for GX being non empty TopSpace
for A being Subset of GX
for x being Point of GX st A is_a_component_of GX & x in A holds
A = skl x

proof end;

theorem :: CONNSP_1:45

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

proof end;

theorem :: CONNSP_1:46

for GX being non empty TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX holds
( A in F iff A is_a_component_of GX ) ) holds
F is_a_cover_of GX

proof end;