eq_self_or_eq_succAbove — Mathlib

English

Let p be an element of Fin(n+1) and i be any element of Fin(n+1). Then either i = p or there exists j ∈ Fin n such that i = p.succAbove j.

Русский

Пусть p ∈ Fin(n+1) и i ∈ Fin(n+1). Тогда либо i = p, либо существует j ∈ Fin n such that i = p.succAbove(j).

LaTeX

$$$i = p \lor \exists j: \mathrm{Fin}(n), i = p.\\succAbove j.$$$

Lean4

/-- Analogue of `Fin.eq_zero_or_eq_succ` for `succAbove`. -/
theorem eq_self_or_eq_succAbove (p i : Fin (n + 1)) : i = p ∨ ∃ j, i = p.succAbove j :=
  succAboveCases p (.inl rfl) (fun j => .inr ⟨j, rfl⟩) i

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