isMIntegralCurveOn_comp_add — Mathlib

English

The forward and backward time-shifted integral-curve-on predicate are equivalent: shifting by dt yields the same class of integral curves.

Русский

Сдвиг по времени на dt сохраняет множество интегральных кривых: эквивалентность предикатов.

LaTeX

$$Iff(IsMIntegralCurveOn γ v s, IsMIntegralCurveOn (γ∘(·+dt)) v {t|t+dt∈s}).$$

Lean4

theorem isMIntegralCurveOn_comp_add {dt : ℝ} :
    IsMIntegralCurveOn γ v s ↔ IsMIntegralCurveOn (γ ∘ (· + dt)) v {t | t + dt ∈ s} :=
  by
  refine ⟨fun hγ ↦ hγ.comp_add _, fun hγ ↦ ?_⟩
  convert hγ.comp_add (-dt)
  · ext t
    simp
  · simp

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