lt_succ_castPred

Mathlib.Data.Fin.SuccPred

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

English

a < succ(a.castPred ha) for appropriate ha.

Русский

a < succ(a.castPred ha) при подходящем ha.

LaTeX

$$$ a < \operatorname{succ}(a.castPred(h_a)). $$$

Lean4

theorem lt_succ_castPred {a : Fin (n + 1)} (ha : a ≠ last n) : a < succ (a.castPred ha) := by
  rw [lt_succ_castPred_iff, le_def]

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

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

Разделы

Аффилиация

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