let X be Subset of REAL; ( X is open implies X in Family_open_set RealSpace )
reconsider V = X as Subset of RealSpace by METRIC_1:def 13;
assume A1:
X is open
; X in Family_open_set RealSpace
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;
( x in X implies ex r being Real st
( r > 0 & Ball (x,r) c= X ) )
reconsider r =
x as
Element of
REAL by METRIC_1:def 13;
assume
x in X
;
ex r being Real st
( r > 0 & Ball (x,r) c= X )
then consider N being
Neighbourhood of
r such that A2:
N c= X
by A1, RCOMP_1:18;
consider g being
Real such that A3:
0 < g
and A4:
N = ].(r - g),(r + g).[
by RCOMP_1:def 6;
reconsider g =
g as
Element of
REAL by XREAL_0:def 1;
A5:
N c= Ball (
x,
g)
proof
reconsider r9 =
r as
Element of
RealSpace ;
let a be
object ;
TARSKI:def 3 ( not a in N or a in Ball (x,g) )
assume A6:
a in N
;
a in Ball (x,g)
then reconsider a9 =
a as
Element of
REAL ;
reconsider a1 =
a9,
r1 =
r9 as
Element of
REAL ;
a9 is
Element of
REAL
;
then reconsider a99 =
a as
Element of
RealSpace by METRIC_1:def 13;
|.(a9 - r).| < g
by A4, A6, RCOMP_1:1;
then
real_dist . (
a9,
r)
< g
by METRIC_1:def 12;
then
(
dist (
r9,
a99)
= real_dist . (
r,
a9) &
real_dist . (
r1,
a1)
< g )
by METRIC_1:9, METRIC_1:def 1, METRIC_1:def 13;
hence
a in Ball (
x,
g)
by METRIC_1:11;
verum
end;
Ball (
x,
g)
c= N
proof
let a be
object ;
TARSKI:def 3 ( not a in Ball (x,g) or a in N )
assume
a in Ball (
x,
g)
;
a in N
then
a in { q where q is Element of RealSpace : dist (x,q) < g }
by METRIC_1:17;
then consider q being
Element of
RealSpace such that A7:
q = a
and A8:
dist (
x,
q)
< g
;
reconsider a9 =
a as
Real by A7;
reconsider x1 =
x,
q1 =
q as
Element of
REAL by METRIC_1:def 13;
real_dist . (
q1,
x1)
< g
by A8, METRIC_1:def 1, METRIC_1:def 13;
then
|.(a9 - r).| < g
by A7, METRIC_1:def 12;
hence
a in N
by A4, RCOMP_1:1;
verum
end;
then
N = Ball (
x,
g)
by A5;
hence
ex
r being
Real st
(
r > 0 &
Ball (
x,
r)
c= X )
by A2, A3;
verum
end;
then
V in Family_open_set RealSpace
by PCOMPS_1:def 4;
hence
X in Family_open_set RealSpace
; verum