:: Locally Connected Spaces
:: by Beata Padlewska
::
:: Received September 5, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
::
:: A NEIGHBORHOOD OF A POINT
::
definition
let
X
be non
empty
TopSpace
;
let
x
be
Point
of
X
;
mode
a_neighborhood
of
x
->
Subset
of
X
means
:
Def1
:
:: CONNSP_2:def 1
x
in
Int
it
;
existence
ex
b
1
being
Subset
of
X
st
x
in
Int
b
1
proof
end;
end;
::
deftheorem
Def1
defines
a_neighborhood
CONNSP_2:def 1 :
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
for
b
3
being
Subset
of
X
holds
(
b
3
is
a_neighborhood
of
x
iff
x
in
Int
b
3
);
::
:: A NEIGHBORHOOD OF A SET
::
definition
let
X
be
TopSpace
;
let
A
be
Subset
of
X
;
mode
a_neighborhood
of
A
->
Subset
of
X
means
:
Def2
:
:: CONNSP_2:def 2
A
c=
Int
it
;
existence
ex
b
1
being
Subset
of
X
st
A
c=
Int
b
1
proof
end;
end;
::
deftheorem
Def2
defines
a_neighborhood
CONNSP_2:def 2 :
for
X
being
TopSpace
for
A
,
b
3
being
Subset
of
X
holds
(
b
3
is
a_neighborhood
of
A
iff
A
c=
Int
b
3
);
theorem
:: CONNSP_2:1
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
for
A
,
B
being
Subset
of
X
st
A
is
a_neighborhood
of
x
&
B
is
a_neighborhood
of
x
holds
A
\/
B
is
a_neighborhood
of
x
proof
end;
theorem
:: CONNSP_2:2
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
for
A
,
B
being
Subset
of
X
holds
( (
A
is
a_neighborhood
of
x
&
B
is
a_neighborhood
of
x
) iff
A
/\
B
is
a_neighborhood
of
x
)
proof
end;
theorem
Th3
:
:: CONNSP_2:3
for
X
being non
empty
TopSpace
for
U1
being
Subset
of
X
for
x
being
Point
of
X
st
U1
is
open
&
x
in
U1
holds
U1
is
a_neighborhood
of
x
proof
end;
theorem
Th4
:
:: CONNSP_2:4
for
X
being non
empty
TopSpace
for
U1
being
Subset
of
X
for
x
being
Point
of
X
st
U1
is
a_neighborhood
of
x
holds
x
in
U1
proof
end;
theorem
Th5
:
:: CONNSP_2:5
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
for
U1
being
Subset
of
X
st
U1
is
a_neighborhood
of
x
holds
ex
V
being non
empty
Subset
of
X
st
(
V
is
a_neighborhood
of
x
&
V
is
open
&
V
c=
U1
)
proof
end;
theorem
Th6
:
:: CONNSP_2:6
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
for
U1
being
Subset
of
X
holds
(
U1
is
a_neighborhood
of
x
iff ex
V
being
Subset
of
X
st
(
V
is
open
&
V
c=
U1
&
x
in
V
) )
proof
end;
theorem
:: CONNSP_2:7
for
X
being non
empty
TopSpace
for
U1
being
Subset
of
X
holds
(
U1
is
open
iff for
x
being
Point
of
X
st
x
in
U1
holds
ex
A
being
Subset
of
X
st
(
A
is
a_neighborhood
of
x
&
A
c=
U1
) )
proof
end;
theorem
:: CONNSP_2:8
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
for
V
being
Subset
of
X
holds
(
V
is
a_neighborhood
of
{
x
}
iff
V
is
a_neighborhood
of
x
)
proof
end;
theorem
Th9
:
:: CONNSP_2:9
for
X
being non
empty
TopSpace
for
B
being non
empty
Subset
of
X
for
x
being
Point
of
(
X
|
B
)
for
A
being
Subset
of
(
X
|
B
)
for
A1
being
Subset
of
X
for
x1
being
Point
of
X
st
B
is
open
&
A
is
a_neighborhood
of
x
&
A
=
A1
&
x
=
x1
holds
A1
is
a_neighborhood
of
x1
proof
end;
Lm1
:
for
X
being non
empty
TopSpace
for
X1
being
SubSpace
of
X
for
A
being
Subset
of
X
for
A1
being
Subset
of
X1
st
A
=
A1
holds
(
Int
A
)
/\
(
[#]
X1
)
c=
Int
A1
proof
end;
theorem
Th10
:
:: CONNSP_2:10
for
X
being non
empty
TopSpace
for
B
being non
empty
Subset
of
X
for
x
being
Point
of
(
X
|
B
)
for
A
being
Subset
of
(
X
|
B
)
for
A1
being
Subset
of
X
for
x1
being
Point
of
X
st
A1
is
a_neighborhood
of
x1
&
A
=
A1
&
x
=
x1
holds
A
is
a_neighborhood
of
x
proof
end;
theorem
Th11
:
:: CONNSP_2:11
for
X
being non
empty
TopSpace
for
A
,
B
being
Subset
of
X
st
A
is
a_component
&
A
c=
B
holds
A
is_a_component_of
B
proof
end;
theorem
:: CONNSP_2:12
for
X
being non
empty
TopSpace
for
X1
being non
empty
SubSpace
of
X
for
x
being
Point
of
X
for
x1
being
Point
of
X1
st
x
=
x1
holds
Component_of
x1
c=
Component_of
x
proof
end;
::
:: LOCALLY CONNECTED TOPOLOGICAL SPACES
::
definition
let
X
be non
empty
TopSpace
;
let
x
be
Point
of
X
;
pred
X
is_locally_connected_in
x
means
:
Def3
:
:: CONNSP_2:def 3
for
U1
being
Subset
of
X
st
U1
is
a_neighborhood
of
x
holds
ex
V
being
Subset
of
X
st
(
V
is
a_neighborhood
of
x
&
V
is
connected
&
V
c=
U1
);
end;
::
deftheorem
Def3
defines
is_locally_connected_in
CONNSP_2:def 3 :
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
holds
(
X
is_locally_connected_in
x
iff for
U1
being
Subset
of
X
st
U1
is
a_neighborhood
of
x
holds
ex
V
being
Subset
of
X
st
(
V
is
a_neighborhood
of
x
&
V
is
connected
&
V
c=
U1
) );
definition
let
X
be non
empty
TopSpace
;
attr
X
is
locally_connected
means
:
Def4
:
:: CONNSP_2:def 4
for
x
being
Point
of
X
holds
X
is_locally_connected_in
x
;
end;
::
deftheorem
Def4
defines
locally_connected
CONNSP_2:def 4 :
for
X
being non
empty
TopSpace
holds
(
X
is
locally_connected
iff for
x
being
Point
of
X
holds
X
is_locally_connected_in
x
);
definition
let
X
be non
empty
TopSpace
;
let
A
be
Subset
of
X
;
let
x
be
Point
of
X
;
pred
A
is_locally_connected_in
x
means
:
Def5
:
:: CONNSP_2:def 5
for
B
being non
empty
Subset
of
X
st
A
=
B
holds
ex
x1
being
Point
of
(
X
|
B
)
st
(
x1
=
x
&
X
|
B
is_locally_connected_in
x1
);
end;
::
deftheorem
Def5
defines
is_locally_connected_in
CONNSP_2:def 5 :
for
X
being non
empty
TopSpace
for
A
being
Subset
of
X
for
x
being
Point
of
X
holds
(
A
is_locally_connected_in
x
iff for
B
being non
empty
Subset
of
X
st
A
=
B
holds
ex
x1
being
Point
of
(
X
|
B
)
st
(
x1
=
x
&
X
|
B
is_locally_connected_in
x1
) );
definition
let
X
be non
empty
TopSpace
;
let
A
be non
empty
Subset
of
X
;
attr
A
is
locally_connected
means
:
Def6
:
:: CONNSP_2:def 6
X
|
A
is
locally_connected
;
end;
::
deftheorem
Def6
defines
locally_connected
CONNSP_2:def 6 :
for
X
being non
empty
TopSpace
for
A
being non
empty
Subset
of
X
holds
(
A
is
locally_connected
iff
X
|
A
is
locally_connected
);
theorem
Th13
:
:: CONNSP_2:13
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
holds
(
X
is_locally_connected_in
x
iff for
V
,
S
being
Subset
of
X
st
V
is
a_neighborhood
of
x
&
S
is_a_component_of
V
&
x
in
S
holds
S
is
a_neighborhood
of
x
)
proof
end;
theorem
Th14
:
:: CONNSP_2:14
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
holds
(
X
is_locally_connected_in
x
iff for
U1
being non
empty
Subset
of
X
st
U1
is
open
&
x
in
U1
holds
ex
x1
being
Point
of
(
X
|
U1
)
st
(
x1
=
x
&
x
in
Int
(
Component_of
x1
)
) )
proof
end;
theorem
Th15
:
:: CONNSP_2:15
for
X
being non
empty
TopSpace
st
X
is
locally_connected
holds
for
S
being
Subset
of
X
st
S
is
a_component
holds
S
is
open
proof
end;
theorem
Th16
:
:: CONNSP_2:16
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
st
X
is_locally_connected_in
x
holds
for
A
being non
empty
Subset
of
X
st
A
is
open
&
x
in
A
holds
A
is_locally_connected_in
x
proof
end;
theorem
Th17
:
:: CONNSP_2:17
for
X
being non
empty
TopSpace
st
X
is
locally_connected
holds
for
A
being non
empty
Subset
of
X
st
A
is
open
holds
A
is
locally_connected
proof
end;
theorem
Th18
:
:: CONNSP_2:18
for
X
being non
empty
TopSpace
holds
(
X
is
locally_connected
iff for
A
being non
empty
Subset
of
X
for
B
being
Subset
of
X
st
A
is
open
&
B
is_a_component_of
A
holds
B
is
open
)
proof
end;
theorem
:: CONNSP_2:19
for
X
being non
empty
TopSpace
st
X
is
locally_connected
holds
for
E
being non
empty
Subset
of
X
for
C
being non
empty
Subset
of
(
X
|
E
)
st
C
is
connected
&
C
is
open
holds
ex
H
being
Subset
of
X
st
(
H
is
open
&
H
is
connected
&
C
=
E
/\
H
)
proof
end;
theorem
Th20
:
:: CONNSP_2:20
for
X
being non
empty
TopSpace
holds
(
X
is
normal
iff for
A
,
C
being
Subset
of
X
st
A
<>
{}
&
C
<>
[#]
X
&
A
c=
C
&
A
is
closed
&
C
is
open
holds
ex
G
being
Subset
of
X
st
(
G
is
open
&
A
c=
G
&
Cl
G
c=
C
) )
proof
end;
theorem
:: CONNSP_2:21
for
X
being non
empty
TopSpace
st
X
is
locally_connected
&
X
is
normal
holds
for
A
,
B
being
Subset
of
X
st
A
<>
{}
&
B
<>
{}
&
A
is
closed
&
B
is
closed
&
A
misses
B
&
A
is
connected
&
B
is
connected
holds
ex
R
,
S
being
Subset
of
X
st
(
R
is
connected
&
S
is
connected
&
R
is
open
&
S
is
open
&
A
c=
R
&
B
c=
S
&
R
misses
S
)
proof
end;
theorem
Th22
:
:: CONNSP_2:22
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
for
F
being
Subset-Family
of
X
st ( for
A
being
Subset
of
X
holds
(
A
in
F
iff (
A
is
open
&
A
is
closed
&
x
in
A
) ) ) holds
F
<>
{}
proof
end;
::
:: A QUASICOMPONENT OF A POINT
::
definition
let
X
be non
empty
TopSpace
;
let
x
be
Point
of
X
;
func
qComponent_of
x
->
Subset
of
X
means
:
Def7
:
:: CONNSP_2:def 7
ex
F
being
Subset-Family
of
X
st
( ( for
A
being
Subset
of
X
holds
(
A
in
F
iff (
A
is
open
&
A
is
closed
&
x
in
A
) ) ) &
meet
F
=
it
);
existence
ex
b
1
being
Subset
of
X
ex
F
being
Subset-Family
of
X
st
( ( for
A
being
Subset
of
X
holds
(
A
in
F
iff (
A
is
open
&
A
is
closed
&
x
in
A
) ) ) &
meet
F
=
b
1
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Subset
of
X
st ex
F
being
Subset-Family
of
X
st
( ( for
A
being
Subset
of
X
holds
(
A
in
F
iff (
A
is
open
&
A
is
closed
&
x
in
A
) ) ) &
meet
F
=
b
1
) & ex
F
being
Subset-Family
of
X
st
( ( for
A
being
Subset
of
X
holds
(
A
in
F
iff (
A
is
open
&
A
is
closed
&
x
in
A
) ) ) &
meet
F
=
b
2
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def7
defines
qComponent_of
CONNSP_2:def 7 :
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
for
b
3
being
Subset
of
X
holds
(
b
3
=
qComponent_of
x
iff ex
F
being
Subset-Family
of
X
st
( ( for
A
being
Subset
of
X
holds
(
A
in
F
iff (
A
is
open
&
A
is
closed
&
x
in
A
) ) ) &
meet
F
=
b
3
) );
theorem
:: CONNSP_2:23
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
holds
x
in
qComponent_of
x
proof
end;
theorem
:: CONNSP_2:24
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
for
A
being
Subset
of
X
st
A
is
open
&
A
is
closed
&
x
in
A
&
A
c=
qComponent_of
x
holds
A
=
qComponent_of
x
proof
end;
theorem
:: CONNSP_2:25
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
holds
qComponent_of
x
is
closed
proof
end;
theorem
:: CONNSP_2:26
for
X
being non
empty
TopSpace
for
x
being
Point
of
X
holds
Component_of
x
c=
qComponent_of
x
proof
end;
:: Moved from YELLOW_6, AG 18.02.2006
theorem
:: CONNSP_2:27
for
T
being non
empty
TopSpace
for
A
being
Subset
of
T
for
p
being
Point
of
T
holds
(
p
in
Cl
A
iff for
G
being
a_neighborhood
of
p
holds
G
meets
A
)
proof
end;
theorem
:: CONNSP_2:28
for
X
being non
empty
TopSpace
for
A
being
Subset
of
X
holds
[#]
X
is
a_neighborhood
of
A
proof
end;
theorem
:: CONNSP_2:29
for
X
being non
empty
TopSpace
for
A
being
Subset
of
X
for
Y
being
a_neighborhood
of
A
holds
A
c=
Y
proof
end;
:: A NEIGHBORHOOD OF A POINT
::