succAbove_castSucc_of_le

Mathlib.Data.Fin.SuccPred

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

← MathLib Explorer

English

If p ≤ i for p,i ∈ Fin(n), then p.castSucc.succAbove(i) = i.succ.

Русский

Если p ≤ i для p,i ∈ Fin(n), то p.castSucc.succAbove(i) = i.succ.

LaTeX

$$$\forall n \in \mathbb{N},\ \forall p,i \in \mathrm{Fin}(n),\ p \le i \Rightarrow p.castSucc.succAbove i = i.succ. $$$

Lean4

theorem succAbove_castSucc_of_le (p i : Fin n) (h : p ≤ i) : succAbove p.castSucc i = i.succ :=
  succAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.2 h)

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

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

Разделы

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

Аффилиация

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