integral_union_eq_left_of_forall₀

English

If a function vanishes almost everywhere on t, then the integral over s ∪ t equals the integral over s when t is null-measurable.

Русский

Если функция равна нулю почти повсюду на t, и 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 integral_union_eq_left_of_forall₀ {f : X → E} (ht : NullMeasurableSet t μ) (ht_eq : ∀ x ∈ t, f x = 0) :
    ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ :=
  integral_union_eq_left_of_ae ((ae_restrict_iff'₀ ht).2 (Eventually.of_forall ht_eq))

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