finSuccEquivLast_symm_none

Mathlib.Logic.Equiv.Fin.Basic

URI: https://scilib.ai/kg/mathlib#finSuccEquivLast_symm_none

English

The inverse of none under finSuccEquivLast is Fin.last n.

Русский

Обратное отображение none через finSuccEquivLast дает Fin.last n.

LaTeX

$$$$ \\mathrm{finSuccEquivLast}.\\mathrm{symm}(\\mathrm{none}) = \\mathrm{Fin.last}(n). $$$$

Lean4

@[simp]
theorem finSuccEquivLast_symm_none : finSuccEquivLast.symm none = Fin.last n :=
  finSuccEquiv'_symm_none _

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

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

Разделы

Аффилиация

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