predAbove_last_castSucc

Mathlib.Data.Fin.SuccPred

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

← MathLib Explorer

English

For i ∈ Fin(n+1), predAbove (last n) (i.castSucc) = i.

Русский

Для i ∈ Fin(n+1) predAbove (last n) (i.castSucc) = i.

LaTeX

$$$ \\forall i \\in \\mathrm{Fin}(n+1),\\ \\operatorname{predAbove}(\\operatorname{last} n, i.castSucc) = i $$$

Lean4

theorem predAbove_last_castSucc {i : Fin (n + 1)} : predAbove (last n) (i.castSucc) = i := by
  rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr (le_last _)), castPred_castSucc]

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

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

Разделы

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

Аффилиация

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