castOrderIso — Mathlib

English

The castOrderIso is an order isomorphism between Fin n and Fin m whenever n = m.

Русский

castOrderIso образует упорядоченный изоморфизм между Fin(n) и Fin(m), когда n = m.

LaTeX

$$$\forall {n m : \mathbb{N}}, (h : n = m) \Rightarrow \mathrm{Fin}(n) \cong_o \mathrm{Fin}(m)$$$

Lean4

/-- `Fin.cast` as an `OrderIso`.

`castOrderIso eq i` embeds `i` into an equal `Fin` type. -/
@[simps]
def castOrderIso (eq : n = m) : Fin n ≃o Fin m
    where
  toEquiv := ⟨Fin.cast eq, Fin.cast eq.symm, leftInverse_cast eq, rightInverse_cast eq⟩
  map_rel_iff' := cast_le_cast eq

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