eq_castSucc_or_eq_last — Mathlib

English

Every element of Fin(n+1) is either the castSucc of some Fin n or the last element of Fin n.

Русский

Каждый элемент Fin(n+1) либо является castSucc некоторого Fin n, либо последним элементом Fin n.

LaTeX

$$$\exists j : Fin n, i = j.castSucc \lor i = last\, n$$$

Lean4

theorem eq_castSucc_or_eq_last {n : Nat} (i : Fin (n + 1)) : (∃ j : Fin n, i = j.castSucc) ∨ i = last n :=
  i.lastCases (Or.inr rfl) (Or.inl ⟨·, rfl⟩)

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