tail_cons

Mathlib.Data.Fin.Tuple.Embedding

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

English

Tail after cons recovers the original embedding: tail(cons x ha) = x.

Русский

После конструирования хвоста через cons получаем исходный x: tail(cons x ha) = x.

LaTeX

$$$\text{tail}(\text{cons } x\ ha) = x$$$

Lean4

theorem tail_cons {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : a ∉ range x) : tail (cons x ha) = x :=
  rfl

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

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

Разделы

Аффилиация

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