snoc_last

Mathlib.Data.Fin.Tuple.Embedding

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

English

The last element of a snoc-constructed embedding equals the appended element a.

Русский

Последний элемент snoc-embedded отображения равен добавленному элементу a.

LaTeX

$$$\text{snoc}_{n} (x) (\mathrm{last}\,n) = a$$$

Lean4

theorem snoc_last {n : ℕ} {x : Fin n ↪ α} {a : α} {ha : a ∉ range x} : snoc x ha (last n) = a := by
  rw [coe_snoc, Fin.snoc_last]

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

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

Разделы

Аффилиация

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