integral_add_adjacent_intervals — Mathlib

English

If f is interval-integrable on [a,b] and [b,c], then ∫_a^b f + ∫_b^c f = ∫_a^c f.

Русский

Если f интегрируема по интервалам [a,b] и [b,c], то сумма интегралов равна интегралу по [a,c].

LaTeX

$$$( \\int_{a}^{b} f(x) \\, dμ ) + ( \\int_{b}^{c} f(x) \\, dμ ) = \\int_{a}^{c} f(x) \\, dμ $$$

Lean4

theorem integral_add_adjacent_intervals (hab : IntervalIntegrable f μ a b) (hbc : IntervalIntegrable f μ b c) :
    ((∫ x in a..b, f x ∂μ) + ∫ x in b..c, f x ∂μ) = ∫ x in a..c, f x ∂μ := by
  rw [← add_neg_eq_zero, ← integral_symm, integral_add_adjacent_intervals_cancel hab hbc]

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