comp_mul — Mathlib

English

For any a ≠ 0, IsMIntegralCurve γ v t0 is equivalent to IsMIntegralCurve (γ ∘ (· * a)) (a • v) (t0 / a).

Русский

Для любого a ≠ 0: IsMIntegralCurve γ v t0 ⇔ IsMIntegralCurve (γ ∘ (· * a)) (a • v) (t0 / a).

LaTeX

$$$IsMIntegralCurve(\\gamma, v, t_0) \\iff IsMIntegralCurve(\\gamma \\circ (\\cdot * a), a \\cdot v, t_0 / a)$$$

Lean4

theorem comp_mul (hγ : IsMIntegralCurve γ v) (a : ℝ) : IsMIntegralCurve (γ ∘ (· * a)) (a • v) :=
  by
  rw [isMIntegralCurve_iff_isMIntegralCurveOn] at *
  exact hγ.comp_mul _

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