setIntegral_eq_integral_of_ae_compl_eq_zero

English

If a function vanishes almost everywhere on sᶜ, then the integral over s equals the integral over the whole space.

Русский

Если функция почти нигде не отлична на дополнении s, то интеграл по s равен интегралу по всему пространству.

LaTeX

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

Lean4

/-- If a function vanishes almost everywhere on `sᶜ`, then its integral on `s`
coincides with its integral on the whole space. -/
theorem setIntegral_eq_integral_of_ae_compl_eq_zero (h : ∀ᵐ x ∂μ, x ∉ s → f x = 0) : ∫ x in s, f x ∂μ = ∫ x, f x ∂μ :=
  by
  symm
  nth_rw 1 [← setIntegral_univ]
  apply setIntegral_eq_of_subset_of_ae_diff_eq_zero nullMeasurableSet_univ (subset_univ _)
  filter_upwards [h] with x hx h'x using hx h'x.2

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