English
Let two integral-curveOn families coincide at a point in an overlap interval Ioo, then they agree on that overlap interval; this is a uniqueness property of integral curves on Ioo-type domains.
Русский
Если две локальные интегральные кривые совпадают в точке пересечения внутри Ioo, они совпадают на всем пересечении; это свойство уникальности интегральных кривых на областях Ioo.
LaTeX
$$$\\text{EqOn}(\\gamma, \\gamma', Ioo(a,b) \\cap Ioo(a',b'))$ whenever they agree at a common point and are integral curves on respective domains$$
Lean4
/-- This is the uniqueness theorem of integral curves applied to a real-indexed family of integral
curves with the same starting point. -/
theorem eqOn_of_isMIntegralCurveOn_Ioo [BoundarylessManifold I M]
(hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) {x : M} (γ : ℝ → ℝ → M)
(hγx : ∀ a, γ a 0 = x) (hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)) {a a' : ℝ} (hpos : 0 < a')
(hle : a' ≤ a) : EqOn (γ a') (γ a) (Ioo (-a') a') :=
by
apply
isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless _ hv (hγ a' (by positivity))
((hγ a (lt_of_lt_of_le hpos hle)).mono _) (by rw [hγx a, hγx a'])
· rw [mem_Ioo]
exact ⟨neg_lt_zero.mpr hpos, by positivity⟩
· apply Ioo_subset_Ioo <;> linarith
