let X be 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 )
let x be Point of X; ( 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 )
thus
( X is_locally_connected_in x implies 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 )
( ( 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 ) implies X is_locally_connected_in x )proof
assume A1:
X is_locally_connected_in x
;
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
let V,
S be
Subset of
X;
( V is a_neighborhood of x & S is_a_component_of V & x in S implies S is a_neighborhood of x )
assume that A2:
V is
a_neighborhood of
x
and A3:
S is_a_component_of V
and A4:
x in S
;
S is a_neighborhood of x
reconsider V9 =
V as non
empty Subset of
X by A2, Th4;
consider S1 being
Subset of
(X | V) such that A5:
S1 = S
and A6:
S1 is
a_component
by A3, CONNSP_1:def 6;
consider V1 being
Subset of
X such that A7:
V1 is
a_neighborhood of
x
and A8:
V1 is
connected
and A9:
V1 c= V
by A1, A2;
V1 c= [#] (X | V)
by A9, PRE_TOPC:def 5;
then reconsider V2 =
V1 as
Subset of
(X | V) ;
A10:
x in Int V1
by A7, Def1;
V2 is
connected
by A8, CONNSP_1:23;
then
(
V2 misses S1 or
V2 c= S1 )
by A6, CONNSP_1:36;
then A11:
(
V2 /\ S1 = {} (X | V9) or
V2 c= S1 )
by XBOOLE_0:def 7;
x in V2
by A7, Th4;
then
Int V1 c= Int S
by A4, A5, A11, TOPS_1:19, XBOOLE_0:def 4;
hence
S is
a_neighborhood of
x
by A10, Def1;
verum
end;
assume A12:
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
; X is_locally_connected_in x
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 )
hence
X is_locally_connected_in x
; verum