curveIntegralFun_def' — Mathlib

English

For a 1-form ω and a path γ, the curve integral function along γ at time t is given by applying ω to the point γ extended at t and to the derivative of the extended path at t.

Русский

Для 1-формы ω и пути γ функция криволинейного интеграла в момент t задаётся как ω(γ^{extend}(t)) применённое к производной пути γ^{extend}(t).

LaTeX

$$$ \\operatorname{curveIntegralFun}(\omega, \\gamma, t) = \\omega\\bigl(\\gamma^{\\mathrm{extend}}(t)\\bigr)\\bigl(\\dfrac{d}{dt}\\gamma^{\\mathrm{extend}}(t)\\bigr) $$$

Lean4

theorem curveIntegralFun_def' : eta_helper Eq✝ @curveIntegralFun.{} @(delta% @definition✝) :=
  by
  intros
  delta curveIntegralFun
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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