exists_succAbove_eq — Mathlib

English

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

Русский

Для x, y ∈ Fin(n+1) при x ≠ y существует z such that y.succAbove z = x.

LaTeX

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

Lean4

theorem exists_succAbove_eq {x y : Fin (n + 1)} (h : x ≠ y) : ∃ z, y.succAbove z = x :=
  by
  obtain hxy | hyx := Fin.lt_or_lt_of_ne h
  exacts [⟨_, succAbove_castPred_of_lt _ _ hxy⟩, ⟨_, succAbove_pred_of_lt _ _ hyx⟩]

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