iInf_mul_le_lintegral — Mathlib

English

For any f, the product of the infimum of f with μ(univ) is a lower bound for the lintegral of f.

Русский

Пусть f: найдём, что (inf f)·μ(univ) ≤ ∫ f dμ.

LaTeX

$$$$ (\inf_x f(x)) \cdot \mu(\mathrm{univ}) \le \int^- x, f(x) \partial \mu. $$$$

Lean4

theorem iInf_mul_le_lintegral (f : α → ℝ≥0∞) : (⨅ x, f x) * μ .univ ≤ ∫⁻ x, f x ∂μ := by
  calc
    (⨅ x, f x) * μ .univ
    _ = ∫⁻ y, ⨅ x, f x ∂μ := by simp
    _ ≤ ∫⁻ x, f x ∂μ := by gcongr; exact iInf_le _ _

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