English
Let γ be a parametrized integral curve with velocity v starting at time t0. Then shifting the time parameter by any real amount dt produces a curve γ∘(·+dt) that is again an integral curve with the same velocity field, but reindexed to start at t0−dt. Conversely, any time-shifted version arises this way. In short, IsMIntegralCurveAt γ v t0 is equivalent to IsMIntegralCurveAt (γ ∘ (·+dt)) v (t0 − dt) for every real dt.
Русский
Пусть γ — параметризованная интегральная кривая с векторным полем скорости v, стартующая во времени t0. При сдвиге параметра времени на произвольное действительное число dt кривая γ∘(·+dt) снова является интегральной кривой с тем же полем v, просто с другим отсчётом времени (t0−dt). И наоборот. Иными словами, IsMIntegralCurveAt γ v t0 эквивалично IsMIntegralCurveAt (γ ∘ (·+dt)) v (t0 − dt) для любого dt.
LaTeX
$$$IsMIntegralCurveAt(\\gamma, v, t_0) \\iff IsMIntegralCurveAt(\\gamma \\circ (\\cdot + dt), v, t_0 - dt)$$$
Lean4
theorem isMIntegralCurveAt_comp_add {dt : ℝ} :
IsMIntegralCurveAt γ v t₀ ↔ IsMIntegralCurveAt (γ ∘ (· + dt)) v (t₀ - dt) :=
by
refine ⟨fun hγ ↦ hγ.comp_add _, fun hγ ↦ ?_⟩
convert hγ.comp_add (-dt)
· ext t
simp only [Function.comp_apply, neg_add_cancel_right]
· simp only [sub_neg_eq_add, sub_add_cancel]
