English
If the distortion of I is at most c, then the diameter of the Cartesian box Icc(I) is bounded by c times the length of any edge of I in that coordinate.
Русский
Если искажение I не превосходит c, тогда диаметр множества Icc(I) не превосходит c·(I.upper i − I.lower i) по любой координате i.
LaTeX
$$$$\forall I,i,c,\; (I.distortion \le c) \Rightarrow diam(Box.Icc I) \le c \cdot (I.upper i - I.lower i).$$$$
Lean4
theorem diam_Icc_le_of_distortion_le (I : Box ι) (i : ι) {c : ℝ≥0} (h : I.distortion ≤ c) :
diam (Box.Icc I) ≤ c * (I.upper i - I.lower i) :=
have : (0 : ℝ) ≤ c * (I.upper i - I.lower i) := mul_nonneg c.coe_nonneg (sub_nonneg.2 <| I.lower_le_upper _)
diam_le_of_forall_dist_le this fun x hx y hy ↦
calc
dist x y ≤ dist I.lower I.upper := Real.dist_le_of_mem_pi_Icc hx hy
_ ≤ I.distortion * (I.upper i - I.lower i) := (I.dist_le_distortion_mul i)
_ ≤ c * (I.upper i - I.lower i) := by gcongr; exact sub_nonneg.2 (I.lower_le_upper i)
