curveIntegralFun_cast — Mathlib

English

If two paths γ and γ⊙ have the same endpoints via cast, their curveIntegralFun coincide.

Русский

Если γ и γ^{cast} имеют одинаковые концы, их curveIntegralFun совпадают.

LaTeX

$$$ \\curveIntegralFun(\\omega, γ^{\\mathrm{cast}}) = \\curveIntegralFun(\\omega, γ) $$$

Lean4

@[simp]
theorem curveIntegralFun_cast (ω : E → E →L[𝕜] F) (γ : Path a b) (hc : c = a) (hd : d = b) :
    curveIntegralFun ω (γ.cast hc hd) = curveIntegralFun ω γ :=
  by
  ext t
  simp only [curveIntegralFun_def', Path.extend_cast]

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