setLIntegral_mono_ae' — Mathlib

English

If g is almost everywhere larger than f on a set, then the lintegral of f on that set is ≤ the lintegral of g on that set.

Русский

Если g ≥ f почти везде на s, то ∫_s f ≤ ∫_s g. (a.e. on μ.restrict s)

LaTeX

$$$$ \text{For } s, f, g: \; \text{AEMeasurable}(g, μ.restrict s) \; \wedge \; (f ≤ g \text{ a.e. on } μ.restrict s) \Rightarrow \int^- x in s, f(x) \partial μ ≤ \int^- x in s, g(x) \partial μ. $$$$

Lean4

theorem setLIntegral_mono_ae' {s : Set α} {f g : α → ℝ≥0∞} (hs : MeasurableSet s) (hfg : ∀ᵐ x ∂μ, x ∈ s → f x ≤ g x) :
    ∫⁻ x in s, f x ∂μ ≤ ∫⁻ x in s, g x ∂μ :=
  lintegral_mono_ae <| (ae_restrict_iff' hs).2 hfg

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