coe_tail

Mathlib.Data.Fin.Tuple.Embedding

URI: https://scilib.ai/kg/mathlib#Fin.Embedding.coe_tail

English

The canonical coercion of tail equals the standard tail function on Fin-n tuples.

Русский

Стандартное отображение коэрции хвоста совпадает с обычной функцией хвоста.

LaTeX

$$$\uparrow(\text{tail } x) = \text{Fin.tail } x$$$

Lean4

@[simp, norm_cast]
theorem coe_tail {n : ℕ} (x : Fin (n + 1) ↪ α) : ↑(tail x) = Fin.tail x :=
  rfl

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

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

Разделы

Аффилиация

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