finSuccEquiv'_symm_none

Mathlib.Logic.Equiv.Fin.Basic

URI: https://scilib.ai/kg/mathlib#finSuccEquiv'_symm_none

English

The inverse at None is the original index: (finSuccEquiv' i).symm none = i.

Русский

Обратное к None даёт исходный элемент: (finSuccEquiv' i).symm none = i.

LaTeX

$$$(\\mathrm{finSuccEquiv'}\\ i).\\mathrm{symm}\\ \\mathrm{none} = i$$$

Lean4

@[simp]
theorem finSuccEquiv'_symm_none (i : Fin (n + 1)) : (finSuccEquiv' i).symm none = i :=
  rfl

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

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

Разделы

Аффилиация

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