finSuccEquiv_succ

Mathlib.Logic.Equiv.Fin.Basic

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

English

For every n and every m ∈ Fin(n), finSuccEquiv(n) maps m.succ to some m.

Русский

Для каждого n и каждого m ∈ Fin(n) функция finSuccEquiv(n) отображает m.succ в some(m).

LaTeX

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

Lean4

@[simp]
theorem finSuccEquiv_succ (m : Fin n) : (finSuccEquiv n) m.succ = some m :=
  finSuccEquiv'_above (Fin.zero_le _)

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

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

Разделы

Аффилиация

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