lintegral_le_iSup_mul — Mathlib

English

For any f, the lintegral of f is bounded above by the supremum of f times μ(univ).

Русский

Линтеграл по f не превосходит супермножество f умноженное на μ(всё пространство).

LaTeX

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

Lean4

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

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