comp_add — Mathlib

English

If γ is an integral curve on s, then γ∘(·+dt) is an integral curve on s translated by dt.

Русский

Если γ интегральная кривая на s, то γ( t+dt ) — интегральная кривая на s+dt.

LaTeX

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

Lean4

theorem comp_add (hγ : IsMIntegralCurveOn γ v s) (dt : ℝ) : IsMIntegralCurveOn (γ ∘ (· + dt)) v {t | t + dt ∈ s} :=
  by
  intro t ht
  rw [comp_apply, ← ContinuousLinearMap.comp_id (ContinuousLinearMap.smulRight 1 (v (γ (t + dt))))]
  apply HasMFDerivWithinAt.comp t (hγ (t + dt) ht) _ subset_rfl
  refine ⟨(continuous_add_right _).continuousWithinAt, ?_⟩
  simp only [mfld_simps]
  exact (hasFDerivWithinAt_id _ _).add_const _

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