fstIdx — Mathlib

English

The function fstIdx returns Some i if the first letter of w is (i, m), and None if w is empty.

Русский

Функция fstIdx возвращает Some i, если первая буква слова равна (i, m), и None, если слово пусто.

LaTeX

$$$ \\mathrm{fstIdx}(w) = \\begin{cases} \\mathrm{Some}(i) & \\text{if } w = (i,m)::\\_, \\\\ \\mathrm{None} & \\text{if } w = [] \\end{cases}$$$

Lean4

/-- `fstIdx w` is `some i` if the first letter of `w` is `⟨i, m⟩` with `m : M i`. If `w` is empty
then it's `none`. -/
def fstIdx (w : Word M) : Option ι :=
  w.toList.head?.map Sigma.fst

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