English
The insertion-at-zero order isomorphism agrees with the cons-order isomorphism.
Русский
Изоморфизм порядка вставки на ноль согласуется с изоморфизмом cons.
LaTeX
$$$\text{insertNthOrderIso} \; \alpha \; 0 = \text{consOrderIso} \; \alpha$$$
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 `p`-th element of the tuple.
This is `Fin.insertNth` as an `OrderIso`. -/
@[simps!, simps toEquiv]
def insertNthOrderIso (α : Fin (n + 1) → Type*) [∀ i, LE (α i)] (p : Fin (n + 1)) :
α p × (∀ i, α (p.succAbove i)) ≃o ∀ i, α i
where
toEquiv := insertNthEquiv α p
map_rel_iff' := by simp [Pi.le_def, Prod.le_def, p.forall_iff_succAbove]
