English
Let ω1 and ω2 be curve-integrable along a common path γ. Then the curve integral of their sum equals the sum of the curve integrals.
Русский
Пусть ω1 и ω2 интегрируемы по кривой γ. Тогда интеграл по сумме ω1 + ω2 равен сумме интегралов.
LaTeX
$$$\\text{CurveIntegrable}(ω_1, γ) \\to \\text{CurveIntegrable}(ω_2, γ) \\Rightarrow \\text{curveIntegral}(ω_1 + ω_2, γ) = \\text{curveIntegral}(ω_1, γ) + \\text{curveIntegral}(ω_2, γ)$$$
Lean4
@[simp]
theorem curveIntegralFun_add : curveIntegralFun (ω₁ + ω₂) γ = curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ := by ext;
simp [curveIntegralFun]