curveIntegral_def — Mathlib

English

The curve integral ω along γ equals the interval integral of curveIntegralFun ω γ over [0,1].

Русский

Криволинейный интеграл ω по γ равен интегралу по [0,1] функции curveIntegralFun ω γ.

LaTeX

$$$ \\curveIntegral(\\omega, \\gamma) = \\int_{0}^{1} \\curveIntegralFun(\\omega, \\gamma, t) \\, dt $$$

Lean4

theorem curveIntegral_def [NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (γ : Path a b) :
    curveIntegral ω γ = ∫ t in 0..1, curveIntegralFun ω γ t := by
  simp only [curveIntegral, NormedSpace.restrictScalars_eq]

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