picard_apply₀

Mathlib.Analysis.ODE.PicardLindelof

URI: https://scilib.ai/kg/mathlib#ODE.picard_apply₀

English

At the initial time t0, the Picard iteration returns the initial value: picard(f, t0, x0, α)(t0) = x0.

Русский

В начальный момент t0 итерация Пикара возвращает начальное значение: picard(f, t0, x0, α)(t0) = x0.

LaTeX

$$$\\operatorname{picard}(f,t_0,x_0,\\alpha)(t_0) = x_0$$$

Lean4

theorem picard_apply₀ {x₀ : E} : picard f t₀ x₀ α t₀ = x₀ := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru