trim_mono — Mathlib

English

Trim is monotone with respect to the underlying outer measure order: if m ≤ n then m.trim ≤ n.trim.

Русский

Обозначение монотонности обрезки по отношению к исходной мере: если m ≤ n, тогда m.trim ≤ n.trim.

LaTeX

$$$$ m \le n \Rightarrow m^{\mathrm{trim}} \le n^{\mathrm{trim}}. $$$$

Lean4

@[mono]
theorem trim_mono : Monotone (trim : OuterMeasure α → OuterMeasure α) := fun _m₁ _m₂ H _s =>
  iInf₂_mono fun _f _hs => ENNReal.tsum_le_tsum fun _b => iInf_mono fun _hf => H _

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