let A be Subset of R^1 ; :: thesis: ( A is open iff for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
thus
( A is open implies for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
:: thesis: ( ( for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) ) implies A is open )proof
assume A1:
A is
open
;
:: thesis: for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A )
let x be
Real;
:: thesis: ( x in A implies ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
assume A2:
x in A
;
:: thesis: ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A )
reconsider x1 =
x as
Element of
REAL ;
reconsider x1 =
x1 as
Element of
RealSpace by METRIC_1:def 14;
reconsider A1 =
A as
Subset of
R^1 ;
A3:
A1 in the
topology of
R^1
by A1, PRE_TOPC:def 5;
the
topology of
R^1 = Family_open_set RealSpace
by TOPMETR:16, TOPMETR:def 7;
then consider r being
Real such that A4:
(
r > 0 &
Ball x1,
r c= A1 )
by A2, A3, PCOMPS_1:def 5;
].(x - r),(x + r).[ c= A1
by A4, Th7;
hence
ex
r being
Real st
(
r > 0 &
].(x - r),(x + r).[ c= A )
by A4;
:: thesis: verum
end;
assume A5:
for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A )
; :: thesis: A is open
reconsider A1 = A as Subset of RealSpace by TOPMETR:16, TOPMETR:def 7;
for x being Element of RealSpace st x in A1 holds
ex r being Real st
( r > 0 & Ball x,r c= A1 )
then A8:
A1 in Family_open_set RealSpace
by PCOMPS_1:def 5;
the topology of R^1 = Family_open_set RealSpace
by TOPMETR:16, TOPMETR:def 7;
hence
A is open
by A8, PRE_TOPC:def 5; :: thesis: verum