Theorems · Theorem · ordinary differential equations

isIntegralCurveAt_iff_exists_pos

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ},
  IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)

γ is an integral curve for v at t₀ iff γ is an integral curve on some interval containing t₀.

Defined in

Mathlib.Analysis.ODE.Basic

Cited by

1 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace