distortion_disjUnion — Mathlib

English

If every box in the partition has distortion equal to c, then the distortion of the whole partition is c.

Русский

Если все коробки разбиения имеют искажение, равное c, то искажение всего разбиения равно c.

LaTeX

$$$ π.distortion = c $ given $ π.boxes.Nonempty $ and $ ∀ J ∈ π, J.distortion = c $$$

Lean4

@[simp]
theorem distortion_disjUnion (h : Disjoint π₁.iUnion π₂.iUnion) :
    (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion := by classical exact sup_union

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