succ_le_or_le_castSucc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem succ_le_or_le_castSucc (p : Fin (n + 1)) (i : Fin n) : succ i ≤ p ∨ p ≤ i.castSucc :=
  by
  rw [le_castSucc_iff, ← castSucc_lt_iff_succ_le]
  exact p.castSucc_lt_or_lt_succ i

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