setIntegral_nonpos_of_ae

Mathlib.MeasureTheory.Integral.Bochner.Set

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

English

If f ≤ 0 almost everywhere, then the integral over the whole space is nonpositive.

Русский

Если f ≤ 0 почти повсеместно, то интеграл по всему пространству не положителен.

LaTeX

$$$$\\int_{x\\in X} f(x)\\,d\\mu \\le 0.$$$$

Lean4

theorem setIntegral_nonpos_of_ae (hf : f ≤ᵐ[μ] 0) : ∫ x in s, f x ∂μ ≤ 0 :=
  setIntegral_nonpos_of_ae_restrict (ae_restrict_of_ae hf)

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

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

Разделы

Аффилиация

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