mk_toOrderHom_apply

Mathlib.AlgebraicTopology.SimplexCategory.Defs

URI: https://scilib.ai/kg/mathlib#SimplexCategory.Hom.mk_toOrderHom_apply

← MathLib Explorer

English

Applying mk and then taking toOrderHom at a point i gives f(i).

Русский

Применение mk и затем взятие toOrderHom в точке i даёт f(i).

LaTeX

$$$(\\mathrm{mk} f).toOrderHom(i) = f(i)$$$

Lean4

theorem mk_toOrderHom_apply {a b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) (i : Fin (a.len + 1)) :
    (mk f).toOrderHom i = f i :=
  rfl

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

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

Разделы

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

Аффилиация

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