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

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

:: 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 :: CONNSP_1:1

canceled;

theorem Th2: :: CONNSP_1:2

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

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

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 )

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

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

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

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

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

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

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

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

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

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

( 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

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;
let A be Subset of GX;

attr A is connected means :Def3: :: CONNSP_1:def 3

GX | A is connected ;

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

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

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

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

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

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 )

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 )

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

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 )

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 )

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

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

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

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

for b_{1} being Subset of GX st b_{1} = {x} holds

b_{1} is connected

end;
let x be Point of GX;

cluster {x} -> connected Subset of GX;

coherence

for b

b

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

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

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 )

( 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

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 <> {}

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

:: 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 Element of K10( the carrier of GX);

coherence

for b_{1} being Subset of GX st b_{1} is a_component holds

b_{1} is connected
by Def5;

end;
cluster a_component -> connected Element of K10( the carrier of GX);

coherence

for b

b

registration

let GX be non empty TopSpace;

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

coherence

for b_{1} being Subset of GX st b_{1} is a_component holds

not b_{1} is empty

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

coherence

for b

not b

proof end;

theorem :: CONNSP_1:34

registration

let GX be TopSpace;

cluster a_component -> closed Element of K10( the carrier of GX);

coherence

for b_{1} being Subset of GX st b_{1} is a_component holds

b_{1} is closed

end;
cluster a_component -> closed Element of K10( the carrier of GX);

coherence

for b

b

proof end;

theorem :: CONNSP_1:35

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

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;

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 )

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

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

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

ex b_{1} 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_{1} )

for b_{1}, b_{2} 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_{1} ) & 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_{2} ) holds

b_{1} = b_{2}

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

( ( 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

( ( for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ) & union F = b

( ( for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ) & union F = b

b

proof end;

:: deftheorem Def7 defines Component_of CONNSP_1:def 7 :

for GX being TopStruct

for x being Point of GX

for b

( b

( ( for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ) & union F = b

theorem Th40: :: CONNSP_1:40

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

( not Component_of x is empty & Component_of x is connected )

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

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

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 )

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

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

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

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

ex b_{1} being Subset of T st b_{1} is empty

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

existence

ex b

proof end;

registration

let T be TopStruct ;

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

coherence

for b_{1} being Subset of T st b_{1} is empty holds

b_{1} is connected

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

coherence

for b

b

proof 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 #) )

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 )

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;