English
An isomorphism e: x ≅ y in SimplexCategory induces an order-iso between Fin(x.len + 1) and Fin(y.len + 1).
Русский
Изоморфизм e: x ≅ y в SimplexCategory индуцирует порядка-изоморфизм между Fin(x.len + 1) и Fin(y.len + 1).
LaTeX
$$$\\mathrm{orderIsoOfIso}(x,y,e) : \\mathrm{Fin}(x.len+1) \\simeq_{\\text{ord}} \\mathrm{Fin}(y.len+1)$$$
Lean4
/-- An isomorphism in `SimplexCategory` induces an `OrderIso`. -/
@[simp]
def orderIsoOfIso {x y : SimplexCategory} (e : x ≅ y) : Fin (x.len + 1) ≃o Fin (y.len + 1) :=
Equiv.toOrderIso
{ toFun := e.hom.toOrderHom
invFun := e.inv.toOrderHom
left_inv := fun i => by simpa only using congr_arg (fun φ => (Hom.toOrderHom φ) i) e.hom_inv_id
right_inv := fun i => by simpa only using congr_arg (fun φ => (Hom.toOrderHom φ) i) e.inv_hom_id }
e.hom.toOrderHom.monotone e.inv.toOrderHom.monotone
