isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless

English

On a boundaryless manifold, γ and γ′ that are contMDiff and integral on Ioo are equal on Ioo.

Русский

На границе без границ κривые γ и γ′, удовлетворяющие contMDiff и интегральности на Ioo, совпадают на Ioo.

LaTeX

$$$\text{Boundaryless}(I,M) \Rightarrow isMIntegralCurve_Ioo_eq_of_contMDiff(γ,γ',...)$$$

Lean4

theorem isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless [BoundarylessManifold I M]
    (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) (hγ : IsMIntegralCurve γ v)
    (hγ' : IsMIntegralCurve γ' v) (h : γ t₀ = γ' t₀) : γ = γ' :=
  isMIntegralCurve_eq_of_contMDiff (fun _ ↦ BoundarylessManifold.isInteriorPoint) hv hγ hγ' h

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