distortion_biUnionPrepartition — Mathlib

English

For a tagged prepartition π and a family πi of prepartitions, the distortion of the biUnionPrepartition equals the supremum over boxes of the distortions of πi(J).

Русский

Для помеченного предварительного разбиения π и семейства πi предразбиений, искажение biUnionPrepartition равно верхней грань по коробкам коробок dist(πi(J)).

LaTeX

$$$ (π.biUnionPrepartition πi).distortion = π.boxes.sup (\lambda J, (πi J).distortion) $$$

Lean4

@[simp]
theorem distortion_biUnionPrepartition (π : TaggedPrepartition I) (πi : ∀ J, Prepartition J) :
    (π.biUnionPrepartition πi).distortion = π.boxes.sup fun J => (πi J).distortion := by classical exact sup_biUnion _ _

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