setIntegral_nonpos — Mathlib

English

Let s be a measurable subset of X and f: X → ℝ satisfy f(x) ≤ 0 for every x ∈ s. Then the integral of f over s is nonpositive: ∫_s f ≤ 0.

Русский

Пусть s — измеримое подмножество X, и f: X → ℝ удовлетворяет f(x) ≤ 0 для всех x ∈ s. Тогда интеграл f по s не положителен: ∫_s f ≤ 0.

LaTeX

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

Lean4

theorem setIntegral_nonpos (hs : MeasurableSet s) (hf : ∀ x, x ∈ s → f x ≤ 0) : ∫ x in s, f x ∂μ ≤ 0 :=
  setIntegral_nonpos_ae hs <| ae_of_all μ hf

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