curveIntegral_add — Mathlib

English

If ω1 and ω2 are curve-integrable along γ, then the curve integral of the sum equals the sum of the curve integrals.

Русский

Если ω1 и ω2 интегрируемы по кривой γ, то интеграл по сумме равен сумме интегралов по каждой функции.

LaTeX

$$$\\text{curveIntegral}(ω_1+ω_2, γ) = \\text{curveIntegral}(ω_1, γ) + \\text{curveIntegral}(ω_2, γ)$$$

Lean4

theorem curveIntegral_add (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) :
    curveIntegral (ω₁ + ω₂) γ = ∫ᶜ x in γ, ω₁ x + ∫ᶜ x in γ, ω₂ x :=
  by
  letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F
  simp only [curveIntegral, curveIntegralFun_add]
  exact intervalIntegral.integral_add h₁ h₂

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