coe_snoc

Mathlib.Data.Fin.Tuple.Embedding

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

English

The canonical coe of the snoc embedding equals the explicit snoc construction on the underlying tuple.

Русский

Коэрция snoc-embedding совпадает с явной конструкцией snoc на базе кортежа.

LaTeX

$$$\text{coe}(\text{snoc } x ha) = \text{Fin.snoc } (\text{coeff } x) a$$$

Lean4

@[simp, norm_cast]
theorem coe_snoc {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : a ∉ range x) : ↑(snoc x ha) = Fin.snoc x a :=
  rfl

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

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

Разделы

Аффилиация

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