mkOfSucc_homToOrderHom_one — Mathlib

English

The value of the order-hom evaluated at 1 for mkOfSucc is i.succ, i.e., the right endpoint is sent to i+1 in the target Δ^n.

Русский

Значение отображения порядка на 1 для mkOfSucc равно i.succ, то есть правая граница отправляется в i+1 в Δ^n.

LaTeX

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

Lean4

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

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