picard_apply — Mathlib

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

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