finSuccAboveOrderIso_apply — Mathlib

English

For any p in Fin(n+1), there is an order isomorphism between α p × (∀ i, α (p.succAbove i)) and ∀ i, α i.

Русский

Для любого p ∈ Fin(n+1) существует изоморфизм порядка между α p × (∀ i, α (p.succAbove i)) и ∀ i, α i.

LaTeX

$$$\alpha_p \times (\forall i:\mathrm{Fin} n, \alpha (p.succAbove i)) \cong_o (\forall i:\mathrm{Fin}(n+1), \alpha i)$$$

Lean4

theorem finSuccAboveOrderIso_apply (p : Fin (n + 1)) (i : Fin n) :
    finSuccAboveOrderIso p i = ⟨p.succAbove i, p.succAbove_ne i⟩ :=
  rfl

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