let X be Subset of COMPLEX; :: thesis: for z0 being Element of COMPLEX
for r being Real st X = { y where y is Complex : |.(y - z0).| < r } holds
X is open
let z0 be Element of COMPLEX ; :: thesis: for r being Real st X = { y where y is Complex : |.(y - z0).| < r } holds
X is open
let r be Real; :: thesis: ( X = { y where y is Complex : |.(y - z0).| < r } implies X is open )
reconsider X0 = X as Subset of COMPLEX ;
assume A1: X = { y where y is Complex : |.(y - z0).| < r } ; :: thesis: X is open
for x being Complex st x in X0 holds
ex N being Neighbourhood of x st N c= X0
proof
let x be Complex; :: thesis: ( x in X0 implies ex N being Neighbourhood of x st N c= X0 )
reconsider r1 = (r - |.(x - z0).|) / 2 as Real ;
set N = { y where y is Complex : |.(y - x).| < r1 } ;
assume x in X0 ; :: thesis: ex N being Neighbourhood of x st N c= X0
then ex y being Complex st
( x = y & |.(y - z0).| < r ) by A1;
then A2: r - |.(x - z0).| > 0 by XREAL_1:50;
then reconsider N = { y where y is Complex : |.(y - x).| < r1 } as Neighbourhood of x by Th6;
r1 < r - |.(x - z0).| by A2, XREAL_1:216;
then A3: r1 + |.(x - z0).| < (r - |.(x - z0).|) + |.(x - z0).| by XREAL_1:8;
take N ; :: thesis: N c= X0
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in N or z in X0 )
assume z in N ; :: thesis: z in X0
then consider y1 being Complex such that
A4: z = y1 and
A5: |.(y1 - x).| < r1 ;
|.(y1 - x).| + |.(x - z0).| < r1 + |.(x - z0).| by A5, XREAL_1:8;
then ( |.(y1 - z0).| <= |.(y1 - x).| + |.(x - z0).| & |.(y1 - x).| + |.(x - z0).| < r ) by A3, COMPLEX1:63, XXREAL_0:2;
then |.(y1 - z0).| < r by XXREAL_0:2;
hence z in X0 by A1, A4; :: thesis: verum
end;
hence X is open by Th11; :: thesis: verum