curveIntegral_cast — Mathlib

English

The curve integral along γ cast with endpoints matches the integral along γ.

Русский

Кривой интеграл вдоль γ^{cast} совпадает с интегралом вдоль γ.

LaTeX

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

Lean4

@[simp]
theorem curveIntegral_cast (ω : E → E →L[𝕜] F) (γ : Path a b) (hc : c = a) (hd : d = b) :
    ∫ᶜ x in γ.cast hc hd, ω x = ∫ᶜ x in γ, ω x := by simp [curveIntegral]

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