setIntegral_nonneg_of_ae_restrict

Mathlib.MeasureTheory.Integral.Bochner.Set

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

English

If f ≥ 0 μ-almost everywhere on s, then the integral over s is nonnegative.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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