castSucc_ne_zero_of_lt — Mathlib

English

Let p and i be elements of Fin(n) with p < i. Then the successor of i in Fin(n+1) is not the zero element.

Русский

Пусть p и i — элементы Fin(n) такие, что p < i. Тогда следующее за i в Fin(n+1) не равно нулю.

LaTeX

$$$$ \\forall n \\in \\mathbb{N}, \\forall p,i \\in \\mathrm{Fin}(n), p < i \\implies \\operatorname{castSucc}(i) \\neq 0. $$$$

Lean4

theorem castSucc_ne_zero_of_lt {p i : Fin n} (h : p < i) : castSucc i ≠ 0 :=
  by
  cases n
  · exact i.elim0
  · rw [castSucc_ne_zero_iff, Ne, Fin.ext_iff]
    exact ((zero_le _).trans_lt h).ne'

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