integral_add — Mathlib

English

If f and g are interval-integrable on [a,b], then the integral of f + g over [a,b] equals the sum of the integrals:

Русский

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

LaTeX

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

Lean4

@[simp]
nonrec theorem integral_add (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
  simp only [intervalIntegral_eq_integral_uIoc, integral_add hf.def' hg.def', smul_add]

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