le_of_castSucc_lt_of_succ_lt — Mathlib

English

If a,b ∈ Fin(n+1) and i ∈ Fin n with castSucc i < a and b < succ i, then b < a.

Русский

Пусть a,b ∈ Fin(n+1) и i ∈ Fin n; если castSucc i < a и b < succ i, то b < a.

LaTeX

$$$$ \\forall {a,b : \\mathrm{Fin}(n+1)} \\{i : \\mathrm{Fin}\\,n\\}, \\ castSucc(i) < a \\to b < succ(i) \\to b < a. $$$$

Lean4

theorem le_of_castSucc_lt_of_succ_lt {a b : Fin (n + 1)} {i : Fin n} (hl : castSucc i < a) (hu : b < succ i) : b < a :=
  by simp [Fin.lt_def, -val_fin_lt] at *; cutsat

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