let n be Nat; for x, z being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist ((x + z),A) <= (dist (x,A)) + |.z.|
let x, z be Element of COMPLEX n; for A being Subset of (COMPLEX n) st A <> {} holds
dist ((x + z),A) <= (dist (x,A)) + |.z.|
let A be Subset of (COMPLEX n); ( A <> {} implies dist ((x + z),A) <= (dist (x,A)) + |.z.| )
defpred S1[ set ] means $1 in A;
deffunc H1( Element of COMPLEX n) -> Element of REAL = In (|.((x + z) - $1).|,REAL);
deffunc H2( Element of COMPLEX n) -> Real = |.((x + z) - $1).|;
reconsider Y = { H1(z1) where z1 is Element of COMPLEX n : S1[z1] } as Subset of REAL from DOMAIN_1:sch 8();
deffunc H3( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);
deffunc H4( Element of COMPLEX n) -> Real = |.(x - $1).|;
A1:
for z1 being Element of COMPLEX n holds H2(z1) = H1(z1)
;
A2:
{ H2(z1) where z1 is Element of COMPLEX n : S1[z1] } = { H1(z2) where z2 is Element of COMPLEX n : S1[z2] }
from FRAENKEL:sch 5(A1);
A3:
for z1 being Element of COMPLEX n holds H3(z1) = H4(z1)
;
A4:
{ H3(z1) where z1 is Element of COMPLEX n : S1[z1] } = { H4(z2) where z2 is Element of COMPLEX n : S1[z2] }
from FRAENKEL:sch 5(A3);
A5:
Y is bounded_below
reconsider X = { H3(z1) where z1 is Element of COMPLEX n : S1[z1] } as Subset of REAL from DOMAIN_1:sch 8();
assume
A <> {}
; dist ((x + z),A) <= (dist (x,A)) + |.z.|
then consider z2 being Element of COMPLEX n such that
A6:
z2 in A
by SUBSET_1:4;
A7:
dist ((x + z),A) = lower_bound Y
by Def17, A2;
A8:
now for r9 being Real st r9 in X holds
r9 >= (dist ((x + z),A)) - |.z.|let r9 be
Real;
( r9 in X implies r9 >= (dist ((x + z),A)) - |.z.| )assume
r9 in X
;
r9 >= (dist ((x + z),A)) - |.z.|then consider z3 being
Element of
COMPLEX n such that A9:
r9 = |.(x - z3).|
and A10:
z3 in A
by A4;
|.((x + z) - z3).| = |.((x - z3) + z).|
by Th75;
then A11:
|.((x + z) - z3).| <= r9 + |.z.|
by A9, Th97;
|.((x + z) - z3).| in Y
by A10, A2;
then
|.((x + z) - z3).| >= dist (
(x + z),
A)
by A7, A5, Def2;
then
r9 + |.z.| >= dist (
(x + z),
A)
by A11, XXREAL_0:2;
hence
r9 >= (dist ((x + z),A)) - |.z.|
by XREAL_1:20;
verum end;
A12:
|.(x - z2).| in X
by A6, A4;
dist (x,A) = lower_bound X
by Def17, A4;
then
(dist ((x + z),A)) - |.z.| <= dist (x,A)
by A12, A8, Th112;
hence
dist ((x + z),A) <= (dist (x,A)) + |.z.|
by XREAL_1:20; verum