exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless

English

On a boundaryless manifold, a C1 vector field yields a local integral curve at an interior point of the initial point.

Русский

На безграничном многообразии векторное поле порождает локальную интегральную кривую в внутренней точке начальной точки.

LaTeX

$$$\exists \gamma:\mathbb{R}\to M,\; \gamma(t_0)=x_0 \land IsMIntegralCurveAt(\gamma,v,t_0).$$$

Lean4

/-- Existence of local integral curves for a $C^1$ vector field on a `C^1` manifold without
boundary. -/
theorem exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless [CompleteSpace E] [BoundarylessManifold I M]
    (hv : ContMDiffAt I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)) x₀) :
    ∃ γ : ℝ → M, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀ :=
  exists_isMIntegralCurveAt_of_contMDiffAt t₀ hv BoundarylessManifold.isInteriorPoint

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