compProj_val

Mathlib.Analysis.ODE.PicardLindelof

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

English

For α in FunSpace and t ∈ Icc tmin tmax, α.compProj t = α t.

Русский

Для каждого α и для всех t из Icc tmin tmax верно α.compProj t = α t.

LaTeX

$$∀ t ∈ Icc tmin tmax, α.compProj t = α t.$$

Lean4

theorem compProj_val {α : FunSpace t₀ x₀ r L} {t : Icc tmin tmax} : α.compProj t = α t := by
  simp only [compProj_apply, projIcc_val]

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

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

Разделы

Аффилиация

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