English
For any ω, γ, t, the function curveIntegralFun ω γ t is given by ω at γ^{extend}(t) acting on the derivative at t.
Русский
Для любых ω, γ, t функция curveIntegralFun ω γ t задаётся как ω(γ^{extend}(t)) действует на производную в t.
LaTeX
$$$ \\operatorname{curveIntegralFun}(\\omega, \\gamma, t) = \\omega\\bigl(\\gamma^{\\mathrm{extend}}(t)\\bigr)\\bigl(\\gamma^{\\mathrm{extend}\\prime}(t)\\bigr) $$$
Lean4
@[simp]
theorem curveIntegralFun_symm (ω : E → E →L[𝕜] F) (γ : Path a b) :
curveIntegralFun ω γ.symm = (-curveIntegralFun ω γ <| 1 - ·) :=
funext <| curveIntegralFun_symm_apply ω γ