English
If a ≠ 0, the equivalence IsMIntegralCurveOn γ v s with γ∘(·*a) and a•v holds with the time-domain restriction {t | t*a ∈ s}. This expresses the nonzero-time-scaling behavior on domains.
Русский
Если a ≠ 0, равносильность IsMIntegralCurveOn γ v s с γ∘(·*a) и a•v держится на области {t | t*a ∈ s}. Это выражает поведение на ненулевых масштабированиях по области.
LaTeX
$$$IsMIntegralCurveOn(\\gamma, v, s) \\iff IsMIntegralCurveOn(\\gamma \\circ (\\cdot * a), a \\cdot v, {t | t * a \\in s})$$$
Lean4
theorem isMIntegralCurve_comp_mul_ne_zero {a : ℝ} (ha : a ≠ 0) :
IsMIntegralCurve γ v ↔ IsMIntegralCurve (γ ∘ (· * a)) (a • v) :=
by
refine ⟨fun hγ ↦ hγ.comp_mul _, fun hγ ↦ ?_⟩
convert hγ.comp_mul a⁻¹
· ext t
simp only [Function.comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]
· simp only [smul_smul, inv_mul_eq_div, div_self ha, one_smul]
