curveIntegralFun_symm — Mathlib

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 ω γ

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