succ_castPred_eq_add_one

Mathlib.Data.Fin.SuccPred

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

← MathLib Explorer

English

(a.castPred ha).succ = a + 1.

Русский

(a.castPred ha).succ = a + 1.

LaTeX

$$$ (a.castPred(h_a)).\text{succ} = a + 1. $$$

Lean4

theorem succ_castPred_eq_add_one {a : Fin (n + 1)} (ha : a ≠ last n) : (a.castPred ha).succ = a + 1 :=
  by
  cases a using lastCases
  · exact (ha rfl).elim
  · rw [castPred_castSucc, coeSucc_eq_succ]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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