Mathlib Map

Theorems · Theorem · ordinary differential equations

ODE.FunSpace.lipschitzWith

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  (self : ODE.FunSpace t₀ x₀ r L), LipschitzWith L self.toFun
Defined in
Mathlib.Analysis.ODE.PicardLindelof
Cited by
2 results in Mathlib
Foundations
Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedAddCommGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ODE.FunSpace.mem_closedBall · cited by 3FunSpace.mem_closedBallODE.FunSpace.continuous · cited by 1FunSpace.continuousSet · cited by 53352SetReal · cited by 25697RealNormedAddCommGroup · cited by 15752NormedAddCommGroupSet.Elem · cited by 7166Set.ElemNNReal · cited by 4310NNRealSet.Icc · cited by 1702Set.IccLipschitzWith · cited by 316LipschitzWithODE.FunSpace · cited by 37ODE.FunSpaceODE.FunSpace.toFun · cited by 20FunSpace.toFunFunSpace.lipschitzWithCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.