Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### Components and Unions of Components

by
Yatsuka Nakamura, and
Andrzej Trybulec

MML identifier: CONNSP_3
[ Mizar article, MML identifier index ]

```environ

vocabulary PRE_TOPC, RELAT_1, CONNSP_1, SETFAM_1, RELAT_2, TARSKI, BOOLE,
SUBSET_1, CONNSP_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1;
constructors CONNSP_1, MEMBERED;
clusters PRE_TOPC, STRUCT_0, SUBSET_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: The component of a subset in a topological space

reserve x,X,X2,Y,Y2 for set;
reserve GX for non empty TopSpace;
reserve A2,B2 for Subset of GX;
reserve B for Subset of GX;

definition let GX be TopStruct, V be Subset of GX;
func skl V -> Subset of GX means
:: 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;
end;

theorem :: CONNSP_3:1
for GX being TopSpace, V being Subset of GX st
(ex A being Subset of GX st A is connected & V c= A)
holds V c= skl V;

theorem :: CONNSP_3:2
for GX being TopSpace, V being Subset of GX st
(not ex A being Subset of GX st A is connected & V c= A)
holds skl V = {};

theorem :: CONNSP_3:3
skl {}GX = the carrier of GX;

theorem :: CONNSP_3:4
for V being Subset of GX st V is connected holds skl V <>{};

theorem :: CONNSP_3:5
for GX being TopSpace, V being Subset of GX st
V is connected & V <> {} holds skl V is connected;

theorem :: CONNSP_3:6
for V,C being Subset of GX st V is connected & C is connected
holds skl V c= C implies C = skl V;

theorem :: CONNSP_3:7
for A being Subset of GX st A is_a_component_of GX
holds skl A=A;

theorem :: CONNSP_3:8
for A being Subset of GX holds
A is_a_component_of GX iff
ex V being Subset of GX st V is connected &
V <> {} & A = skl V;

theorem :: CONNSP_3:9
for V being Subset of GX st V is connected & V<>{}
holds skl V is_a_component_of GX;

theorem :: CONNSP_3:10
for A, V be Subset of GX st
A is_a_component_of GX & V is connected & V c= A & V<>{}
holds A = skl V;

theorem :: CONNSP_3:11
for V being Subset of GX st V is connected & V<>{} holds
skl (skl V)=skl V;

theorem :: CONNSP_3:12
for A,B being Subset of GX st A is connected &
B is connected & A<>{} & A c= B
holds skl A = skl B;

theorem :: CONNSP_3:13
for A,B being Subset of GX st A is connected &
B is connected & A<>{} & A c= B
holds B c= skl A;

theorem :: CONNSP_3:14
for A being Subset of GX,B being Subset of GX st
A is connected & A \/ B is connected & A<>{}
holds A \/ B c= skl A;

theorem :: CONNSP_3:15
for A being Subset of GX, p being Point of GX
st A is connected & p in A holds
skl p=skl A;

theorem :: CONNSP_3:16
for A,B being Subset of GX st A is connected &
B is connected & A meets B
holds A \/ B c= skl A & A \/ B c= skl B & A c= skl B & B c= skl A;

theorem :: CONNSP_3:17
for A being Subset of GX st A is connected & A<>{}
holds Cl A c= skl A;

theorem :: CONNSP_3:18
for A,B being Subset of GX
st A is_a_component_of GX & B is connected & B<>{} & A misses B
holds A misses skl B;

begin

definition let GX be TopStruct;
mode a_union_of_components of GX -> Subset of GX means
:: 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_of GX) &
it = union F;
end;

theorem :: CONNSP_3:19
{}(GX) is a_union_of_components of GX;

theorem :: CONNSP_3:20
for A being Subset of GX st A=(the carrier of GX) holds
A is a_union_of_components of GX;

theorem :: CONNSP_3:21
for A being Subset of GX,p being Point of GX st p in A
& A is a_union_of_components of GX holds
skl p c= A;

theorem :: CONNSP_3:22
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;

theorem :: CONNSP_3:23
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;

theorem :: CONNSP_3:24
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;

theorem :: CONNSP_3:25
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;

begin :: Operations Down and Up

definition let GX be TopStruct, B be Subset of GX,
p be Point of GX;
assume  p in B;
func Down(p,B) -> Point of GX|B equals
:: CONNSP_3:def 3
p;
end;

definition let GX be TopStruct, B be Subset of GX,
p be Point of GX|B;
assume B<>{};
func Up(p) -> Point of GX equals
:: CONNSP_3:def 4
p;
end;

definition let GX be TopStruct, V,B be Subset of GX;
func Down(V,B) -> Subset of GX|B equals
:: CONNSP_3:def 5
V /\ B;
end;

definition let GX be TopStruct, B be Subset of GX;
let V be Subset of GX|B;
func Up(V) -> Subset of GX equals
:: CONNSP_3:def 6
V;
end;

definition let GX be TopStruct, B be Subset of GX,
p be Point of GX;
assume  p in B;
func skl(p,B) -> Subset of GX means
:: CONNSP_3:def 7
for q being Point of GX|B st q=p holds it=skl q;
end;

theorem :: CONNSP_3:26
for B being Subset of GX, p be Point of GX st p in B
holds skl(p,B)<>{};

theorem :: CONNSP_3:27
for B being Subset of GX, p be Point of GX st p in B
holds skl(p,B)=skl Down(p,B);

theorem :: CONNSP_3:28
for V,B being Subset of GX st V c= B holds Down(V,B)=V;

theorem :: CONNSP_3:29
for GX being TopSpace
for V,B being Subset of GX st V is open holds
Down(V,B) is open;

theorem :: CONNSP_3:30
for V,B being Subset of GX st V c= B holds
Cl Down(V,B) =(Cl V) /\ B;

theorem :: CONNSP_3:31
for B being Subset of GX,V being Subset of GX|
B
holds Cl V =(Cl Up(V)) /\ B;

theorem :: CONNSP_3:32
for V,B being Subset of GX st V c= B holds
Cl Down(V,B) c= Cl V;

theorem :: CONNSP_3:33
for B being Subset of GX,
V being Subset of GX|B st
V c= B holds Down(Up(V),B)=V;

theorem :: CONNSP_3:34
for GX being TopSpace
for V,B being Subset of GX,
W being Subset of GX|B st V=W & W is connected holds V is connected;

theorem :: CONNSP_3:35
for B being Subset of GX, p be Point of GX st p in B
holds skl(p,B) is connected;
```