integral_union_eq_left_of_forall — Mathlib

English

If f vanishes on t, and t is measurable, then the integral over s ∪ t equals the integral over s, provided the usual measurability conditions hold.

Русский

Если f равна нулю на 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 : MeasurableSet t) (ht_eq : ∀ x ∈ t, f x = 0) :
    ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ :=
  integral_union_eq_left_of_forall₀ ht.nullMeasurableSet ht_eq

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