succ_predAbove_zero

Mathlib.Data.Fin.SuccPred

URI: https://scilib.ai/kg/mathlib#Fin.succ_predAbove_zero

English

For any j ∈ Fin(n+1) with NeZero n, succ (predAbove 0 j) = j.

Русский

Для любого j ∈ Fin(n+1) при NeZero n, succ (predAbove 0 j) = j.

LaTeX

$$$ \\forall j \\in \\mathrm{Fin}(n+1),\\ Succ(\\operatorname{predAbove}(0,j)) = j \\quad (n>0) $$$

Lean4

theorem succ_predAbove_zero [NeZero n] {j : Fin (n + 1)} (h : j ≠ 0) : succ (predAbove 0 j) = j := by simp [h]

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

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

Разделы

Аффилиация

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