curveIntegralFun_restrictScalars — Mathlib

English

The integral along γ of a ω(t) viewed with scalars restricted to 𝕝 is the same as the integral of ω(t) without restriction.

Русский

Интеграл вдоль γ от ω(t), рассмотренного с ограничением по скаляру 𝕝, совпадает с интегралом от ω(t) без ограничений.

LaTeX

$$$\\int_{\\gamma} (\\omega x).\\text{restrictScalars} 𝕝 = \\int_{\\gamma} \\omega x$$$

Lean4

@[simp]
theorem curveIntegralFun_restrictScalars :
    curveIntegralFun (fun t ↦ (ω t).restrictScalars 𝕝) γ = curveIntegralFun ω γ :=
  by
  ext
  letI : NormedSpace ℝ E := .restrictScalars ℝ 𝕜 E
  simp [curveIntegralFun_def]

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