lintegral_mono_fn — Mathlib

English

The supremum over all measurable g with g ≤ f of their lintegral equals the lintegral of f.

Русский

Предел по верхней границе над всеми измеримыми g с g ≤ f равен линегралу f.

LaTeX

$$$\forall f : α \to \mathbb{R}_{\ge 0}^{\infty},\; ∨ (g : α \to \mathbb{R}_{\ge 0}^{\infty}) (\mathrm{Measurable} g) (g ≤ f), \; ∫^- a, g a \partial μ = ∫^- a, f a ∂μ$$$

Lean4

@[deprecated lintegral_mono (since := "2025-07-10")]
theorem lintegral_mono_fn ⦃f g : α → ℝ≥0∞⦄ (hfg : ∀ x, f x ≤ g x) : ∫⁻ a, f a ∂μ ≤ ∫⁻ a, g a ∂μ :=
  lintegral_mono hfg

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