formPerm_apply_getElem_zero — Mathlib

English

If l is Nodup and hl: 1 < length l, then formPerm l l[0] = l[1].

Русский

При Nodup и 1 < |l| имеем formPerm l l[0] = l[1].

LaTeX

$$$\forall \alpha\, [\DecidableEq\ \alpha],\forall l:\,\mathrm{List}\ \alpha,\ l.Nodup\rightarrow\ (\forall hl:\, 1 < l.length),\ \mathrm{formPerm}\ l\ l[0] = l[1]$$$

Lean4

theorem formPerm_apply_getElem_zero (l : List α) (h : Nodup l) (hl : 1 < l.length) : formPerm l l[0] = l[1] :=
  by
  rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)
  · simp at hl
  · simp at hl
  · rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]

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