curveIntegral_fun_add — Mathlib

English

The curve integral of a sum of two 2-variable linear maps along a path equals the sum of the curve integrals of each map along the path.

Русский

Интеграл по кривой от суммы двух двухпеременных линейных отображений вдоль пути равен сумме интегралов по каждому отображению.

LaTeX

$$$\\int_{\\text{curve}} (ω_1 x + ω_2 x) = \\int_{\\text{curve}} ω_1 x + \\int_{\\text{curve}} ω_2 x$$$

Lean4

theorem curveIntegral_fun_add (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) :
    ∫ᶜ x in γ, (ω₁ x + ω₂ x) = ∫ᶜ x in γ, ω₁ x + ∫ᶜ x in γ, ω₂ x :=
  curveIntegral_add h₁ h₂

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