isMIntegralCurveOn_comp_sub — Mathlib

English

The equivalence with negative time shift: IsMIntegralCurveOn γ v s is equivalent to IsMIntegralCurveOn(γ∘(·−dt)) v on {t|t−dt∈s}.

Русский

Эквивалентность с обратным сдвигом по времени: IsMIntegralCurveOn(γ,v,s) эквивалентно IsMIntegralCurveOn(γ∘(−dt), v) на {t| t−dt∈s}.

LaTeX

$$$\mathrm{IsMIntegralCurveOn}(\gamma,v,s) \iff \mathrm{IsMIntegralCurveOn}(\gamma\circ(\cdot-dt),v,\{t\mid t-dt\in s\}).$$$

Lean4

theorem isMIntegralCurveOn_comp_sub {dt : ℝ} :
    IsMIntegralCurveOn γ v s ↔ IsMIntegralCurveOn (γ ∘ (· - dt)) v {t | t - dt ∈ s} := by
  simpa using isMIntegralCurveOn_comp_add (dt := -dt)

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