curveIntegralFun_def — Mathlib

English

The value of curveIntegralFun ω γ t is ω evaluated at γ^{extend}(t) on the derivative of γ^{extend} at t.

Русский

Значение curveIntegralFun ω γ t равно ω(γ^{extend}(t)) на производной γ^{extend} в точке t.

LaTeX

$$$ \\operatorname{curveIntegralFun}(\\omega, \\gamma, t) = \\omega\\bigl(\\gamma^{\\mathrm{extend}}(t)\\bigr)\\bigl( \\dfrac{d}{dt}\\gamma^{\\mathrm{extend}}(t) \\bigr) $$$

Lean4

theorem curveIntegralFun_def [NormedSpace ℝ E] (ω : E → E →L[𝕜] F) (γ : Path a b) (t : ℝ) :
    curveIntegralFun ω γ t = ω (γ.extend t) (derivWithin γ.extend I t) := by
  simp only [curveIntegralFun, NormedSpace.restrictScalars_eq]

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