succAbove_ne_zero_zero — Mathlib

English

Assume n ≠ 0 and a ≠ 0 in Fin(n+1). Then a.succAbove(0) = 0.

Русский

Пусть n ≠ 0 и a ≠ 0 в Fin(n+1). Тогда a.succAbove(0) = 0.

LaTeX

$$$\forall n \in \mathbb{N},\ [\mathrm{NeZero}(n)] \Rightarrow \forall a \in \mathrm{Fin}(n+1), a \neq 0 \Rightarrow a.succAbove(0) = 0.$$$

Lean4

@[simp]
theorem succAbove_ne_zero_zero [NeZero n] {a : Fin (n + 1)} (ha : a ≠ 0) : a.succAbove 0 = 0 :=
  by
  rw [Fin.succAbove_of_castSucc_lt]
  · exact castSucc_zero'
  · exact Fin.pos_iff_ne_zero.2 ha

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