le_iInf_lintegral — Mathlib

English

The lintegral of the iInf of f_i over μ is at least the iInf of the lintegrals.

Русский

Линеграл от infimum функции f_i по μ не хуже infimum интегралов.

LaTeX

$$$$ \int^- a, \big(\big\wedge_i f_i(a)\big) \partial \mu \le \bigwedge_i \int^- a, f_i(a) \partial \mu. $$$$

Lean4

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

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