removeNth_last

Mathlib.Data.Fin.Tuple.Basic

URI: https://scilib.ai/kg/mathlib#Fin.removeNth_last

English

Removing the last entry yields the initial segment: removeNth(last n) f = init f.

Русский

Удаление последнего элемента даёт начальный сегмент: removeNth(last n) f = init f.

LaTeX

$$removeNth\ (last\ n)\ f = init\ f$$

Lean4

@[simp]
theorem removeNth_last {α : Type*} (f : Fin (n + 1) → α) : removeNth (last n) f = init f := by ext;
  simp [init, removeNth]

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

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

Разделы

Аффилиация

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