pred_lt_castPred

Mathlib.Data.Fin.SuccPred

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

English

pred a h1 < castPred a h2.

Русский

pred a h1 < castPred a h2.

LaTeX

$$$ \operatorname{pred}(a, h_1) < \operatorname{castPred}(a, h_2). $$$

Lean4

theorem pred_lt_castPred {a : Fin (n + 1)} (h₁ : a ≠ 0) (h₂ : a ≠ last n) : pred a h₁ < castPred a h₂ := by
  rw [pred_lt_castPred_iff, le_def]

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

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

Разделы

Аффилиация

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