finSuccAboveOrderIso_symm_apply_last

English

Equality of the last-position insertion isomorphism with the snoc-order isomorphism.

Русский

Согласование вставки на последнюю позицию с изоморфизмом snoc.

LaTeX

$$$\operatorname{insertNthOrderIso}(\_, \operatorname{last}\ n) = \operatorname{snocOrderIso}(\_)$$$

Lean4

theorem finSuccAboveOrderIso_symm_apply_last (x : { x : Fin (n + 1) // x ≠ Fin.last n }) :
    (finSuccAboveOrderIso (Fin.last n)).symm x = Fin.castLT x.1 (Fin.val_lt_last x.2) :=
  by
  rw [← Option.some_inj]
  simp [finSuccAboveOrderIso, finSuccAboveEquiv, OrderIso.symm]

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