English
For any t, picard(f, t0, x0, α)(t) equals x0 plus the integral ∫_{t0}^{t} f(τ, α(τ)) dτ.
Русский
Для любого t выполняется равенство $\\operatorname{picard}(f,t_0,x_0,\\alpha)(t)=x_0+\\int_{t_0}^{t} f(\\tau,\\alpha(\\tau)) \\, d\\tau$.
LaTeX
$$$\\operatorname{picard}(f,t_0,x_0,\\alpha)(t) = x_0 + \\int_{t_0}^{t} f(\\tau,\\alpha(\\tau)) \\, d\\tau$$$
Lean4
@[simp]
theorem picard_apply {x₀ : E} {t : ℝ} : picard f t₀ x₀ α t = x₀ + ∫ τ in t₀..t, f τ (α τ) :=
rfl