orderSucc_castSucc

Mathlib.Data.Fin.SuccPredOrder

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

English

For i ∈ Fin n, Order.succ i.castSucc = i.succ.

Русский

Для i ∈ Fin(n): Order.succ(i.castSucc) = i.succ.

LaTeX

$$$\forall i \in \mathrm{Fin}(n),\ \mathrm{Order.succ}(i.castSucc) = i.succ$$$

Lean4

@[simp]
theorem orderSucc_castSucc {n : ℕ} (i : Fin n) : Order.succ i.castSucc = i.succ := by simp [orderSucc_apply]

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

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

Разделы

Аффилиация

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