integral_interval_add_interval_comm

English

For integrable f on intervals [a,b] and [c,d], we have integral over [a,b] plus integral over [c,d] equals integral over [a,d] plus integral over [c,b].

Русский

Для интегрируемой функции по интервалам [a,b] и [c,d] выполняется равенство интегралов, соответствующее коммутативности сложения интервалов.

LaTeX

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

Lean4

theorem integral_interval_add_interval_comm (hab : IntervalIntegrable f μ a b) (hcd : IntervalIntegrable f μ c d)
    (hac : IntervalIntegrable f μ a c) :
    ((∫ x in a..b, f x ∂μ) + ∫ x in c..d, f x ∂μ) = (∫ x in a..d, f x ∂μ) + ∫ x in c..b, f x ∂μ := by
  rw [← integral_add_adjacent_intervals hac hcd, add_assoc, add_left_comm,
    integral_add_adjacent_intervals hac (hac.symm.trans hab), add_comm]

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