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