succAbove_eq_zero_iff — Mathlib

English

If a ≠ 0, then a.succAbove(b) = 0 iff b = 0.

Русский

Если a ≠ 0, то a.succAbove(b) = 0 тогда и только тогда b = 0.

LaTeX

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

Lean4

theorem succAbove_eq_zero_iff [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) : a.succAbove b = 0 ↔ b = 0 := by
  rw [← succAbove_ne_zero_zero ha, succAbove_right_inj]

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