integral_inter_add_diff₀ — Mathlib

English

For null-measurable t, the sum of integrals over s∩t and s\\t equals the integral over s.

Русский

Для нулевой измеримости t сумма интегралов по s∩t и s\\t равна интегралу по s.

LaTeX

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

Lean4

theorem integral_inter_add_diff₀ (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ) :
    ∫ x in s ∩ t, f x ∂μ + ∫ x in s \ t, f x ∂μ = ∫ x in s, f x ∂μ :=
  by
  rw [← Measure.restrict_inter_add_diff₀ s ht, integral_add_measure]
  · exact Integrable.mono_measure hfs (Measure.restrict_mono inter_subset_left le_rfl)
  · exact Integrable.mono_measure hfs (Measure.restrict_mono diff_subset le_rfl)

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