let X be Subset of REAL ; :: thesis: ( X is open implies X in Family_open_set RealSpace )
assume A1:
X is open
; :: thesis: X in Family_open_set RealSpace
A2:
for x being Element of RealSpace st x in X holds
ex r being Real st
( r > 0 & Ball x,r c= X )
proof
let x be
Element of
RealSpace ;
:: thesis: ( x in X implies ex r being Real st
( r > 0 & Ball x,r c= X ) )
assume A3:
x in X
;
:: thesis: ex r being Real st
( r > 0 & Ball x,r c= X )
reconsider r =
x as
Real by METRIC_1:def 14;
consider N being
Neighbourhood of
r such that A4:
N c= X
by A1, 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 a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in N or a in Ball x,g )
assume A6:
a in N
;
:: thesis: a in Ball x,g
then reconsider a' =
a as
Real ;
a' is
Element of
REAL
;
then reconsider a'' =
a as
Element of
RealSpace by METRIC_1:def 14;
reconsider r' =
r as
Element of
RealSpace ;
reconsider a1 =
a',
r1 =
r' as
Element of
REAL ;
A7:
dist r',
a'' = real_dist . r,
a'
by METRIC_1:def 1, METRIC_1:def 14;
abs (a' - r) < g
by A5, A6, RCOMP_1:8;
then
real_dist . a',
r < g
by METRIC_1:def 13;
then
real_dist . r1,
a1 < g
by METRIC_1:10;
hence
a in Ball x,
g
by A7, METRIC_1:12;
:: thesis: verum
end;
thus
Ball x,
g c= N
:: thesis: verumproof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in Ball x,g or a in N )
assume
a in Ball x,
g
;
:: thesis: a in N
then
a in { q where q is Element of RealSpace : dist x,q < g }
by METRIC_1:18;
then consider q being
Element of
RealSpace such that A8:
(
q = a &
dist x,
q < g )
;
reconsider a' =
a as
Real by A8, METRIC_1:def 14;
reconsider x1 =
x,
q1 =
q as
Element of
REAL by METRIC_1:def 14;
real_dist . q1,
x1 < g
by A8, METRIC_1:def 1, METRIC_1:def 14;
then
abs (a' - r) < g
by A8, METRIC_1:def 13;
hence
a in N
by A5, RCOMP_1:8;
:: thesis: verum
end;
end;
hence
ex
r being
Real st
(
r > 0 &
Ball x,
r c= X )
by A4, A5;
:: thesis: verum
end;
reconsider V = X as Subset of RealSpace by METRIC_1:def 14;
V in Family_open_set RealSpace
by A2, PCOMPS_1:def 5;
hence
X in Family_open_set RealSpace
; :: thesis: verum