Theorems · Definition · ordinary differential equations

ODE.FunSpace.toFun

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} →
      {t₀ : ↑(Set.Icc tmin tmax)} → {x₀ : E} → {r L : NNReal} → ODE.FunSpace t₀ x₀ r L → ↑(Set.Icc tmin tmax) → E

The domain is Icc tmin tmax.

Defined in: Mathlib.Analysis.ODE.PicardLindelof
Cited by: 20 results in Mathlib
Foundations: Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
Set.Elemstatement and proof · cited by 7,166
NNRealstatement and proof · cited by 4,310
Set.Iccstatement and proof · cited by 1,702
ODE.FunSpacestatement and proof · cited by 37

Cited by22

Results whose statement or proof uses this declaration.

ODE.FunSpace.compProjproof · cited by 13
ODE.FunSpace.toContinuousMapproof · cited by 6
ODE.FunSpace.next_applystatement · cited by 5
ODE.FunSpace.compProj_applystatement · cited by 3
ODE.FunSpace.compProj_of_memstatement and proof · cited by 3
ODE.FunSpace.mem_closedBallstatement and proof · cited by 3
ODE.FunSpace.compProj_valstatement and proof · cited by 2
ODE.FunSpace.extstatement and proof · cited by 2
ODE.FunSpace.lipschitzWithstatement · cited by 2
ODE.FunSpace.mem_closedBall₀statement · cited by 2
ODE.FunSpace.next_apply₀statement · cited by 2
IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAtproof · cited by 2