setIntegral_mono_set — Mathlib

English

If f is integrable and f ≤ g almost everywhere on s, then ∫_s f ≤ ∫_s g.

Русский

Если f интегрируемо и f ≤ g почти повсеместно на s, то ∫_s f ≤ ∫_s g.

LaTeX

$$$$\\int_{x\\in s} f(x)\\,d\\mu \\le \\int_{x\\in s} g(x)\\,d\\mu.$$$$

Lean4

theorem setIntegral_mono_set (hfi : IntegrableOn f t μ) (hf : 0 ≤ᵐ[μ.restrict t] f) (hst : s ≤ᵐ[μ] t) :
    ∫ x in s, f x ∂μ ≤ ∫ x in t, f x ∂μ :=
  integral_mono_measure (Measure.restrict_mono_ae hst) hf hfi

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