trim_sum_ge — Mathlib

English

For a family (m_i), the sum of their trims is below or equal to the trim of the sum:

Русский

Для семейства мер сумма обрезок меньше или равна обрезке суммы: (Σ m_i).trim ≥ Σ (m_i).trim.

LaTeX

$$$$ (\\sum_i (m_i).\\mathrm{trim}) \le (\\sum_i m_i).\\mathrm{trim}. $$$$

Lean4

theorem trim_sum_ge {ι} (m : ι → OuterMeasure α) : (sum fun i => (m i).trim) ≤ (sum m).trim := fun s =>
  by
  simp only [sum_apply, trim_eq_iInf, le_iInf_iff]
  exact fun t st ht => ENNReal.tsum_le_tsum fun i => iInf_le_of_le t <| iInf_le_of_le st <| iInf_le _ ht

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