setIntegral_nonpos_of_ae_restrict

Mathlib.MeasureTheory.Integral.Bochner.Set

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

English

If f ≤ 0 almost everywhere on s, then the restricted integral over s is nonpositive.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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