English
If two integral curves γ, γ' both solve the same velocity field on their respective Ioo domains and agree at a common time in the intersection, then the piecewise combination agrees with γ' on the intersection and with γ on the respective sides.
Русский
Если две интегральные кривые γ и γ' решают одно и то же поле скорости на своих доменах Ioo и совпадают в общую точку пересечения, то соответствующая кусочная кривая совпадает на соответствующих частях.
LaTeX
$$$EqOn((Ioo a b).piecewise γ γ', γ' , Ioo a' b')$ при условиях пересечения$$
Lean4
/-- The existence of a global integral curve is equivalent to the existence of a family of local
integral curves `γ : ℝ → ℝ → M` with the same starting point `γ 0 = x` such that each `γ a` is
defined on `Ioo (-a) a`. -/
theorem exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo [BoundarylessManifold I M]
(hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) (x : M) :
(∃ γ, γ 0 = x ∧ IsMIntegralCurve γ v) ↔ ∀ a, ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a) :=
by
refine ⟨fun ⟨γ, h1, h2⟩ _ ↦ ⟨γ, h1, h2.isMIntegralCurveOn _⟩, fun h ↦ ?_⟩
choose γ hγx hγ using h
exact
⟨fun t ↦ γ (|t| + 1) t, hγx (|0| + 1),
isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo hv γ hγx (fun a _ ↦ hγ a)⟩
