succAbove_left_inj — Mathlib

English

Equivalently, x.succAbove = y.succAbove iff x = y for x,y ∈ Fin(n+1).

Русский

Эквивалентно: x.succAbove = y.succAbove тогда и только тогда, когда x=y для x,y ∈ Fin(n+1).

LaTeX

$$$\forall n \in \mathbb{N},\ \forall x,y \in \mathrm{Fin}(n+1),\ x.succAbove = y.succAbove \iff x = y.$$$

Lean4

/-- `succAbove` is injective at the pivot -/
@[simp]
theorem succAbove_left_inj {x y : Fin (n + 1)} : x.succAbove = y.succAbove ↔ x = y :=
  succAbove_left_injective.eq_iff

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