init_snoc

Mathlib.Data.Fin.Tuple.Embedding

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

English

Init and snoc interact so that init(snoc x ha) = x, illustrating the compatibility of begin/end trimming with appending.

Русский

Инициация и добавление элементы согласуются: init(snoc x ha) = x.

LaTeX

$$$\text{init}(\text{snoc } x\ ha) = x$$$

Lean4

theorem init_snoc {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : a ∉ range x) : init (snoc x ha) = x := by simp [snoc, init]

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

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

Разделы

Аффилиация

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