distortion_unionComplToSubordinate

English

The distortion of the union-complement subordinate partition equals the maximum of the distortions of π1 and π2.

Русский

Искажение разбиения unionComplToSubordinate равно максимуму искажений π1 и π2.

LaTeX

$$$ (\\pi_1.\\mathrm{unionComplToSubordinate}(\\pi_2,hU,r)).\\mathrm{distortion} = \\max(\\pi_1.\\mathrm{distortion}, \\pi_2.\\mathrm{distortion}) $$$

Lean4

@[simp]
theorem distortion_unionComplToSubordinate (π₁ : TaggedPrepartition I) (π₂ : Prepartition I)
    (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → Ioi (0 : ℝ)) :
    (π₁.unionComplToSubordinate π₂ hU r).distortion = max π₁.distortion π₂.distortion := by
  simp [unionComplToSubordinate]

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