let n be Nat; for B being non empty Subset of (TOP-REAL n) st B is open holds
(TOP-REAL n) | B is locally_connected
let B be non empty Subset of (TOP-REAL n); ( B is open implies (TOP-REAL n) | B is locally_connected )
A1:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
assume A2:
B is open
; (TOP-REAL n) | B is locally_connected
for A being non empty Subset of ((TOP-REAL n) | B)
for C being Subset of ((TOP-REAL n) | B) st A is open & C is_a_component_of A holds
C is open
proof
let A be non
empty Subset of
((TOP-REAL n) | B);
for C being Subset of ((TOP-REAL n) | B) st A is open & C is_a_component_of A holds
C is open let C be
Subset of
((TOP-REAL n) | B);
( A is open & C is_a_component_of A implies C is open )
assume that A3:
A is
open
and A4:
C is_a_component_of A
;
C is open
consider C1 being
Subset of
(((TOP-REAL n) | B) | A) such that A5:
C1 = C
and A6:
C1 is
a_component
by A4, CONNSP_1:def 6;
C1 c= [#] (((TOP-REAL n) | B) | A)
;
then A7:
C1 c= A
by PRE_TOPC:def 5;
A c= the
carrier of
((TOP-REAL n) | B)
;
then
A c= B
by PRE_TOPC:8;
then
C c= B
by A5, A7;
then reconsider C0 =
C as
Subset of
(TOP-REAL n) by XBOOLE_1:1;
reconsider CC =
C0 as
Subset of
(TopSpaceMetr (Euclid n)) by A1;
for
p being
Point of
(Euclid n) st
p in C0 holds
ex
r being
Real st
(
r > 0 &
Ball (
p,
r)
c= C0 )
proof
consider A0 being
Subset of
(TOP-REAL n) such that A8:
A0 is
open
and A9:
A0 /\ ([#] ((TOP-REAL n) | B)) = A
by A3, TOPS_2:24;
A10:
A0 /\ B = A
by A9, PRE_TOPC:def 5;
A11:
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider AA =
A0 /\ B as
Subset of
(TopSpaceMetr (Euclid n)) ;
let p be
Point of
(Euclid n);
( p in C0 implies ex r being Real st
( r > 0 & Ball (p,r) c= C0 ) )
assume A12:
p in C0
;
ex r being Real st
( r > 0 & Ball (p,r) c= C0 )
AA is
open
by A2, A8, A11, PRE_TOPC:30;
then consider r1 being
Real such that A13:
r1 > 0
and A14:
Ball (
p,
r1)
c= AA
by A5, A7, A12, A10, TOPMETR:15;
reconsider r1 =
r1 as
Real ;
A15:
Ball (
p,
r1)
c= A
by A9, A14, PRE_TOPC:def 5;
then reconsider BL2 =
Ball (
p,
r1) as
Subset of
((TOP-REAL n) | B) by XBOOLE_1:1;
Ball (
p,
r1)
c= [#] (((TOP-REAL n) | B) | A)
by A15, PRE_TOPC:def 5;
then reconsider BL =
Ball (
p,
r1) as
Subset of
(((TOP-REAL n) | B) | A) ;
reconsider BL =
BL as
Subset of
(((TOP-REAL n) | B) | A) ;
reconsider BL2 =
BL2 as
Subset of
((TOP-REAL n) | B) ;
reconsider BL1 =
Ball (
p,
r1) as
Subset of
(TOP-REAL n) by TOPREAL3:8;
reconsider BL1 =
BL1 as
Subset of
(TOP-REAL n) ;
hence
ex
r being
Real st
(
r > 0 &
Ball (
p,
r)
c= C0 )
by A13;
verum
end;
then
CC is
open
by TOPMETR:15;
then A18:
(
[#] ((TOP-REAL n) | B) = B &
C0 is
open )
by A1, PRE_TOPC:30, PRE_TOPC:def 5;
C c= the
carrier of
((TOP-REAL n) | B)
;
then
C c= B
by PRE_TOPC:8;
then
C0 /\ B = C
by XBOOLE_1:28;
hence
C is
open
by A18, TOPS_2:24;
verum
end;
hence
(TOP-REAL n) | B is locally_connected
by CONNSP_2:18; verum