res_zero

Mathlib.Topology.MetricSpace.PiNat

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

English

For any x, res x 0 = nil (empty list).

Русский

Для любой последовательности x, res x 0 = пустой список.

LaTeX

$$$res\\ x\\ 0 = []$$$

Lean4

@[simp]
theorem res_zero (x : ℕ → α) : res x 0 = @nil α :=
  rfl

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

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

Разделы

Аффилиация

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