integral_sub — Mathlib

English

The integral of f − g over [a,b] equals the difference of the integrals of f and g over [a,b].

Русский

Интеграл от f − g по [a,b] равен разности интегралов f и g по [a,b].

LaTeX

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

Lean4

@[simp]
theorem integral_sub (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) :
    ∫ x in a..b, f x - g x ∂μ = (∫ x in a..b, f x ∂μ) - ∫ x in a..b, g x ∂μ := by
  simpa only [sub_eq_add_neg] using (integral_add hf hg.neg).trans (congr_arg _ integral_neg)

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