distortion_biUnion — Mathlib

English

The distortion of a biUnion equals the maximum over the boxes of the πi-distortions.

Русский

Искажение biUnion равно максимуму по коробкам частичных предразбиений πi-distortion.

LaTeX

$$$ (\pi.bnUnion \pi_i).distortion = \pi.boxes.sup (\lambda J, (\pi_i J).distortion). $$$

Lean4

theorem distortion_biUnion (π : Prepartition I) (πi : ∀ J, Prepartition J) :
    (π.biUnion πi).distortion = π.boxes.sup fun J => (πi J).distortion := by classical exact sup_biUnion _ _

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