let a, b be Real; for X being Subset of
for V being Subset of st V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace a,b)
let X be Subset of ; for V being Subset of st V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace a,b)
let V be Subset of ; ( V = X & X is open implies V in Family_open_set (Closed-Interval-MSpace a,b) )
assume A1:
V = X
; ( not X is open or V in Family_open_set (Closed-Interval-MSpace a,b) )
assume A2:
X is open
; V in Family_open_set (Closed-Interval-MSpace a,b)
for x being Element of st x in V holds
ex r being Real st
( r > 0 & Ball x,r c= V )
proof
let x be
Element of ;
( x in V implies ex r being Real st
( r > 0 & Ball x,r c= V ) )
assume A3:
x in V
;
ex r being Real st
( r > 0 & Ball x,r c= V )
then reconsider r =
x as
Real by A1;
consider N being
Neighbourhood of
r such that A4:
N c= X
by A1, A2, A3, RCOMP_1:39;
consider g being
real number such that A5:
0 < g
and A6:
N = ].(r - g),(r + g).[
by RCOMP_1:def 7;
reconsider g =
g as
Real by XREAL_0:def 1;
A7:
Ball x,
g c= N
proof
let aa be
set ;
TARSKI:def 3 ( not aa in Ball x,g or aa in N )
assume
aa in Ball x,
g
;
aa in N
then
aa in { q where q is Element of : dist x,q < g }
by METRIC_1:18;
then consider q being
Element of
such that A8:
q = aa
and A9:
dist x,
q < g
;
A10:
(
q in the
carrier of
(Closed-Interval-MSpace a,b) & the
carrier of
(Closed-Interval-MSpace a,b) c= the
carrier of
RealSpace )
by TOPMETR:def 1;
then reconsider a' =
aa as
Real by A8, METRIC_1:def 14;
reconsider x1 =
x,
q1 =
q as
Element of
REAL by A1, A3, A10, METRIC_1:def 14;
dist x,
q =
the
distance of
(Closed-Interval-MSpace a,b) . x,
q
by METRIC_1:def 1
.=
real_dist . x,
q
by METRIC_1:def 14, TOPMETR:def 1
;
then
real_dist . q1,
x1 < g
by A9, METRIC_1:10;
then
abs (a' - r) < g
by A8, METRIC_1:def 13;
hence
aa in N
by A6, RCOMP_1:8;
verum
end;
N c= Ball x,
g
proof
let aa be
set ;
TARSKI:def 3 ( not aa in N or aa in Ball x,g )
assume A11:
aa in N
;
aa in Ball x,g
then reconsider a' =
aa as
Real ;
abs (a' - r) < g
by A6, A11, RCOMP_1:8;
then A12:
real_dist . a',
r < g
by METRIC_1:def 13;
aa in X
by A4, A11;
then reconsider a'' =
aa,
r' =
r as
Element of
by A1;
dist r',
a'' =
the
distance of
(Closed-Interval-MSpace a,b) . r',
a''
by METRIC_1:def 1
.=
real_dist . r',
a''
by METRIC_1:def 14, TOPMETR:def 1
;
then
dist r',
a'' < g
by A12, METRIC_1:10;
hence
aa in Ball x,
g
by METRIC_1:12;
verum
end;
then
N = Ball x,
g
by A7, XBOOLE_0:def 10;
hence
ex
r being
Real st
(
r > 0 &
Ball x,
r c= V )
by A1, A4, A5;
verum
end;
hence
V in Family_open_set (Closed-Interval-MSpace a,b)
by PCOMPS_1:def 5; verum