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

::
:: Separated sets
::

definition

let GX be TopStruct ;
let A, B be Subset of GX;

pred A,B are_separated means :: 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 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 by PRE_TOPC:22;

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, K1, L, 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 :: 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 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 A, C 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 A, C 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 b₁ being Subset of GX st b₁ = {x} holds
b₁ 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 :: 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 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 b₁ being Subset of GX st b₁ is a_component holds
b₁ is connected ;

end;

registration

let GX be non empty TopSpace;

cluster a_component -> non empty for Element of K10( the carrier of GX);

coherence
for b₁ being Subset of GX st b₁ is a_component holds
not b₁ 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 b₁ being Subset of GX st b₁ is a_component holds
b₁ 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 :: CONNSP_1:def 6
ex B1 being Subset of (GX | A) st
( B1 = B & B1 is a_component );

end;

:: deftheorem 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 b₁ 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 = b₁ )

proof end;

uniqueness
for b₁, b₂ 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 = b₁ ) & 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 = b₂ ) holds
b₁ = b₂

proof end;

end;

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

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;

registration

let T be TopStruct ;

cluster empty for Element of K10( the carrier of T);

existence
ex b₁ being Subset of T st b₁ is empty

proof end;

end;

registration

let T be TopStruct ;

cluster empty -> connected for Element of K10( the carrier of T);

coherence
for b₁ being Subset of T st b₁ is empty holds
b₁ 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 ) by Th44;

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