setIntegral_eq_zero_of_forall_eq_zero

English

If f vanishes almost everywhere on t, then the integral over s ∪ t equals the integral over s.

Русский

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

LaTeX

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

Lean4

theorem setIntegral_eq_zero_of_forall_eq_zero (ht_eq : ∀ x ∈ t, f x = 0) : ∫ x in t, f x ∂μ = 0 :=
  setIntegral_eq_zero_of_ae_eq_zero (Eventually.of_forall ht_eq)

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