setIntegral_eq_zero_iff_of_nonneg_ae

English

For a real-valued function f that is nonnegative μ-a.e. on s and integrable, the integral over s is zero if and only if f is μ-restrict ae equal to 0 on s.

Русский

Для функции f≥0 μ-почти всюду на s и интегрируемой, интеграл по s равен нулю тогда и только тогда, когда f равно нулю μ-предельность на s.

LaTeX

$$$$ \\int_{s} f \\, d\\mu = 0 \\quad\\text{iff}\\quad f = 0 \\, \\text{a.e. w.r.t. } \\mu|_{s} $$$$

Lean4

theorem setIntegral_eq_zero_iff_of_nonneg_ae {f : X → ℝ} (hf : 0 ≤ᵐ[μ.restrict s] f) (hfi : IntegrableOn f s μ) :
    ∫ x in s, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict s] 0 :=
  integral_eq_zero_iff_of_nonneg_ae hf hfi

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