distortion_filter_le — Mathlib

English

The distortion of a filtered tagged prepartition does not exceed the distortion of the original partition.

Русский

Искажение фильтрованного помеченного предварительного разбиения не превосходит искажения исходного разбиения.

LaTeX

$$$ (\text{π.filter } p).distortion ≤ π.distortion $$$

Lean4

theorem distortion_filter_le (p : Box ι → Prop) : (π.filter p).distortion ≤ π.distortion := by
  classical exact sup_mono (filter_subset _ _)

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