let a, b be Real; for X being Subset of REAL
for V being Subset of (Closed-Interval-MSpace a,b) st V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace a,b)
let X be Subset of REAL ; for V being Subset of (Closed-Interval-MSpace a,b) st V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace a,b)
let V be Subset of (Closed-Interval-MSpace a,b); ( 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 (Closed-Interval-MSpace a,b) st x in V holds
ex r being Real st
( r > 0 & Ball x,r c= V )
proof
let x be
Element of
(Closed-Interval-MSpace a,b);
( 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 (Closed-Interval-MSpace a,b) : dist x,q < g }
by METRIC_1:18;
then consider q being
Element of
(Closed-Interval-MSpace a,b) 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 a9 =
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 (a9 - 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 a9 =
aa as
Real ;
abs (a9 - r) < g
by A6, A11, RCOMP_1:8;
then A12:
real_dist . a9,
r < g
by METRIC_1:def 13;
aa in X
by A4, A11;
then reconsider a99 =
aa,
r9 =
r as
Element of
(Closed-Interval-MSpace a,b) by A1;
dist r9,
a99 =
the
distance of
(Closed-Interval-MSpace a,b) . r9,
a99
by METRIC_1:def 1
.=
real_dist . r9,
a99
by METRIC_1:def 14, TOPMETR:def 1
;
then
dist r9,
a99 < 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