fstIdx_ne_iff — Mathlib

English

For any w and i, fstIdx(w) ≠ some i iff every first component in w’s head (if any) is different from i.

Русский

Для любого w и i, fstIdx(w) ≠ some i тогда и только тогда, когда все первые компоненты в голове слова (если есть) отличаются от i.

LaTeX

$$$ \\mathrm{fstIdx}(w) \\neq \\mathrm{Some}(i) \\iff \\forall l \\in w.toList.head?, i \\neq \\Sigma_1(l).$$$

Lean4

theorem fstIdx_ne_iff {w : Word M} {i} : fstIdx w ≠ some i ↔ ∀ l ∈ w.toList.head?, i ≠ Sigma.fst l :=
  not_iff_not.mp <| by simp [fstIdx]

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