distortion_disjUnion — Mathlib

English

If π1.iUnion and π2.iUnion are disjoint, then the distortion of π1.disjUnion π2 equals the maximum of their distortions.

Русский

Если iUnion π1 и iUnion π2 несовместны, то искажение π1.disjUnion π2 равно максимуму их искажений.

LaTeX

$$$ (π_1.disjUnion π_2 h).distortion = \max(π_1.distortion, π_2.distortion). $$$

Lean4

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

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