English
For any p in Fin(n+1), there is an order isomorphism between α p × (∀ i, α (p.succAbove i)) and ∀ i, α i, splitting at position p.
Русский
Для любого p в Fin(n+1) существует порядок-изоморфизм между α p × (∀ i, α (p.succAbove i)) и ∀ i, α i, разделяющий последовательность на позицию p.
LaTeX
$$$\alpha_p \times (\forall i:\mathrm{Fin} n, \alpha (p.succAbove i)) \cong_o (\forall i:\mathrm{Fin}(n+1), \alpha i)$$$
Lean4
/-- Order isomorphism between tuples of length `n + 1` and pairs of an element and a tuple of length
`n` given by separating out the last element of the tuple.
This is `Fin.snoc` as an `OrderIso`. -/
@[simps!, simps toEquiv]
def snocOrderIso (α : Fin (n + 1) → Type*) [∀ i, LE (α i)] : α (last n) × (∀ i, α (castSucc i)) ≃o ∀ i, α i
where
toEquiv := snocEquiv α
map_rel_iff' := by simp [Pi.le_def, Prod.le_def, forall_iff_castSucc]
