init_snoc

Mathlib.Data.Fin.Tuple.Basic

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

← MathLib Explorer

English

snoc(p,x) evaluated at i.castSucc equals p(i).

Русский

snoc(p,x) в позиции i.castSucc даёт p i.

LaTeX

$$$\\mathrm{snoc}\\ p\\ x\\ i.castSucc = p\\ i$$$

Lean4

@[simp]
theorem init_snoc : init (snoc p x) = p := by
  ext i
  simp only [init, snoc, coe_castSucc, is_lt, cast_eq, dite_true]
  convert cast_eq rfl (p i)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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