Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Connected Spaces

by

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

```environ

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

begin
reserve GX for TopSpace;
reserve A, B, C for Subset of GX;
reserve TS for TopStruct;
reserve K, K1, L, L1 for Subset of TS;

::
::                         Separated sets
::

definition let GX be TopStruct, 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;
end;

canceled;

theorem :: CONNSP_1:2
K,L are_separated implies K misses L;

theorem :: CONNSP_1:3
[#]TS = K \/ L & K is closed & L is closed & K misses L
implies K,L are_separated;

theorem :: CONNSP_1:4
[#]GX = A \/ B & A is open & B is open & A misses B
implies A,B are_separated;

theorem :: CONNSP_1:5
[#]GX = A \/ B & A,B are_separated implies
A is open closed & B is open closed;

theorem :: CONNSP_1:6
for X' being SubSpace of GX, P1,Q1 being Subset of GX,
P,Q being Subset of X' st P=P1 & Q=Q1 holds
P,Q are_separated implies P1,Q1 are_separated;

theorem :: CONNSP_1:7
for X' being SubSpace of GX, P,Q being Subset of GX,
P1,Q1 being Subset of X' st P=P1 & Q=Q1 & P \/ Q c= [#](X')
holds P,Q are_separated implies P1,Q1 are_separated;

theorem :: CONNSP_1:8
K,L are_separated & K1 c= K & L1 c= L implies
K1,L1 are_separated;

theorem :: CONNSP_1:9
A,B are_separated & A,C are_separated implies A,B \/ C are_separated;

theorem :: CONNSP_1:10
(K is closed & L is closed) or (K is open & L is open)
implies K \ L,L \ K are_separated;

::
::                        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
holds A = {}GX or B = {}GX;
end;

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

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

theorem :: CONNSP_1:13
GX is connected iff for A being Subset of GX st A <> {}GX
& A <> [#]GX holds Cl A meets Cl([#]GX \ A);

theorem :: CONNSP_1:14
GX is connected iff for A being Subset of GX st A is open closed holds
A = {}GX or A = [#]GX;

theorem :: CONNSP_1:15
for GY being TopSpace
for F being map of GX,GY st F is continuous
& F.:[#]GX = [#]GY & GX is connected holds GY is connected;

::
::                          Connected Sets
::

definition let GX be TopStruct, A be Subset of GX;
attr A is connected means
:: CONNSP_1:def 3
GX|A is connected;
end;

theorem :: CONNSP_1:16
A is connected
iff for P,Q being Subset of GX st A = P \/ Q &
P,Q are_separated holds P = {}GX or Q = {}GX;

theorem :: CONNSP_1:17
A is connected & A c= B \/ C & B,C are_separated implies
A c= B or A c= C;

theorem :: CONNSP_1:18
A is connected & B is connected & not A,B are_separated
implies A \/ B is connected;

theorem :: CONNSP_1:19
C is connected & C c= A & A c= Cl C implies A is connected;

theorem :: CONNSP_1:20
A is connected implies Cl A is connected;

theorem :: CONNSP_1:21
GX is connected & A is connected & [#]GX \ A = B \/ C &
B,C are_separated implies A \/ B is connected & A \/ C is connected;

theorem :: CONNSP_1:22
[#]GX \ A = B \/ C & B,C are_separated & A is closed implies
A \/ B is closed & A \/ C is closed;

theorem :: CONNSP_1:23
C is connected & C meets A & C \ A <> {}GX implies C meets Fr A;

theorem :: CONNSP_1:24
for X' being SubSpace of GX,
A being Subset of GX,
B being Subset of X' st A = B
holds A is connected iff B is connected;

theorem :: CONNSP_1:25
A is closed & B is closed & A \/ B is connected & A /\ B is connected
implies
A is connected & B is connected;

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

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

theorem :: CONNSP_1:28
:: do poprawienia, przy poprawnej definicji "connected" !!!
[#]GX is connected iff GX is connected;

theorem :: CONNSP_1:29
for GX being non empty TopSpace
for x being Point of GX holds {x} is connected;

definition let GX be TopStruct, x,y be Point of GX;
pred x, y are_joined means
:: CONNSP_1:def 4
ex C being Subset of GX st C is connected & x in C & y in C;
end;

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

theorem :: CONNSP_1:31
(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);

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;

theorem :: CONNSP_1:33
for GX being non empty TopSpace
for x being Point of GX, 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 <> {};

::
::              Components of Topological Spaces
::

definition let GX be TopStruct, A be Subset of GX;
pred A is_a_component_of GX means
:: CONNSP_1:def 5
A is connected & for B being Subset of GX st
B is connected holds A c= B implies A = B;
end;

theorem :: CONNSP_1:34
for GX being non empty TopSpace, A being Subset of GX
st A is_a_component_of GX holds A <> {}GX;

theorem :: CONNSP_1:35
A is_a_component_of GX implies A is closed;

theorem :: CONNSP_1:36
A is_a_component_of GX & B is_a_component_of GX implies
A = B or A,B are_separated;

theorem :: CONNSP_1:37
A is_a_component_of GX & B is_a_component_of GX implies
A = B or A misses B;

theorem :: CONNSP_1:38
C is connected implies
for S being Subset of GX st S is_a_component_of GX holds
C misses S or C c= S;

definition let GX be TopStruct, 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_of GX|A;
end;

theorem :: CONNSP_1:39
GX is connected & A is connected & C is_a_component_of [#]GX \ A implies
[#]GX \ C is connected;

::
::                    A Component of a Point
::

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

reserve GX for non empty TopSpace;
reserve A, C for Subset of GX;
reserve x for Point of GX;

theorem :: CONNSP_1:40
x in skl x;

theorem :: CONNSP_1:41
skl x is connected;

theorem :: CONNSP_1:42
C is connected & skl x c= C implies C = skl x;

theorem :: CONNSP_1:43
A is_a_component_of GX iff ex x being Point of GX st A = skl x;

theorem :: CONNSP_1:44
A is_a_component_of GX & x in A implies A = skl x;

theorem :: CONNSP_1:45
A = skl x implies
for p being Point of GX st p in A holds skl p = A;

theorem :: CONNSP_1:46
for F being Subset-Family of GX st for A being Subset of GX
holds A in F iff A is_a_component_of GX
holds F is_a_cover_of GX;
```