finSuccEquiv_symm_some

Mathlib.Logic.Equiv.Fin.Basic

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

English

The inverse of some m under finSuccEquiv(n) is m.succ.

Русский

Обратный образ some(m) функции finSuccEquiv(n) равен m.succ.

LaTeX

$$$$ \\forall m \\in \\mathrm{Fin}(n), \\; (\\mathrm{finSuccEquiv}(n)).\\mathrm{symm}(\\mathrm{some}(m)) = m.succ. $$$$

Lean4

@[simp]
theorem finSuccEquiv_symm_some (m : Fin n) : (finSuccEquiv n).symm (some m) = m.succ :=
  congr_fun Fin.succAbove_zero m

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

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

Разделы

Аффилиация

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