let n be Nat; for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds
dist (x,A) > 0
let x be Element of COMPLEX n; for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds
dist (x,A) > 0
let A be Subset of (COMPLEX n); ( not x in A & A <> {} & A is closed implies dist (x,A) > 0 )
assume that
A1:
not x in A
and
A2:
A <> {}
and
A3:
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
and
A4:
dist (x,A) <= 0
; SEQ_4:def 15 contradiction
A5:
dist (x,A) = 0
by A2, A4, Th113;
now for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A )deffunc H1(
Element of
COMPLEX n)
-> Element of
REAL =
In (
|.(x - $1).|,
REAL);
deffunc H2(
Element of
COMPLEX n)
-> Real =
|.(x - $1).|;
defpred S1[
set ]
means $1
in A;
A6:
for
z being
Element of
COMPLEX n holds
H1(
z)
= H2(
z)
;
A7:
{ H1(z1) where z1 is Element of COMPLEX n : S1[z1] } = { H2(z2) where z2 is Element of COMPLEX n : S1[z2] }
from FRAENKEL:sch 5(A6);
reconsider X =
{ H1(z) where z is Element of COMPLEX n : S1[z] } as
Subset of
REAL from DOMAIN_1:sch 8();
let r be
Real;
( r > 0 implies ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) )assume A8:
r > 0
;
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A )consider z being
Element of
COMPLEX n such that A9:
z in A
by A2, SUBSET_1:4;
A10:
X is
bounded_below
A11:
|.(x - z).| in X
by A9, A7;
(
dist (
x,
A)
= lower_bound X &
0 + r = r )
by Def17, A7;
then consider r9 being
Real such that A12:
r9 in X
and A13:
r9 < r
by A5, A8, A11, A10, Def2;
consider z1 being
Element of
COMPLEX n such that A14:
(
r9 = |.(x - z1).| &
z1 in A )
by A12, A7;
take z =
z1 - x;
( |.z.| < r & x + z in A )thus
(
|.z.| < r &
x + z in A )
by A13, A14, Th79, Th103;
verum end;
hence
contradiction
by A1, A3; verum