formPerm_apply_head — Mathlib

English

If x,y,xs are such that x::y::xs is nodup, then formPerm (x::y::xs) x = y.

Русский

Если x, y, xs образуют список без повторов, то formPerm (x::y::xs) x = y.

LaTeX

$$$\forall \alpha\, [\DecidableEq\ \alpha],\forall x,y:\,\alpha,\forall xs:\,\mathrm{List}\ \alpha,\ (\mathrm{List}.Nodup\ (x :: y :: xs)) \rightarrow \mathrm{formPerm}\ (x :: y :: xs)\ x = y$$$

Lean4

theorem formPerm_apply_head (x y : α) (xs : List α) (h : Nodup (x :: y :: xs)) : formPerm (x :: y :: xs) x = y := by
  simp [formPerm_apply_of_notMem h.notMem]

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