revOrderIso

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.revOrderIso

← MathLib Explorer

English

The reverse (order dual) of Fin n is order-isomorphic to Fin n via revOrderIso.

Русский

Обратное упорядочение Fin n эквивалентно Fin n через revOrderIso.

LaTeX

$$$\mathrm{Fin}(n)^{\mathrm{op}} \cong_o \mathrm{Fin}(n)$$$

Lean4

/-- `Fin.rev n` as an order-reversing isomorphism. -/
@[simps! apply toEquiv]
def revOrderIso : (Fin n)ᵒᵈ ≃o Fin n :=
  ⟨OrderDual.ofDual.trans revPerm, rev_le_rev⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru