const_down_toOrderHom — Mathlib

English

The down map of const n k is the constant order-hom at k; i.e., (const n k m).down.toOrderHom = OrderHom.const k.

Русский

Уменьшение константного отображения доOrderHom равно константному order-hom на k.

LaTeX

$$$(const\ n\ k\ m).down.toOrderHom = OrderHom.const\ _ k$$$

Lean4

@[simp]
theorem const_down_toOrderHom (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ) :
    (const n k m).down.toOrderHom = OrderHom.const _ k :=
  rfl

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