setIntegral_eq_of_subset_of_forall_diff_eq_zero

English

If s ⊆ t and f vanishes a.e. on t, then the integrals over t and s coincide given measurability and integrability assumptions.

Русский

Если s ⊆ t и f нулевая почти повсюду на t, то интегралы по t и s совпадают при выполнении условий измеримости и интегрируемости.

LaTeX

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

Lean4

/-- If a function vanishes on `t \ s` with `s ⊆ t`, then its integrals on `s`
and `t` coincide if `t` is measurable. -/
theorem setIntegral_eq_of_subset_of_forall_diff_eq_zero (ht : MeasurableSet t) (hts : s ⊆ t)
    (h't : ∀ x ∈ t \ s, f x = 0) : ∫ x in t, f x ∂μ = ∫ x in s, f x ∂μ :=
  setIntegral_eq_of_subset_of_ae_diff_eq_zero ht.nullMeasurableSet hts (Eventually.of_forall fun x hx => h't x hx)

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