English
If a ≠ 0, IsMIntegralCurveOn γ v s is equivalent to IsMIntegralCurveOn (γ ∘ (·*a)) (a•v) on {t | t*a ∈ s}. This shows how integral-curve behavior scales with nonzero time dilation.
Русский
Если a ≠ 0, IsMIntegralCurveOn γ v s эквивалентно IsMIntegralCurveOn (γ ∘ (·*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 isMIntegralCurveOn_comp_mul_ne_zero {a : ℝ} (ha : a ≠ 0) :
IsMIntegralCurveOn γ v s ↔ IsMIntegralCurveOn (γ ∘ (· * a)) (a • v) {t | t * a ∈ s} :=
by
refine ⟨fun hγ ↦ hγ.comp_mul a, 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]
· simp only [mem_setOf_eq, mul_assoc, inv_mul_eq_div, div_self ha, mul_one, setOf_mem_eq]
