Theorems · Definition · ordinary differential equations

ODE.FunSpace.compProj

{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 → ℝ → E

Extend the domain of α from Icc tmin tmax to ℝ such that α t = α tmin for all t ≤ tmin and α t = α tmax for all t ≥ tmax.

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

13 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup