zero_succAbove

Mathlib.Data.Fin.SuccPred

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

English

For any i ∈ Fin n, (0 : Fin(n+1)).succAbove i = i.succ.

Русский

Для любого i ∈ Fin(n), (0 : Fin(n+1)).succAbove i = i.succ.

LaTeX

$$$\forall n \in \mathbb{N},\ \forall i \in \mathrm{Fin}(n),\ (0 : \mathrm{Fin}(n+1)).succAbove(i) = i.succ.$$$

Lean4

@[simp]
theorem zero_succAbove {n : ℕ} (i : Fin n) : (0 : Fin (n + 1)).succAbove i = i.succ :=
  rfl

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

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

Разделы

Аффилиация

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