res_succ

Mathlib.Topology.MetricSpace.PiNat

URI: https://scilib.ai/kg/mathlib#PiNat.res_succ

English

res x (n+1) = x n :: res x n.

Русский

res x (n+1) = x(n) :: res x n.

LaTeX

$$$res(x,n+1)=x(n) :: res(x,n)$$$

Lean4

@[simp]
theorem res_succ (x : ℕ → α) (n : ℕ) : res x n.succ = x n :: res x n :=
  rfl

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

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

Разделы

Аффилиация

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