curveIntegralFun_symm_apply — Mathlib

English

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

Русский

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

LaTeX

$$$ \\curveIntegral(\\omega, \\gamma) = \\int_0^1 \\curveIntegralFun(\\omega, \\gamma, t) \\, dt $$$

Lean4

theorem curveIntegralFun_symm_apply (ω : E → E →L[𝕜] F) (γ : Path a b) (t : ℝ) :
    curveIntegralFun ω γ.symm t = -curveIntegralFun ω γ (1 - t) := by
  simp [curveIntegralFun, γ.extend_symm, derivWithin_comp_const_sub]

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