toOrderHom — Mathlib

English

Recover the monotone map from a morphism in the simplex category; it is the same as the underlying order-preserving map.

Русский

Из морфизма в SimplexCategory восстанавливается монотонное отображение; оно совпадает с базовым монотонным отображением.

LaTeX

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

Lean4

/-- Recover the monotone map from a morphism in the simplex category. -/
def toOrderHom {a b : SimplexCategory} (f : SimplexCategory.Hom a b) : Fin (a.len + 1) →o Fin (b.len + 1) :=
  f

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