head

Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

URI: https://scilib.ai/kg/mathlib#SimplexCategoryGenRel.IsAdmissible.head

← MathLib Explorer

English

The head of an m-admissible list, as an element of Fin(m+1), is the first entry a.

Русский

Голова m-допустимого списка, как элемент Fin(m+1), равна первой записи a.

LaTeX

$$$\\\\text{Head}(a,L) = a \\\\text{ in } Fin(m+1).$$$

Lean4

/-- The head of an `m`-admissible list. -/
@[simps!]
def head (a : ℕ) (L : List ℕ) (hl : IsAdmissible m (a :: L)) : Fin (m + 1) :=
  hl.getElemAsFin 0 (by simp)

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

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

Разделы

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

Аффилиация

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