toOrderHom_mk

Mathlib.AlgebraicTopology.SimplexCategory.Defs

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

English

For any f, the underlying order map of mk f equals f.

Русский

Для любого f базовый отображение mk f равно f.

LaTeX

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

Lean4

@[simp]
theorem toOrderHom_mk {a b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) : (mk f).toOrderHom = f :=
  rfl

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

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

Разделы

Аффилиация

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