mkOfSucc_homToOrderHom_zero — Mathlib

English

The value of the order-hom evaluated at 0 for mkOfSucc is i.castSucc, i.e., the left endpoint is sent to i in the target structure Δ^n.

Русский

Значение соответствующего отображения порядка на 0 для mkOfSucc равно i.castSucc, то есть левая граница отправляется в i в Δ^n.

LaTeX

$$$\text{(OrderHom).coe} (\mathrm{Hom.toOrderHom} (\mathrm{mkOfSucc}\, i))\ 0 = i.{\text{castSucc}}$$$

Lean4

@[simp]
theorem mkOfSucc_homToOrderHom_zero {n} (i : Fin n) :
    DFunLike.coe (F := Fin 2 →o Fin (n + 1)) (Hom.toOrderHom (mkOfSucc i)) 0 = i.castSucc :=
  rfl

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