English
Two global integral curves with the same initial point coincide.
Русский
Две глобальные интегральные кривые с одинаковой начальнной точкой совпадают.
LaTeX
$$$\gamma(t_0)=\gamma'(t_0) \Rightarrow \gamma=\gamma'.$$$
Lean4
/-- Global integral curves are unique.
If a continuously differentiable vector field `v` admits two global integral curves
`γ γ' : ℝ → M`, and `γ t₀ = γ' t₀` for some `t₀`, then `γ` and `γ'` are equal. -/
theorem isMIntegralCurve_eq_of_contMDiff (hγt : ∀ t, I.IsInteriorPoint (γ t))
(hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) (hγ : IsMIntegralCurve γ v)
(hγ' : IsMIntegralCurve γ' v) (h : γ t₀ = γ' t₀) : γ = γ' :=
by
ext t
obtain ⟨T, ht₀, ht⟩ : ∃ T, t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T :=
by
obtain ⟨T, hT₁, hT₂⟩ := exists_abs_lt t
obtain ⟨hT₂, hT₃⟩ := abs_lt.mp hT₂
obtain ⟨S, hS₁, hS₂⟩ := exists_abs_lt t₀
obtain ⟨hS₂, hS₃⟩ := abs_lt.mp hS₂
exact ⟨T + S, by constructor <;> constructor <;> linarith⟩
exact
isMIntegralCurveOn_Ioo_eqOn_of_contMDiff ht (fun t _ ↦ hγt t) hv ((hγ.isMIntegralCurveOn _).mono (subset_univ _))
((hγ'.isMIntegralCurveOn _).mono (subset_univ _)) h ht₀
