finSuccAboveOrderIso_symm_apply_ne_last

English

Promote a finite index n into a larger Fin m while preserving the underlying order; this is the order-preserving embedding.

Русский

Переход от Fin n к Fin m с сохранением порядка; это вложение, сохраняющее порядок.

LaTeX

$$$\text{castLEOrderIso} : (n \le m) \to (Fin n \simeq_o { i: Fin m // i < n })$$$

Lean4

theorem finSuccAboveOrderIso_symm_apply_ne_last {p : Fin (n + 1)} (h : p ≠ Fin.last n)
    (x : { x : Fin (n + 1) // x ≠ p }) : (finSuccAboveEquiv p).symm x = (p.castLT (Fin.val_lt_last h)).predAbove x :=
  by
  rw [← Option.some_inj]
  simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_ne_last_apply h x.property

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