IsMIntegralCurveAt — Mathlib

English

If γ is an integral curve for v, then γ is an integral curve on any subset s.

Русский

Если γ – интегральная кривая для вектора поля v, то она интегральна на любой подмножество s.

LaTeX

$$IsMIntegralCurveOn γ v s$$

Lean4

/-- If `v` is a vector field on `M` and `t₀ : ℝ`, `IsMIntegralCurveAt γ v t₀` means `γ : ℝ → M` is a
local integral curve of `v` in a neighbourhood containing `t₀`. The value of `γ` outside of this
interval is irrelevant and considered junk. -/
def IsMIntegralCurveAt (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (t₀ : ℝ) : Prop :=
  ∀ᶠ t in 𝓝 t₀, HasMFDerivAt 𝓘(ℝ, ℝ) I γ t ((1 : ℝ →L[ℝ] ℝ).smulRight <| v (γ t))

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