const_comp

Mathlib.AlgebraicTopology.SimplexCategory.Basic

URI: https://scilib.ai/kg/mathlib#SimplexCategory.const_comp

← MathLib Explorer

English

The mkHom construction coincides with the standard mk on Hom in SimplexCategory.

Русский

Конструкция mkHom совпадает со стандартной mk на Hom в SimplexCategory.

LaTeX

$$$\\text{mkHom}(f) = \\text{SimplexCategory.Hom.mk}(f).$$$

Lean4

@[simp]
theorem const_comp (x : SimplexCategory) {y z : SimplexCategory} (f : y ⟶ z) (i : Fin (y.len + 1)) :
    const x y i ≫ f = const x z (f.toOrderHom i) :=
  rfl

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

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

Разделы

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

Аффилиация

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