equivPair_eq_of_fstIdx_ne — Mathlib

English

For any index i and word w, if the first index of w is not i, then the i-th equivalence pair of w is the pair with head 1 and tail w (together with the corresponding witness).

Русский

Для любых индексов i и слова w, если первый индекс w не равен i, то пара equivPair(i,w) тривиальна и равна (1, w) с доказательством.

LaTeX

$$$$ \\forall i\\, \\forall w\\, \\forall h:\\ fstIdx(w) \\neq Some(i)\\ \\Rightarrow\\ equivPair(i,w) = \\langle 1, w, h \\rangle $$$$

Lean4

theorem equivPair_eq_of_fstIdx_ne {i} {w : Word M} (h : fstIdx w ≠ some i) : equivPair i w = ⟨1, w, h⟩ :=
  (equivPair i).apply_eq_iff_eq_symm_apply.mpr <| Eq.symm (dif_pos rfl)

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