Theorems · Definition · ordinary differential equations

IsIntegralCurveAt

{E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E) → (ℝ → E → E) → ℝ → Prop

IsIntegralCurveAt γ v t₀ means γ : ℝ → E is a local integral curve of v in a neighbourhood containing t₀.

Defined in

Mathlib.Analysis.ODE.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace