integral_diff — Mathlib

English

If t ⊆ s, then the integral over s\\t equals ∫_s f − ∫_t f.

Русский

Если t ⊆ s, то интеграл по s\\t равен ∫_s f − ∫_t f.

LaTeX

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

Lean4

theorem integral_diff (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :
    ∫ x in s \ t, f x ∂μ = ∫ x in s, f x ∂μ - ∫ x in t, f x ∂μ :=
  by
  rw [eq_sub_iff_add_eq, ← setIntegral_union, diff_union_of_subset hts]
  exacts [disjoint_sdiff_self_left, ht, hfs.mono_set diff_subset, hfs.mono_set hts]

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