predAbove_of_castSucc_lt — Mathlib

English

Let p ∈ Fin n, i ∈ Fin(n+1) and h be castSucc p < i. Then p.predAbove i = i.pred (Fin.ne_zero_of_lt h).

Русский

Пусть p ∈ Fin(n), i ∈ Fin(n+1) и h: castSucc p < i. Тогда p.predAbove i = i.pred (Fin.ne_zero_of_lt h).

LaTeX

$$$ \\forall p \\in \\mathrm{Fin}(n), \\forall i \\in \\mathrm{Fin}(n+1),\\ h:\\ \\operatorname{castSucc}(p) < i \\\\ :\\ p.predAbove i = i.pred \\bigl( \\operatorname{Fin.ne\\_zero\\_of\\_lt} h \\bigr) $$$

Lean4

theorem predAbove_of_castSucc_lt (p : Fin n) (i : Fin (n + 1)) (h : castSucc p < i) :
    p.predAbove i = i.pred (Fin.ne_zero_of_lt h) :=
  dif_pos h

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