curveIntegral_fun_smul — Mathlib

English

curveIntegralFun (c • ω) γ = c • curveIntegralFun ω γ, where c multiplies each ω(t).

Русский

Криволинейный интеграл-функция линейна по скаляру: curveIntegralFun(c • ω) γ = c • curveIntegralFun ω γ.

LaTeX

$$$\\operatorname{curveIntegralFun}(c \\cdot \\omega, \\gamma) = c \\cdot \\operatorname{curveIntegralFun}(\\omega, \\gamma)$$$

Lean4

@[simp]
theorem curveIntegral_fun_smul : ∫ᶜ x in γ, c • ω x = c • ∫ᶜ x in γ, ω x :=
  curveIntegral_smul

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