len

Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

URI: https://scilib.ai/kg/mathlib#FreeSimplexQuiver.len

English

There is a canonical way to recover the natural number from a FreeSimplexQuiver object, via len.

Русский

Существует канонический способ восстановить натуральное число из объекта FreeSimplexQuiver с помощью функции len.

LaTeX

$$$$ \\mathrm{len}(x) = x $$$$

Lean4

/-- Getting back the natural number from the objects. -/
def len (x : FreeSimplexQuiver) : ℕ :=
  x

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

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

Разделы

Аффилиация

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