IsMIntegralCurve — Mathlib

English

A curve is integral at t0 iff there exists a neighborhood around t0 on which it is integral.

Русский

Кривая интегрирует в точке t0 тогда и только тогда, когда существует окрестность t0, на которой она интегрируема.

LaTeX

$$isMIntegralCurveAt_iff : IsMIntegralCurveAt γ v t0 ↔ ∃ s ∈ nhds t0, IsMIntegralCurveOn γ v s$$

Lean4

/-- If `v : M → TM` is a vector field on `M`, `IsMIntegralCurve γ v` means `γ : ℝ → M` is a global
integral curve of `v`. That is, `γ t` is tangent to `v (γ t)` for all `t : ℝ`. -/
def IsMIntegralCurve (γ : ℝ → M) (v : (x : M) → TangentSpace I x) : Prop :=
  ∀ t : ℝ, HasMFDerivAt 𝓘(ℝ, ℝ) I γ t ((1 : ℝ →L[ℝ] ℝ).smulRight (v (γ t)))

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