curveIntegralFun_add — Mathlib

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]

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