lt_castPred_succ_iff

Mathlib.Data.Fin.SuccPred

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

← MathLib Explorer

English

For a, b, ha, the statement lt_castPred_succ_iff: b < (a.succ.castPred ha) ↔ b ≤ a.

Русский

Для a, b, ha верно: b < (a.succ.castPred ha) ↔ b ≤ a.

LaTeX

$$$ b < (a.succ.castPred(h_a)) \iff b \le a. $$$

Lean4

theorem lt_castPred_succ_iff {a b : Fin (n + 1)} (ha : succ a ≠ last (n + 1)) : b < (succ a).castPred ha ↔ b ≤ a := by
  rw [lt_castPred_iff, castSucc_lt_succ_iff]

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

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

Разделы

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

Аффилиация

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