castPred_inj

Mathlib.Data.Fin.SuccPred

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

← MathLib Explorer

English

If castPred i hi = castPred j hj, then i = j.

Русский

Если castPred i hi = castPred j hj, то i = j.

LaTeX

$$$ \operatorname{castPred} i h_i = \operatorname{castPred} j h_j \iff i = j. $$$

Lean4

@[simp]
theorem castPred_inj {i j : Fin (n + 1)} {hi : i ≠ last n} {hj : j ≠ last n} : castPred i hi = castPred j hj ↔ i = j :=
  by simp_rw [Fin.ext_iff, le_antisymm_iff, ← le_def, castPred_le_castPred_iff]

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

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

Разделы

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

Аффилиация

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