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]