setLIntegral_mono — Mathlib

English

If g is measurable and f ≤ g on a set, then the lintegral of f over that set is ≤ the lintegral of g over the same set.

Русский

Если g измерима и f ≤ g на s, то ∫_s f ≤ ∫_s g.

LaTeX

$$$$ \text{If } \mathrm{Measurable}(g) \text{ and } \forall x \in s, f(x) \le g(x), \quad \int^- x in s, f(x) \partial \mu \le \int^- x in s, g(x) \partial \mu. $$$$

Lean4

theorem setLIntegral_mono {s : Set α} {f g : α → ℝ≥0∞} (hg : Measurable g) (hfg : ∀ x ∈ s, f x ≤ g x) :
    ∫⁻ x in s, f x ∂μ ≤ ∫⁻ x in s, g x ∂μ :=
  setLIntegral_mono_ae hg.aemeasurable (ae_of_all _ hfg)

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