curveIntegral_sub — Mathlib

English

Let ω1 and ω2 be integrable along γ. Then the integral of their difference equals the difference of their integrals: ∫_γ (ω1 − ω2) = ∫_γ ω1 − ∫_γ ω2.

Русский

Пусть ω1 и ω2 интегрируемы вдоль γ. Тогда интеграл их разности равен разности интегралов: ∫_γ (ω1 − ω2) = ∫_γ ω1 − ∫_γ ω2.

LaTeX

$$$\\curveIntegral(\\omega_1 - \\omega_2, \\gamma) = \\curveIntegral(\\omega_1, \\gamma) - \\curveIntegral(\\omega_2, \\gamma)$$$

Lean4

theorem curveIntegral_sub (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) :
    curveIntegral (ω₁ - ω₂) γ = ∫ᶜ x in γ, ω₁ x - ∫ᶜ x in γ, ω₂ x := by
  rw [sub_eq_add_neg, sub_eq_add_neg, curveIntegral_add h₁ h₂.neg, curveIntegral_neg]

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