let n be Element of NAT ; :: thesis: for r1 being Real
for A being Subset of (COMPLEX n) st A <> {} holds
Ball (A,r1) is open
let r1 be Real; :: thesis: for A being Subset of (COMPLEX n) st A <> {} holds
Ball (A,r1) is open
let A be Subset of (COMPLEX n); :: thesis: ( A <> {} implies Ball (A,r1) is open )
assume A1: A <> {} ; :: thesis: Ball (A,r1) is open
let x be Element of COMPLEX n; :: according to SEQ_4:def 17 :: thesis: ( x in Ball (A,r1) implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (A,r1) ) ) )
assume x in Ball (A,r1) ; :: thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (A,r1) ) )
then A2: dist (x,A) < r1 by Th90;
take r = r1 - (dist (x,A)); :: thesis: ( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (A,r1) ) )
thus 0 < r by A2, XREAL_1:52; :: thesis: for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (A,r1)
let z be Element of COMPLEX n; :: thesis: ( |.z.| < r implies x + z in Ball (A,r1) )
assume |.z.| < r ; :: thesis: x + z in Ball (A,r1)
then A3: |.z.| + (dist (x,A)) < r + (dist (x,A)) by XREAL_1:8;
dist ((x + z),A) <= |.z.| + (dist (x,A)) by A1, Th86;
then dist ((x + z),A) < r + (dist (x,A)) by A3, XXREAL_0:2;
hence x + z in Ball (A,r1) ; :: thesis: verum