insertNthOrderIso_zero — Mathlib

English

The insertion-at-last position order isomorphism coincides with the snoc-order isomorphism when p is the last index.

Русский

Изоморфизм порядка вставки на последнюю позицию совпадает с изоморфизмом snoc, когда p — последний индекс.

LaTeX

$$$\text{insertNthOrderIso} \; \alpha \; \text{last}\; n = \text{snocOrderIso} \; \alpha$$$

Lean4

@[simp]
theorem insertNthOrderIso_zero (α : Fin (n + 1) → Type*) [∀ i, LE (α i)] : insertNthOrderIso α 0 = consOrderIso α := by
  ext; simp [insertNthOrderIso]

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