finSuccEquiv'_symm_some

Mathlib.Logic.Equiv.Fin.Basic

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

English

The inverse sends Some j to i.succAbove j: (finSuccEquiv' i).symm (Some j) = i.succAbove j.

Русский

Обратное отправляет Some j в i.succAbove j: (finSuccEquiv' i).symm (Some j) = i.succAbove j.

LaTeX

$$$(\\mathrm{finSuccEquiv'}\\ i).\\mathrm{symm}\\ (\\mathrm{Some}(j)) = i.\\mathrm{succAbove}(j)$$$

Lean4

@[simp]
theorem finSuccEquiv'_symm_some (i : Fin (n + 1)) (j : Fin n) : (finSuccEquiv' i).symm (some j) = i.succAbove j :=
  rfl

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

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

Разделы

Аффилиация

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