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