isMIntegralCurveAt_comp_sub — Mathlib

English

If γ is an integral curve of v, then translating the parameter by any dt preserves the integral-curve property. That is, IsMIntegralCurve γ v ↔ IsMIntegralCurve (γ ∘ (·+dt)) v.

Русский

Если γ является интегральной кривой v, то сдвиг параметра времени на dt сохраняет эту свойство: IsMIntegralCurve γ v ↔ IsMIntegralCurve (γ ∘ (·+dt)) v.

LaTeX

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

Lean4

theorem isMIntegralCurveAt_comp_sub {dt : ℝ} :
    IsMIntegralCurveAt γ v t₀ ↔ IsMIntegralCurveAt (γ ∘ (· - dt)) v (t₀ + dt) := by
  simpa using isMIntegralCurveAt_comp_add (dt := -dt)

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