curveIntegralFun_smul — Mathlib

English

The curve integral linearity with respect to a scalar: curveIntegralFun (c • ω) γ = c • curveIntegralFun ω γ.

Русский

Линейность криволинейного интеграла по умножению на скаляр: curveIntegralFun(c • ω) γ = c • curveIntegralFun(ω) γ.

LaTeX

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

Lean4

@[simp]
theorem curveIntegralFun_smul : curveIntegralFun (c • ω) γ = c • curveIntegralFun ω γ :=
  by
  ext
  simp [curveIntegralFun]

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