exists_succAbove_eq_iff — Mathlib

English

For x,y ∈ Fin(n+1), (exists z with x.succAbove z = y) is equivalent to y ≠ x.

Русский

Для x,y ∈ Fin(n+1), существование z с x.succAbove z = y эквивалентно y ≠ x.

LaTeX

$$$\forall n \in \mathbb{N}\, \forall x,y \in \mathrm{Fin}(n+1),\bigl(\exists z, x.succAbove(z) = y\bigr) \Leftrightarrow y \neq x.$$$

Lean4

@[simp]
theorem exists_succAbove_eq_iff {x y : Fin (n + 1)} : (∃ z, x.succAbove z = y) ↔ y ≠ x :=
  ⟨by rintro ⟨y, rfl⟩; exact succAbove_ne _ _, exists_succAbove_eq⟩

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