standardσ_nil

Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

URI: https://scilib.ai/kg/mathlib#SimplexCategoryGenRel.standardσ_nil

English

The standardσ of an empty list is the identity morphism.

Русский

Стандартное σ для пустого списка равно единичному морфизму.

LaTeX

$$$\\\\text{standardσ}([\,\\\\]) = id$$$

Lean4

@[simp]
theorem standardσ_nil (m : ℕ) : standardσ .nil (by grind) = 𝟙 (mk m) :=
  rfl

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

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

Разделы

Аффилиация

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