Theorems · Theorem · ordinary differential equations

IsPicardLindelof.of_contDiffAt_one

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → E} {x₀ : E},
  ContDiffAt ℝ 1 f x₀ →
    ∃ ε, ∃ (hε : 0 < ε), ∃ a r L K, ∃ (_ : 0 < r), ∀ (t₀ : ℝ), IsPicardLindelof (fun x => f) ⟨t₀, ⋯⟩ x₀ a r L K

A time-independent, continuously differentiable ODE satisfies the hypotheses of the Picard-Lindelöf theorem.

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace