comp_add — Mathlib

English

If γ is an integral curve of v, then for every real dt the curve γ ∘ (·+dt) is again an integral curve with velocity v, i.e., IsMIntegralCurve γ v → IsMIntegralCurve (γ ∘ (·+dt)) v.

Русский

Если γ является интегральной кривой v, то для каждого dt кривая γ ∘ (·+dt) снова является интегральной кривой с той же скоростью v.

LaTeX

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

Lean4

theorem comp_add (hγ : IsMIntegralCurve γ v) (dt : ℝ) : IsMIntegralCurve (γ ∘ (· + dt)) v :=
  by
  rw [isMIntegralCurve_iff_isMIntegralCurveOn] at *
  simpa using hγ.comp_add dt

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