asOrderHom — Mathlib

English

The m-simplices of the n-th standard simplex are precisely the monotone maps from Fin(m+1) to Fin(n+1).

Русский

m-симплекс n-го стандартного симплекса являются ровно монотонными отображениями Fin(m+1) → Fin(n+1).

LaTeX

$$$\alpha : Δ[n].obj m \quad \Longrightarrow\quad \alpha.down.toOrderHom : Fin(m.unop.len+1) \to Fin(n+1)$$$

Lean4

/-- The `m`-simplices of the `n`-th standard simplex are
the monotone maps from `Fin (m+1)` to `Fin (n+1)`. -/
def asOrderHom {n} {m} (α : Δ[n].obj m) : OrderHom (Fin (m.unop.len + 1)) (Fin (n + 1)) :=
  α.down.toOrderHom

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