CONNSP_1: Connected Spaces

:: Connected Spaces
:: by Beata Padlewska
::
:: Received May 6, 1989
:: Copyright (c) 1990 Association of Mizar Users

begin

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 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 X9 being SubSpace of GX
for P1, Q1 being Subset of GX
for P, Q being Subset of X9 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 X9 being SubSpace of GX
for P, Q being Subset of GX
for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & 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 X9 being SubSpace of GX
for A being Subset of GX
for B being Subset of X9 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 :: CONNSP_1:29

canceled;

registration

let GX be non empty TopSpace;
let x be Point of GX;
cluster {x} -> connected Subset of GX;
coherence

proof end;

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;
attr A is a_component 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 a_component CONNSP_1:def 5 :

registration

let GX be TopStruct ;
cluster a_component -> connected Element of K10( the carrier of GX);
coherence by Def5;

end;

registration

let GX be non empty TopSpace;
cluster a_component -> non empty Element of K10( the carrier of GX);
coherence

proof end;

end;

theorem :: CONNSP_1:34

for GX being non empty TopSpace
for A being Subset of GX st A is a_component holds
A <> {} GX ;

registration

let GX be TopSpace;
cluster a_component -> closed Element of K10( the carrier of GX);
coherence

proof end;

end;

theorem :: CONNSP_1:35

for GX being TopSpace
for A being Subset of GX st A is a_component holds
A is closed ;

theorem Th36: :: CONNSP_1:36

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

proof end;

theorem :: CONNSP_1:37

for GX being TopSpace
for A, B being Subset of GX st A is a_component & B is a_component & not A = B holds
A misses B by Th2, Th36;

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 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 );

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 Component_of 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 Component_of CONNSP_1:def 7 :

theorem Th40: :: CONNSP_1:40

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

proof end;

theorem :: CONNSP_1:41

canceled;

registration

let GX be non empty TopSpace;
let x be Point of GX;
cluster Component_of x -> non empty connected ;
coherence

proof end;

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 & Component_of x c= C holds
C = Component_of 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 iff ex x being Point of GX st A = Component_of 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 & x in A holds
A = Component_of x

proof end;

theorem :: CONNSP_1:45

for GX being non empty TopSpace
for x, p being Point of GX st p in Component_of x holds
Component_of p = Component_of x

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 ) ) holds
F is Cover of GX

proof end;

begin

registration

let T be TopStruct ;
cluster empty Element of K10( the carrier of T);
existence

proof end;

end;

registration

let T be TopStruct ;
cluster empty -> connected Element of K10( the carrier of T);
coherence

proof end;

end;

theorem Th47: :: CONNSP_1:47

for T being TopSpace
for X being set holds
( X is connected Subset of T iff X is connected Subset of TopStruct(# the carrier of T, the topology of T #) )

proof end;

theorem :: CONNSP_1:48

for T being TopSpace
for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
( X is a_component iff Y is a_component )

proof end;