castSucc_lt_or_lt_succ

Mathlib.Data.Fin.SuccPred

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

English

For p ∈ Fin(n+1) and i ∈ Fin n, either castSucc i < p or p < i.succ.

Русский

Для p ∈ Fin(n+1) и i ∈ Fin n верно: castSucc i < p или p < i.succ.

LaTeX

$$$$ \\forall {p : \\mathrm{Fin}(n+1)} {i : \\mathrm{Fin} \\,n}, \\ castSucc i < p \\; \\lor \\; p < i.succ. $$$$

Lean4

theorem castSucc_lt_or_lt_succ (p : Fin (n + 1)) (i : Fin n) : castSucc i < p ∨ p < i.succ := by
  simpa [Fin.lt_def, -val_fin_lt] using by cutsat

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

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

Разделы

Аффилиация

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