Theorems · Theorem · ordinary differential equations

ODE_solution_unique_of_mem_Icc

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {a b t₀ : ℝ},
  (∀ t ∈ Set.Ioo a b, LipschitzOnWith K (v t) (s t)) →
    t₀ ∈ Set.Ioo a b →
      ContinuousOn f (Set.Icc a b) →
        (∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t) →
          (∀ t ∈ Set.Ioo a b, f t ∈ s t) →
            ContinuousOn g (Set.Icc a b) →
              (∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t) →
                (∀ t ∈ Set.Ioo a b, g t ∈ s t) → f t₀ = g t₀ → Set.EqOn f g (Set.Icc a b)

A version of ODE_solution_unique_of_mem_Icc_right for uniqueness in a closed interval whose interior contains the initial time.

Defined in

Mathlib.Analysis.ODE.ExistUnique

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace