let X be 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) ) )
let x be Point of X; ( 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) ) )
A1:
( X is_locally_connected_in x implies 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) ) )
( ( 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) ) ) implies X is_locally_connected_in x )
proof
assume A7:
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) )
;
X is_locally_connected_in x
for
U1 being
Subset of
X st
U1 is
a_neighborhood of
x holds
ex
V1 being
Subset of
X st
(
V1 is
a_neighborhood of
x &
V1 is
connected &
V1 c= U1 )
proof
let U1 be
Subset of
X;
( U1 is a_neighborhood of x implies ex V1 being Subset of X st
( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 ) )
assume
U1 is
a_neighborhood of
x
;
ex V1 being Subset of X st
( V1 is a_neighborhood of x & V1 is connected & V1 c= U1 )
then consider V being non
empty Subset of
X such that A8:
V is
a_neighborhood of
x
and A9:
V is
open
and A10:
V c= U1
by Th5;
consider x1 being
Point of
(X | V) such that A11:
x1 = x
and A12:
x in Int (Component_of x1)
by A7, A8, A9, Th4;
set S1 =
Component_of x1;
reconsider S =
Component_of x1 as
Subset of
X by PRE_TOPC:11;
take
S
;
( S is a_neighborhood of x & S is connected & S c= U1 )
Component_of x1 c= [#] (X | V)
;
then A13:
(
Component_of x1 is
connected &
S c= V )
by PRE_TOPC:def 5;
Component_of x1 is
a_neighborhood of
x1
by A11, A12, Def1;
hence
(
S is
a_neighborhood of
x &
S is
connected &
S c= U1 )
by A9, A10, A11, A13, Th9, CONNSP_1:23;
verum
end;
hence
X is_locally_connected_in x
;
verum
end;
hence
( 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) ) )
by A1; verum