Theorems · Theorem · ordinary differential equations

IsPicardLindelof.weaken_lipschitz

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal}, IsPicardLindelof f t₀ x₀ a r L K → ∀ {K' : NNReal}, K ≤ K' → IsPicardLindelof f t₀ x₀ a r L K'

IsPicardLindelof is preserved when enlarging the Lipschitz constant K.

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup