exists_eq_forall_mem_Icc_hasDerivWithinAt₀

English

In the autonomous time-independent case, there exists α with α(t0) = x0 and HasDerivWithinAt α(t) = f(α(t)) on Icc(tmin,tmax).

Русский

Автономный случай: существует α с α(t0)=x0 и HasDerivWithinAt α(t) = f(α(t)) на Icc(tmin,tmax).

LaTeX

$$$\\exists α:\\; α(t_0)=x_0 \\land \\forall t\\in Icc(t_{min},t_{max}),\\ HasDerivWithinAt(α(t))\\ (f(α(t))).$$$

Lean4

/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, differential form. -/
theorem exists_eq_forall_mem_Icc_hasDerivWithinAt₀ (hf : IsPicardLindelof f t₀ x₀ a 0 L K) :
    ∃ α : ℝ → E, α t₀ = x₀ ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t :=
  exists_eq_forall_mem_Icc_hasDerivWithinAt hf (mem_closedBall_self le_rfl)

Похожие утверждения