toContinuousMap_apply_eq_apply

Mathlib.Analysis.ODE.PicardLindelof

URI: https://scilib.ai/kg/mathlib#ODE.FunSpace.toContinuousMap_apply_eq_apply

English

For α in FunSpace and t in the domain, (α.toContinuousMap)(t) = α(t).

Русский

Для $\\alpha$ в пространстве функций и $t$ из области, выполнено $(\\alpha^{\\mathrm{toContinuousMap}})(t)=\\alpha(t)$.

LaTeX

$$$\\alpha^{\\mathrm{toContinuousMap}}(t)=\\alpha(t)$$$

Lean4

@[simp]
theorem toContinuousMap_apply_eq_apply (α : FunSpace t₀ x₀ r L) (t : Icc tmin tmax) : α.toContinuousMap t = α t :=
  rfl

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

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

Разделы

Аффилиация

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