isMIntegralCurve_comp_add — Mathlib

English

For any dt, IsMIntegralCurve γ v is equivalent to IsMIntegralCurve (γ ∘ (·+dt)) v; i.e., shifting the time parameter does not affect the status of being an integral curve.

Русский

Для любого dt равенство IsMIntegralCurve γ v ⇔ IsMIntegralCurve (γ ∘ (·+dt)) v: сдвиг времени не меняет статус интегральной кривой.

LaTeX

$$$IsMIntegralCurve(\\gamma, v) \\iff IsMIntegralCurve(\\gamma \\circ (\\cdot + dt), v)$$$

Lean4

theorem isMIntegralCurve_comp_add {dt : ℝ} : IsMIntegralCurve γ v ↔ IsMIntegralCurve (γ ∘ (· + dt)) v :=
  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]

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