revOrderIso_symm_apply

Mathlib.Order.Fin.Basic

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

English

The inverse of revOrderIso applied to i equals OrderDual.toDual (rev i).

Русский

Обратное revOrderIso применено к i равно OrderDual.toDual (rev i).

LaTeX

$$$\forall {i : \mathrm{Fin}(n)}, revOrderIso^{-1}(i) = OrderDual.toDual (rev(i))$$$

Lean4

@[simp]
theorem revOrderIso_symm_apply (i : Fin n) : revOrderIso.symm i = OrderDual.toDual (rev i) :=
  rfl

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

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

Разделы

Аффилиация

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