Theorems · Definition · ordinary differential equations

ODE.FunSpace.casesOn

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} →
      {t₀ : ↑(Set.Icc tmin tmax)} →
        {x₀ : E} →
          {r L : NNReal} →
            {motive : ODE.FunSpace t₀ x₀ r L → Sort u} →
              (t : ODE.FunSpace t₀ x₀ r L) →
                ((toFun : ↑(Set.Icc tmin tmax) → E) →
                    (lipschitzWith : LipschitzWith L toFun) →
                      (mem_closedBall₀ : toFun t₀ ∈ Metric.closedBall x₀ ↑r) →
                        motive { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ }) →
                  motive t

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup