iSup_lintegral_le — Mathlib

English

For any family of functions f_i, the supremum of their lintegrals is bounded by the lintegral of the pointwise supremum.

Русский

Для семейства функций f_i супремум их линегралов не превосходит линеграл по точному супремиуму функции.

LaTeX

$$$$ \big\lceil \! \big( \sup_i \int^- a, f_i(a) \partial \mu \big) \bigleftrightarrow \int^- a, \big( \sup_i f_i(a) \big) \partial \mu. $$$$

Lean4

theorem iSup_lintegral_le {ι : Sort*} (f : ι → α → ℝ≥0∞) : ⨆ i, ∫⁻ a, f i a ∂μ ≤ ∫⁻ a, ⨆ i, f i a ∂μ :=
  by
  simp only [← iSup_apply]
  exact (monotone_lintegral μ).le_map_iSup

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