curveIntegralFun_sub — Mathlib

English

Let ω1 and ω2 be operator-valued functions along a fixed path γ. Then the curve integral is linear in the integrand: the integral of ω1 − ω2 along γ equals the integral of ω1 along γ minus the integral of ω2 along γ.

Русский

Пусть вдоль заданного пути γ имеются линейноподобные отображения ω1 и ω2. Тогда кривая интеграла линейна по ядру: интеграл по кривой ω1 − ω2 равен интегралу ω1 минус интеграл ω2.

LaTeX

$$$\\operatorname{curveIntegralFun}(\\omega_1 - \\omega_2, \\gamma) = \\operatorname{curveIntegralFun}(\\omega_1, \\gamma) - \\operatorname{curveIntegralFun}(\\omega_2, \\gamma)$$$

Lean4

@[simp]
theorem curveIntegralFun_sub : curveIntegralFun (ω₁ - ω₂) γ = curveIntegralFun ω₁ γ - curveIntegralFun ω₂ γ := by
  simp [sub_eq_add_neg]

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