curveIntegralFun_neg — Mathlib

English

For two curve-integrable forms along γ, the integral of their sum equals the sum of the integrals along γ.

Русский

Для двух форм, интегрируемых по кривой, интеграл их суммы равен сумме интегралов по кривой.

LaTeX

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

Lean4

@[simp]
theorem curveIntegralFun_neg : curveIntegralFun (-ω) γ = -curveIntegralFun ω γ := by ext; simp [curveIntegralFun]

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