diam_le — Mathlib

English

For any J in the partition, the diameter of Icc(J) is bounded by twice the radius r(tag(J)).

Русский

Для любой коробки J в разбиении диаметр Icc(J) ограничен вдвое радиусом r(tag(J)).

LaTeX

$$$ \\operatorname{diam}(\\mathrm{Icc}(J)) \\le 2 \\; r(\\pi.tag(J)) $$$

Lean4

theorem diam_le [Fintype ι] {π : TaggedPrepartition I} (h : π.IsSubordinate r) (hJ : J ∈ π.boxes) :
    diam (Box.Icc J) ≤ 2 * r (π.tag J) :=
  calc
    diam (Box.Icc J) ≤ diam (closedBall (π.tag J) (r <| π.tag J)) := diam_mono (h J hJ) isBounded_closedBall
    _ ≤ 2 * r (π.tag J) := diam_closedBall (le_of_lt (r _).2)

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