distortion_biUnionTagged — Mathlib

English

The distortion of a tagged prepartition built by biUnionTagged equals the supremum over boxes of the distortions of the corresponding tagged prepartitions.

Русский

Искажение помеченного предварительного разбиения, построенного biUnionTagged, равно верхней грань коробок по искажениям соответствующих помеченных предварительных разбиений.

LaTeX

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

Lean4

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

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