diam_boxIcc — Mathlib

English

The diameter of Box.Icc(box n ν) is at most 1/n.

Русский

Диаметр Box.Icc(box n ν) не превосходит 1/n.

LaTeX

$$$\operatorname{diam}(Box.Icc(box(n,ν))) \le \frac{1}{n}$$$

Lean4

theorem diam_boxIcc (ν : ι → ℤ) : Metric.diam (Box.Icc (box n ν)) ≤ 1 / n :=
  by
  rw [BoxIntegral.Box.Icc_eq_pi]
  refine ENNReal.toReal_le_of_le_ofReal (by positivity) <| EMetric.diam_pi_le_of_le (fun i ↦ ?_)
  simp_rw [Real.ediam_Icc, box.upper_sub_lower, le_rfl]

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