English
There exists a nonnegative bound L' such that for any x,y within the closed ball and α,β fixed by next, the pointwise distance dist α β is bounded by L' times the distance between x and y.
Русский
Существует неотриценная константа L' такая, что для любых x,y в шаре и любых зафиксированных α,β, расстояние между α и β не превосходит L' умноженное на расстояние между x и y.
LaTeX
$$$\\exists L'\\ge 0:\\ \\forall x,y\\in\\overline{B}(x_0,r),\\forall α,β:\\ IsFixedPt(\\text{next } hf hx) α, IsFixedPt(\\text{next } hf hy) β,\\ dist α β \\le L' \\ dist x y.$$$
Lean4
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, differential form. This version shows the
existence of a local flow. -/
theorem exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt (hf : IsPicardLindelof f t₀ x₀ a r L K) :
∃ α : E → ℝ → E,
∀ x ∈ closedBall x₀ r, α x t₀ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t :=
have ⟨α, hα⟩ := exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith hf
⟨α, hα.1⟩
