curveIntegral_fun_sub — Mathlib

English

For ω1, ω2 along γ, the curve integral of their pointwise difference equals the difference of curve integrals of each.

Русский

Для ω1, ω2 вдоль γ верхняя кривая интеграла разности равна разности отдельных криволинеинных интегралов.

LaTeX

$$$\\int_\\gamma (\\omega_1 - \\omega_2) = \\int_\\gamma \\omega_1 - \\int_\\gamma \\omega_2$$$

Lean4

theorem curveIntegral_fun_sub (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) :
    ∫ᶜ x in γ, (ω₁ x - ω₂ x) = ∫ᶜ x in γ, ω₁ x - ∫ᶜ x in γ, ω₂ x :=
  curveIntegral_sub h₁ h₂

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