ofFn_cons

Mathlib.Data.List.OfFn

URI: https://scilib.ai/kg/mathlib#List.ofFn_cons

English

The list built from Fin.cons a f equals a :: List.ofFn f.

Русский

Список, получаемый из Fin.cons a f, равен a :: List.ofFn f.

LaTeX

$$$ \\operatorname{List.ofFn} (\\operatorname{Fin.cons} a\ \\\\; f) = a :: \\operatorname{List.ofFn} f $$$

Lean4

theorem ofFn_cons {n} (a : α) (f : Fin n → α) : ofFn (Fin.cons a f) = a :: ofFn f :=
  by
  rw [ofFn_succ]
  rfl

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

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

Разделы

Аффилиация

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