biUnionPrepartition — Mathlib

English

For any J in the partition, the diameter of Icc(J) is at most 2 times the radius r(tag(J)).

Русский

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

LaTeX

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

Lean4

theorem biUnionPrepartition [Fintype ι] (h : IsSubordinate π r) (πi : ∀ J, Prepartition J) :
    IsSubordinate (π.biUnionPrepartition πi) r := fun _ hJ =>
  Subset.trans (Box.le_iff_Icc.1 <| π.toPrepartition.le_biUnionIndex hJ) <| h _ <| π.toPrepartition.biUnionIndex_mem hJ

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