toSimplexCategory_len

Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

URI: https://scilib.ai/kg/mathlib#SimplexCategoryGenRel.toSimplexCategory_len

English

The length of a simplex is preserved by the toSimplexCategory functor: (toSimplexCategory.obj x).len = x.len.

Русский

Длина простейшего сохраняется под функтором: (toSimplexCategory.obj x).len = x.len.

LaTeX

$$$\bigl( toSimplexCategory.obj(x) \bigr).\mathrm{len} = x.\mathrm{len}$$$

Lean4

@[simp]
theorem toSimplexCategory_len {x : SimplexCategoryGenRel} : (toSimplexCategory.obj x).len = x.len :=
  rfl

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

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

Разделы

Аффилиация

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