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 ) )
reconsider A1 = A as Subset of RealSpace by TOPMETR:16, TOPMETR:def 7;
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
reconsider A1 =
A as
Subset of
R^1 ;
A1:
the
topology of
R^1 = Family_open_set RealSpace
by TOPMETR:16, TOPMETR:def 7;
assume
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 )
then A2:
A1 in the
topology of
R^1
by PRE_TOPC:def 5;
let x be
Real;
:: thesis: ( x in A implies 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;
assume
x in A
;
:: thesis: ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A )
then consider r being
Real such that A3:
r > 0
and A4:
Ball x1,
r c= A1
by A2, A1, 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 A3;
:: 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
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