setIntegral_eq_integral_of_forall_compl_eq_zero

English

If f vanishes on the complement of s, then the integral over s equals the integral over the whole space.

Русский

Если f равна нулю на дополнении s, то интеграл по s равен интегралу по всему пространству.

LaTeX

$$$$ \int_{x \in s} f(x) \, d\mu = \int_{x \in X} f(x) \, d\mu $$$$

Lean4

/-- If a function vanishes on `sᶜ`, then its integral on `s` coincides with its integral on the
whole space. -/
theorem setIntegral_eq_integral_of_forall_compl_eq_zero (h : ∀ x, x ∉ s → f x = 0) : ∫ x in s, f x ∂μ = ∫ x, f x ∂μ :=
  setIntegral_eq_integral_of_ae_compl_eq_zero (Eventually.of_forall h)

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