setIntegral_mono_ae

Mathlib.MeasureTheory.Integral.Bochner.Set

URI: https://scilib.ai/kg/mathlib#MeasureTheory.setIntegral_mono_ae

English

If f ≤ g almost everywhere on s with respect to μ, then the integral over s of f is ≤ the integral over s of g.

Русский

Если 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_ae (h : f ≤ᵐ[μ] g) : ∫ x in s, f x ∂μ ≤ ∫ x in s, g x ∂μ :=
  setIntegral_mono_ae_restrict hf hg (ae_restrict_of_ae h)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru