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


begin

::
:: Separated sets
::
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
for A, B being Subset of GX st Cl A misses B & A misses Cl B holds
( Cl B misses A & B misses Cl A ) ;
end;

:: deftheorem Def1 defines are_separated CONNSP_1:def 1 :
for GX being TopStruct
for A, B being Subset of GX holds
( A,B are_separated iff ( Cl A misses B & A misses Cl B ) );

theorem Th1: :: CONNSP_1:1
for TS being TopStruct
for K, L being Subset of TS st K,L are_separated holds
K misses L
proof end;

theorem Th2: :: CONNSP_1:2
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 Th3: :: CONNSP_1:3
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 Th4: :: CONNSP_1:4
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 Th5: :: CONNSP_1:5
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 Th6: :: CONNSP_1:6
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 Th7: :: CONNSP_1:7
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 Th8: :: CONNSP_1:8
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 Th9: :: CONNSP_1:9
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;

::
:: Connected Spaces
::
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 :
for GX being TopStruct holds
( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated & not A = {} GX holds
B = {} GX );

theorem Th10: :: CONNSP_1:10
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: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 open & B is open holds
A meets B )
proof end;

theorem Th12: :: CONNSP_1:12
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:13
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:14
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;

::
:: Connected Sets
::
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 :
for GX being TopStruct
for A being Subset of GX holds
( A is connected iff GX | A is connected );

theorem Th15: :: CONNSP_1:15
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 Th16: :: CONNSP_1:16
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 Th17: :: CONNSP_1:17
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 Th18: :: CONNSP_1:18
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 Th19: :: CONNSP_1:19
for GX being TopSpace
for A being Subset of GX st A is connected holds
Cl A is connected
proof end;

theorem Th20: :: CONNSP_1:20
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:21
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:22
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 Th23: :: CONNSP_1:23
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:24
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 Th25: :: CONNSP_1:25
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 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 ) & meet F <> {} GX holds
union F is connected
proof end;

theorem Th27: :: CONNSP_1:27
for GX being TopSpace holds
( [#] GX is connected iff GX is connected )
proof end;

registration
let GX be non empty TopSpace;
let x be Point of GX;
cluster {x} -> connected for Subset of GX;
coherence
for b1 being Subset of GX st b1 = {x} holds
b1 is connected
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 :
for GX being TopStruct
for x, y being Point of GX holds
( x,y are_joined iff ex C being Subset of GX st
( C is connected & x in C & y in C ) );

theorem Th28: :: CONNSP_1:28
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 Th29: :: CONNSP_1:29
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:30
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 Th31: :: CONNSP_1:31
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;

::
:: Components of Topological Spaces
::
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 :
for GX being TopStruct
for A being Subset of GX holds
( A is a_component iff ( A is connected & ( for B being Subset of GX st B is connected & A c= B holds
A = B ) ) );

registration
let GX be TopStruct ;
cluster a_component -> connected for Element of K10( the carrier of GX);
coherence
for b1 being Subset of GX st b1 is a_component holds
b1 is connected by Def5;
end;

registration
let GX be non empty TopSpace;
cluster a_component -> non empty for Element of K10( the carrier of GX);
coherence
for b1 being Subset of GX st b1 is a_component holds
not b1 is empty
proof end;
end;

theorem :: CONNSP_1:32
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 for Element of K10( the carrier of GX);
coherence
for b1 being Subset of GX st b1 is a_component holds
b1 is closed
proof end;
end;

theorem :: CONNSP_1:33
for GX being TopSpace
for A being Subset of GX st A is a_component holds
A is closed ;

theorem Th34: :: CONNSP_1:34
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:35
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 Th1, Th34;

theorem :: CONNSP_1:36
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 :
for GX being TopStruct
for A, B being Subset of GX holds
( B is_a_component_of A iff ex B1 being Subset of (GX | A) st
( B1 = B & B1 is a_component ) );

theorem :: CONNSP_1:37
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;

::
:: A Component of a Point
::
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
ex b1 being Subset of GX 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 = b1 )
proof end;
uniqueness
for b1, b2 being Subset of GX st 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 = b1 ) & 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 = b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Component_of CONNSP_1:def 7 :
for GX being TopStruct
for x being Point of GX
for b3 being Subset of GX holds
( b3 = Component_of x iff 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 = b3 ) );

theorem Th38: :: CONNSP_1:38
for GX being non empty TopSpace
for x being Point of GX holds x in Component_of x
proof end;

registration
let GX be non empty TopSpace;
let x be Point of GX;
cluster Component_of x -> non empty connected ;
coherence
( not Component_of x is empty & Component_of x is connected )
proof end;
end;

theorem Th39: :: CONNSP_1:39
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 Th40: :: CONNSP_1:40
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:41
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:42
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:43
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 for Element of K10( the carrier of T);
existence
ex b1 being Subset of T st b1 is empty
proof end;
end;

registration
let T be TopStruct ;
cluster empty -> connected for Element of K10( the carrier of T);
coherence
for b1 being Subset of T st b1 is empty holds
b1 is connected
proof end;
end;

theorem Th44: :: CONNSP_1:44
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:45
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;

:: from JORDAN2C, 2011.07.03, A.T.
theorem :: CONNSP_1:46
for G being non empty TopSpace
for P, A being Subset of G
for Q being Subset of (G | A) st P = Q & P is connected holds
Q is connected
proof end;