isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless

English

If two integral curves γ and γ′ agree at t0 within an interval Ioo, and γ, γ′ satisfy contMDiff, then they coincide on Ioo.

Русский

Если γ и γ′ совпадают в точке t0 внутри интервала Iоо, и удовлетворяют требованиям contMDiff, то они совпадают на Iоо.

LaTeX

$$$t_0 \in Ioo(a,b) \Rightarrow (\forall t \in Ioo(a,b),Is interior point) \Rightarrow γ|_{Ioo(a,b)}=γ'|_{Ioo(a,b)}$$$

Lean4

theorem isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless [BoundarylessManifold I M]
    (hv : ContMDiffAt I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)) (γ t₀)) (hγ : IsMIntegralCurveAt γ v t₀)
    (hγ' : IsMIntegralCurveAt γ' v t₀) (h : γ t₀ = γ' t₀) : γ =ᶠ[𝓝 t₀] γ' :=
  isMIntegralCurveAt_eventuallyEq_of_contMDiffAt BoundarylessManifold.isInteriorPoint hv hγ hγ' h

Похожие утверждения