hasMFDerivAt — Mathlib

English

If γ has an integral-curve-at property at t0, then its derivative in coordinates exists and is given by the vector v at γ(t0), pushed forward by the coordinate chart.

Русский

Если γ имеет свойство интегральной кривой в точке t0, то в локальных координатах существует производная γ и она задается вектором v(γ(t0)) через отображение координат.

LaTeX

$$$\mathrm{HasMFDerivAt}(\mathcal{I})\, I\, \gamma\, t_0\;\bigl((1 : \mathbb{R} \to_L[\mathbb{R}] \mathbb{R}).smulRight (v(\gamma(t_0)))\bigr).$$$

Lean4

theorem hasMFDerivAt (h : IsMIntegralCurveAt γ v t₀) :
    HasMFDerivAt 𝓘(ℝ, ℝ) I γ t₀ ((1 : ℝ →L[ℝ] ℝ).smulRight (v (γ t₀))) :=
  have ⟨_, hs, h⟩ := isMIntegralCurveAt_iff.mp h
  h t₀ (mem_of_mem_nhds hs) |>.hasMFDerivAt hs

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