isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless

English

Global uniqueness on Ioo with contMDiff and boundaryless property implies γ = γ'.

Русский

Глобальная уникальность на Ioo с contMDiff и свойством без границы позволяет γ = γ'.

LaTeX

$$$\text{Boundaryless}(I,M) \Rightarrow IsMIntegralCurve_eq_of_contMDiff(\dots)$.$$

Lean4

theorem isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless [BoundarylessManifold I M] (ht₀ : t₀ ∈ Ioo a b)
    (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) (hγ : IsMIntegralCurveOn γ v (Ioo a b))
    (hγ' : IsMIntegralCurveOn γ' v (Ioo a b)) (h : γ t₀ = γ' t₀) : EqOn γ γ' (Ioo a b) :=
  isMIntegralCurveOn_Ioo_eqOn_of_contMDiff ht₀ (fun _ _ ↦ BoundarylessManifold.isInteriorPoint) hv hγ hγ' h

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