dist_le_distortion_mul — Mathlib

English

The distance between the two corners of the box, in the ambient metric, is bounded by the distortion times the edge length in a fixed coordinate i.

Русский

Расстояние между двумя углами коробки в метрическом смысле ограничено искажением на длину ребра вдоль фиксированной координаты i.

LaTeX

$$$$\forall I,i,\; dist(I.lower,I.upper) \leq I.distortion \cdot (I.upper(i)-I.lower(i)).$$$$

Lean4

theorem dist_le_distortion_mul (I : Box ι) (i : ι) : dist I.lower I.upper ≤ I.distortion * (I.upper i - I.lower i) :=
  by
  have A : I.lower i - I.upper i < 0 := sub_neg.2 (I.lower_lt_upper i)
  simpa only [← NNReal.coe_le_coe, ← dist_nndist, NNReal.coe_mul, Real.dist_eq, abs_of_neg A, neg_sub] using
    I.nndist_le_distortion_mul i

Похожие утверждения