let n be Nat; :: thesis: for A being Subset of (COMPLEX n) holds
( A is closed iff A ` is open )
let A be Subset of (COMPLEX n); :: thesis: ( A is closed iff A ` is open )
thus ( A is closed implies A ` is open ) :: thesis: ( A ` is open implies A is closed )
proof
assume A1: for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A ; :: according to SEQ_4:def 15 :: thesis: A ` is open
let x be Element of COMPLEX n; :: according to SEQ_4:def 14 :: thesis: ( x in A ` implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ` ) ) )
assume x in A ` ; :: thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ` ) )
then not x in A by XBOOLE_0:def 5;
then consider r being Real such that
A2: r > 0 and
A3: for z being Element of COMPLEX n st |.z.| < r holds
not x + z in A by A1;
take r ; :: thesis: ( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ` ) )
thus 0 < r by A2; :: thesis: for z being Element of COMPLEX n st |.z.| < r holds
x + z in A `
let z be Element of COMPLEX n; :: thesis: ( |.z.| < r implies x + z in A ` )
assume |.z.| < r ; :: thesis: x + z in A `
hence x + z in A ` by A3, SUBSET_1:29; :: thesis: verum
end;
assume A4: for x being Element of COMPLEX n st x in A ` holds
ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ` ) ) ; :: according to SEQ_4:def 14 :: thesis: A is closed
let x be Element of COMPLEX n; :: according to SEQ_4:def 15 :: thesis: ( ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) implies x in A )
assume A5: for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ; :: thesis: x in A
now :: thesis: for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & not x + z in A ` )
let r be Real; :: thesis: ( r > 0 implies ex z being Element of COMPLEX n st
( |.z.| < r & not x + z in A ` ) )
assume r > 0 ; :: thesis: ex z being Element of COMPLEX n st
( |.z.| < r & not x + z in A ` )
then consider z being Element of COMPLEX n such that
A6: ( |.z.| < r & x + z in A ) by A5;
take z = z; :: thesis: ( |.z.| < r & not x + z in A ` )
thus ( |.z.| < r & not x + z in A ` ) by A6, XBOOLE_0:def 5; :: thesis: verum
end;
then not x in A ` by A4;
hence x in A by SUBSET_1:29; :: thesis: verum