English
For any box I and coordinate i, the nonnegative distance between I.lower and I.upper is bounded by distortion(I) times the edge length along i: nndist(I.lower,I.upper) ≤ distortion(I) · nndist(I.lower i, I.upper i).
Русский
Для каждой координаты i справедливо неотрицательное неравенство nndist(I.lower,I.upper) ≤ dist(I) · nndist(I.lower i, I.upper i).
LaTeX
$$$$\forall I,i,\; nndist(I.lower,I.upper) \\leq I.distortion \cdot nndist(I.lower(i),I.upper(i)).$$$$
Lean4
theorem nndist_le_distortion_mul (I : Box ι) (i : ι) :
nndist I.lower I.upper ≤ I.distortion * nndist (I.lower i) (I.upper i) :=
calc
nndist I.lower I.upper = nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i) :=
(div_mul_cancel₀ _ <| mt nndist_eq_zero.1 (I.lower_lt_upper i).ne).symm
_ ≤ I.distortion * nndist (I.lower i) (I.upper i) :=
by
apply mul_le_mul_right'
apply Finset.le_sup (Finset.mem_univ i)
