isMIntegralCurve_comp_sub — Mathlib

English

If γ is an integral curve of v, then composing γ with a time-scaling factor a ≠ 0 yields another integral curve with velocity a·v, i.e., IsMIntegralCurve γ v → IsMIntegralCurve (γ ∘ (·*a)) (a·v).

Русский

Если γ является интегральной кривой v, то композиция γ с масштабированием времени на a ≠ 0 дает другую интегральную кривую с ускорением a·v.

LaTeX

$$$IsMIntegralCurve(\\gamma, v) \\rightarrow IsMIntegralCurve(\\gamma \\circ (\\cdot * a), a \\cdot v)$$$

Lean4

theorem isMIntegralCurve_comp_sub {dt : ℝ} : IsMIntegralCurve γ v ↔ IsMIntegralCurve (γ ∘ (· - dt)) v := by
  simpa using isMIntegralCurve_comp_add (dt := -dt)

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