succAbove_ne_zero — Mathlib

English

If n ≠ 0 and a ≠ 0 and b ≠ 0, then a.succAbove(b) ≠ 0.

Русский

Если n ≠ 0 и a ≠ 0 и b ≠ 0, то a.succAbove(b) ≠ 0.

LaTeX

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

Lean4

theorem succAbove_ne_zero [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) (hb : b ≠ 0) : a.succAbove b ≠ 0 :=
  mt (succAbove_eq_zero_iff ha).mp hb

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