English
There is an order isomorphism between α0 × (∀ i, α (succ i)) and ∀ i, α i, given by splitting the first element from the rest.
Русский
Существует порядок-изоморфизм между α0 × (∀ i, α (succ i)) и ∀ i, α i, который разделяет первый элемент от остатка.
LaTeX
$$$\alpha_0 \times (\forall i:\mathrm{Fin} n, \alpha (succ\,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 first element of the tuple.
This is `Fin.cons` as an `OrderIso`. -/
@[simps!, simps toEquiv]
def consOrderIso (α : Fin (n + 1) → Type*) [∀ i, LE (α i)] : α 0 × (∀ i, α (succ i)) ≃o ∀ i, α i
where
toEquiv := consEquiv α
map_rel_iff' := forall_iff_succ
