comp_add — Mathlib

English

If γ is integral at t0, then γ shifted by dt is integral at t0−dt.

Русский

Если γ интегральна в точке t0, то γ сдвинутая на dt интегральна в точке t0−dt.

LaTeX

$$$\mathrm{IsMIntegralCurveAt}(\gamma,v,t_0) \Rightarrow \mathrm{IsMIntegralCurveAt}(\gamma\circ(\cdot+dt),v,t_0-dt).$$$

Lean4

theorem comp_add (hγ : IsMIntegralCurveAt γ v t₀) (dt : ℝ) : IsMIntegralCurveAt (γ ∘ (· + dt)) v (t₀ - dt) :=
  by
  rw [isMIntegralCurveAt_iff'] at *
  obtain ⟨ε, hε, h⟩ := hγ
  refine ⟨ε, hε, ?_⟩
  convert h.comp_add dt
  rw [Metric.ball]
  simp_rw [Metric.mem_ball, Real.dist_eq, ← sub_add, add_sub_right_comm]

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