finSuccEquiv'_zero

Mathlib.Logic.Equiv.Fin.Basic

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

English

finSuccEquiv' (0) equals finSuccEquiv(n).

Русский

finSuccEquiv'(0) равна finSuccEquiv(n).

LaTeX

$$$$ \\mathrm{finSuccEquiv}'(0) = \\mathrm{finSuccEquiv}(n). $$$$

Lean4

/-- The equiv version of `Fin.predAbove_zero`. -/
theorem finSuccEquiv'_zero : finSuccEquiv' (0 : Fin (n + 1)) = finSuccEquiv n :=
  rfl

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

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

Разделы

Аффилиация

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