setIntegral_measure_zero — Mathlib

English

If a set s has μ-measure zero, then integrating over s yields zero: ∫ x∈s f(x) dμ = 0.

Русский

Если множество s имеет μ-мера равную нулю, то интеграл по s равен нулю: ∫ x∈s f(x) dμ = 0.

LaTeX

$$$$\int x \in s, f(x) \partial\mu = 0.$$$$

Lean4

@[simp]
theorem setIntegral_measure_zero (f : α → G) {μ : Measure α} {s : Set α} (hs : μ s = 0) : ∫ x in s, f x ∂μ = 0 :=
  Measure.restrict_eq_zero.mpr hs ▸ integral_zero_measure f

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