:: by Yatsuka Nakamura and Andrzej Trybulec

::

:: Received February 5, 1996

:: Copyright (c) 1996 Association of Mizar Users

begin

definition

let GX be TopStruct ;

let V be Subset of GX;

func Component_of V -> Subset of GX means :Def1: :: CONNSP_3:def 1

ex F being Subset-Family of GX st

( ( for A being Subset of GX holds

( A in F iff ( A is connected & V c= 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 & V c= 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 & V c= 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 & V c= A ) ) ) & union F = b_{2} ) holds

b_{1} = b_{2}

end;
let V be Subset of GX;

func Component_of V -> Subset of GX means :Def1: :: CONNSP_3:def 1

ex F being Subset-Family of GX st

( ( for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) ) & union F = it );

existence

ex b

( ( for A being Subset of GX holds

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

proof end;

uniqueness for b

( ( for A being Subset of GX holds

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

( ( for A being Subset of GX holds

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

b

proof end;

:: deftheorem Def1 defines Component_of CONNSP_3:def 1 :

for GX being TopStruct

for V, b

( b

( ( for A being Subset of GX holds

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

theorem Th1: :: CONNSP_3:1

for GX being TopSpace

for V being Subset of GX st ex A being Subset of GX st

( A is connected & V c= A ) holds

V c= Component_of V

for V being Subset of GX st ex A being Subset of GX st

( A is connected & V c= A ) holds

V c= Component_of V

proof end;

theorem :: CONNSP_3:2

for GX being TopSpace

for V being Subset of GX st ( for A being Subset of GX holds

( not A is connected or not V c= A ) ) holds

Component_of V = {}

for V being Subset of GX st ( for A being Subset of GX holds

( not A is connected or not V c= A ) ) holds

Component_of V = {}

proof end;

theorem Th3: :: CONNSP_3:3

proof end;

theorem :: CONNSP_3:4

for GX being non empty TopSpace

for V being Subset of GX st V is connected holds

Component_of V <> {}

for V being Subset of GX st V is connected holds

Component_of V <> {}

proof end;

theorem Th5: :: CONNSP_3:5

for GX being TopSpace

for V being Subset of GX st V is connected & V <> {} holds

Component_of V is connected

for V being Subset of GX st V is connected & V <> {} holds

Component_of V is connected

proof end;

theorem Th6: :: CONNSP_3:6

for GX being non empty TopSpace

for V, C being Subset of GX st V is connected & C is connected & Component_of V c= C holds

C = Component_of V

for V, C being Subset of GX st V is connected & C is connected & Component_of V c= C holds

C = Component_of V

proof end;

theorem Th7: :: CONNSP_3:7

for GX being non empty TopSpace

for A being Subset of GX st A is a_component holds

Component_of A = A

for A being Subset of GX st A is a_component holds

Component_of A = A

proof end;

theorem Th8: :: CONNSP_3:8

for GX being non empty TopSpace

for A being Subset of GX holds

( A is a_component iff ex V being Subset of GX st

( V is connected & V <> {} & A = Component_of V ) )

for A being Subset of GX holds

( A is a_component iff ex V being Subset of GX st

( V is connected & V <> {} & A = Component_of V ) )

proof end;

theorem :: CONNSP_3:9

for GX being non empty TopSpace

for V being Subset of GX st V is connected & V <> {} holds

Component_of V is a_component by Th8;

for V being Subset of GX st V is connected & V <> {} holds

Component_of V is a_component by Th8;

theorem :: CONNSP_3:10

for GX being non empty TopSpace

for A, V being Subset of GX st A is a_component & V is connected & V c= A & V <> {} holds

A = Component_of V

for A, V being Subset of GX st A is a_component & V is connected & V c= A & V <> {} holds

A = Component_of V

proof end;

theorem Th11: :: CONNSP_3:11

for GX being non empty TopSpace

for V being Subset of GX st V is connected & V <> {} holds

Component_of (Component_of V) = Component_of V

for V being Subset of GX st V is connected & V <> {} holds

Component_of (Component_of V) = Component_of V

proof end;

theorem Th12: :: CONNSP_3:12

for GX being non empty TopSpace

for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds

Component_of A = Component_of B

for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds

Component_of A = Component_of B

proof end;

theorem Th13: :: CONNSP_3:13

for GX being non empty TopSpace

for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds

B c= Component_of A

for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds

B c= Component_of A

proof end;

theorem Th14: :: CONNSP_3:14

for GX being non empty TopSpace

for A, B being Subset of GX st A is connected & A \/ B is connected & A <> {} holds

A \/ B c= Component_of A

for A, B being Subset of GX st A is connected & A \/ B is connected & A <> {} holds

A \/ B c= Component_of A

proof end;

theorem Th15: :: CONNSP_3:15

for GX being non empty TopSpace

for A being Subset of GX

for p being Point of GX st A is connected & p in A holds

Component_of p = Component_of A

for A being Subset of GX

for p being Point of GX st A is connected & p in A holds

Component_of p = Component_of A

proof end;

theorem :: CONNSP_3:16

for GX being non empty TopSpace

for A, B being Subset of GX st A is connected & B is connected & A meets B holds

( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A )

for A, B being Subset of GX st A is connected & B is connected & A meets B holds

( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A )

proof end;

theorem :: CONNSP_3:17

for GX being non empty TopSpace

for A being Subset of GX st A is connected & A <> {} holds

Cl A c= Component_of A

for A being Subset of GX st A is connected & A <> {} holds

Cl A c= Component_of A

proof end;

theorem :: CONNSP_3:18

for GX being non empty TopSpace

for A, B being Subset of GX st A is a_component & B is connected & B <> {} & A misses B holds

A misses Component_of B

for A, B being Subset of GX st A is a_component & B is connected & B <> {} & A misses B holds

A misses Component_of B

proof end;

begin

Lm1: now

let GX be TopStruct ; :: thesis: ex F being Subset-Family of GX st

( ( for B being Subset of GX st B in F holds

B is a_component ) & {} GX = union F )

reconsider S = {} as Subset-Family of GX by XBOOLE_1:2;

for B being Subset of GX st B in S holds

B is a_component ;

hence ex F being Subset-Family of GX st

( ( for B being Subset of GX st B in F holds

B is a_component ) & {} GX = union F ) by ZFMISC_1:2; :: thesis: verum

end;
( ( for B being Subset of GX st B in F holds

B is a_component ) & {} GX = union F )

reconsider S = {} as Subset-Family of GX by XBOOLE_1:2;

for B being Subset of GX st B in S holds

B is a_component ;

hence ex F being Subset-Family of GX st

( ( for B being Subset of GX st B in F holds

B is a_component ) & {} GX = union F ) by ZFMISC_1:2; :: thesis: verum

definition

let GX be TopStruct ;

mode a_union_of_components of GX -> Subset of GX means :Def2: :: CONNSP_3:def 2

ex F being Subset-Family of GX st

( ( for B being Subset of GX st B in F holds

B is a_component ) & it = union F );

existence

ex b_{1} being Subset of GX ex F being Subset-Family of GX st

( ( for B being Subset of GX st B in F holds

B is a_component ) & b_{1} = union F )

end;
mode a_union_of_components of GX -> Subset of GX means :Def2: :: CONNSP_3:def 2

ex F being Subset-Family of GX st

( ( for B being Subset of GX st B in F holds

B is a_component ) & it = union F );

existence

ex b

( ( for B being Subset of GX st B in F holds

B is a_component ) & b

proof end;

:: deftheorem Def2 defines a_union_of_components CONNSP_3:def 2 :

for GX being TopStruct

for b

( b

( ( for B being Subset of GX st B in F holds

B is a_component ) & b

theorem Th19: :: CONNSP_3:19

proof end;

theorem Th20: :: CONNSP_3:20

for GX being non empty TopSpace

for A being Subset of GX st A = the carrier of GX holds

A is a_union_of_components of GX

for A being Subset of GX st A = the carrier of GX holds

A is a_union_of_components of GX

proof end;

theorem Th21: :: CONNSP_3:21

for GX being non empty TopSpace

for A being Subset of GX

for p being Point of GX st p in A & A is a_union_of_components of GX holds

Component_of p c= A

for A being Subset of GX

for p being Point of GX st p in A & A is a_union_of_components of GX holds

Component_of p c= A

proof end;

theorem :: CONNSP_3:22

for GX being non empty TopSpace

for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds

( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX )

for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds

( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX )

proof end;

theorem :: CONNSP_3:23

for GX being non empty TopSpace

for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds

A is a_union_of_components of GX ) holds

union Fu is a_union_of_components of GX

for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds

A is a_union_of_components of GX ) holds

union Fu is a_union_of_components of GX

proof end;

theorem :: CONNSP_3:24

for GX being non empty TopSpace

for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds

A is a_union_of_components of GX ) holds

meet Fu is a_union_of_components of GX

for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds

A is a_union_of_components of GX ) holds

meet Fu is a_union_of_components of GX

proof end;

theorem :: CONNSP_3:25

for GX being non empty TopSpace

for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds

A \ B is a_union_of_components of GX

for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds

A \ B is a_union_of_components of GX

proof end;

begin

definition

let GX be TopStruct ;

let B be Subset of GX;

let p be Point of GX;

assume A1: p in B ;

func Down (p,B) -> Point of (GX | B) equals :Def3: :: CONNSP_3:def 3

p;

coherence

p is Point of (GX | B)

end;
let B be Subset of GX;

let p be Point of GX;

assume A1: p in B ;

func Down (p,B) -> Point of (GX | B) equals :Def3: :: CONNSP_3:def 3

p;

coherence

p is Point of (GX | B)

proof end;

:: deftheorem Def3 defines Down CONNSP_3:def 3 :

for GX being TopStruct

for B being Subset of GX

for p being Point of GX st p in B holds

Down (p,B) = p;

definition

let GX be TopStruct ;

let B be Subset of GX;

let p be Point of (GX | B);

assume A1: B <> {} ;

func Up p -> Point of GX equals :: CONNSP_3:def 4

p;

coherence

p is Point of GX

end;
let B be Subset of GX;

let p be Point of (GX | B);

assume A1: B <> {} ;

func Up p -> Point of GX equals :: CONNSP_3:def 4

p;

coherence

p is Point of GX

proof end;

:: deftheorem defines Up CONNSP_3:def 4 :

for GX being TopStruct

for B being Subset of GX

for p being Point of (GX | B) st B <> {} holds

Up p = p;

definition

let GX be TopStruct ;

let V, B be Subset of GX;

func Down (V,B) -> Subset of (GX | B) equals :: CONNSP_3:def 5

V /\ B;

coherence

V /\ B is Subset of (GX | B)

end;
let V, B be Subset of GX;

func Down (V,B) -> Subset of (GX | B) equals :: CONNSP_3:def 5

V /\ B;

coherence

V /\ B is Subset of (GX | B)

proof end;

:: deftheorem defines Down CONNSP_3:def 5 :

for GX being TopStruct

for V, B being Subset of GX holds Down (V,B) = V /\ B;

definition

let GX be TopStruct ;

let B be Subset of GX;

let V be Subset of (GX | B);

func Up V -> Subset of GX equals :: CONNSP_3:def 6

V;

coherence

V is Subset of GX

end;
let B be Subset of GX;

let V be Subset of (GX | B);

func Up V -> Subset of GX equals :: CONNSP_3:def 6

V;

coherence

V is Subset of GX

proof end;

:: deftheorem defines Up CONNSP_3:def 6 :

for GX being TopStruct

for B being Subset of GX

for V being Subset of (GX | B) holds Up V = V;

definition

let GX be TopStruct ;

let B be Subset of GX;

let p be Point of GX;

assume A1: p in B ;

func Component_of (p,B) -> Subset of GX means :Def7: :: CONNSP_3:def 7

for q being Point of (GX | B) st q = p holds

it = Component_of q;

existence

ex b_{1} being Subset of GX st

for q being Point of (GX | B) st q = p holds

b_{1} = Component_of q

for b_{1}, b_{2} being Subset of GX st ( for q being Point of (GX | B) st q = p holds

b_{1} = Component_of q ) & ( for q being Point of (GX | B) st q = p holds

b_{2} = Component_of q ) holds

b_{1} = b_{2}

end;
let B be Subset of GX;

let p be Point of GX;

assume A1: p in B ;

func Component_of (p,B) -> Subset of GX means :Def7: :: CONNSP_3:def 7

for q being Point of (GX | B) st q = p holds

it = Component_of q;

existence

ex b

for q being Point of (GX | B) st q = p holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines Component_of CONNSP_3:def 7 :

for GX being TopStruct

for B being Subset of GX

for p being Point of GX st p in B holds

for b

( b

b

theorem :: CONNSP_3:26

for GX being non empty TopSpace

for B being Subset of GX

for p being Point of GX st p in B holds

p in Component_of (p,B)

for B being Subset of GX

for p being Point of GX st p in B holds

p in Component_of (p,B)

proof end;

theorem Th27: :: CONNSP_3:27

for GX being non empty TopSpace

for B being Subset of GX

for p being Point of GX st p in B holds

Component_of (p,B) = Component_of (Down (p,B))

for B being Subset of GX

for p being Point of GX st p in B holds

Component_of (p,B) = Component_of (Down (p,B))

proof end;

theorem :: CONNSP_3:28

canceled;

theorem :: CONNSP_3:29

proof end;

theorem Th30: :: CONNSP_3:30

for GX being non empty TopSpace

for V, B being Subset of GX st V c= B holds

Cl (Down (V,B)) = (Cl V) /\ B

for V, B being Subset of GX st V c= B holds

Cl (Down (V,B)) = (Cl V) /\ B

proof end;

theorem :: CONNSP_3:31

for GX being non empty TopSpace

for B being Subset of GX

for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B

for B being Subset of GX

for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B

proof end;

theorem :: CONNSP_3:32

proof end;

theorem :: CONNSP_3:33

for GX being non empty TopSpace

for B being Subset of GX

for V being Subset of (GX | B) st V c= B holds

Down ((Up V),B) = V by XBOOLE_1:28;

for B being Subset of GX

for V being Subset of (GX | B) st V c= B holds

Down ((Up V),B) = V by XBOOLE_1:28;

theorem :: CONNSP_3:34

canceled;

theorem :: CONNSP_3:35

for GX being non empty TopSpace

for B being Subset of GX

for p being Point of GX st p in B holds

Component_of (p,B) is connected

for B being Subset of GX

for p being Point of GX st p in B holds

Component_of (p,B) is connected

proof end;

registration

let T be non empty TopSpace;

cluster non empty a_union_of_components of T;

existence

not for b_{1} being a_union_of_components of T holds b_{1} is empty

end;
cluster non empty a_union_of_components of T;

existence

not for b

proof end;

theorem :: CONNSP_3:36

for T being non empty TopSpace

for A being non empty a_union_of_components of T st A is connected holds

A is a_component

for A being non empty a_union_of_components of T st A is connected holds

A is a_component

proof end;