setLIntegral_eq_zero — Mathlib

English

If on a measurable set s the function f equals zero, then the integral over s is zero: ∫_s f dμ = 0.

Русский

Если на измеримом множестве s функция f равна нулю, то интеграл по s равен нулю.

LaTeX

$$$\\int_s f \\, d\\mu = 0$$$

Lean4

theorem setLIntegral_eq_zero {f : α → ℝ≥0∞} {s : Set α} (hs : MeasurableSet s) (h's : EqOn f 0 s) :
    ∫⁻ x in s, f x ∂μ = 0 := by simp [setLIntegral_congr_fun hs h's]

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