:: Connected Spaces
:: by Beata Padlewska
::
:: Received May 6, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
::
:: Separated sets
::
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;
::
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
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
proof
end;
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
,
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
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
:
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;
::
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
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
C
,
A
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
C
,
A
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
1
being
Subset
of
GX
st
b
1
=
{
x
}
holds
b
1
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
:
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;
::
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
for
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;
registration
let
GX
be non
empty
TopSpace
;
cluster
a_component
->
non
empty
for
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
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
1
being
Subset
of
GX
st
b
1
is
a_component
holds
b
1
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
:
Def6
:
:: CONNSP_1:def 6
ex
B1
being
Subset
of
(
GX
|
A
)
st
(
B1
=
B
&
B1
is
a_component
);
end;
::
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: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
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
)
proof
end;
uniqueness
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
proof
end;
end;
::
deftheorem
Def7
defines
Component_of
CONNSP_1:def 7 :
for
GX
being
TopStruct
for
x
being
Point
of
GX
for
b
3
being
Subset
of
GX
holds
(
b
3
=
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
3
) );
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;
begin
registration
let
T
be
TopStruct
;
cluster
empty
for
Element
of
K10
( the
carrier
of
T
);
existence
ex
b
1
being
Subset
of
T
st
b
1
is
empty
proof
end;
end;
registration
let
T
be
TopStruct
;
cluster
empty
->
connected
for
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
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
)
proof
end;
:: 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;
:: Separated sets
::