formPerm_eq_head_iff_eq_getLast — Mathlib

English

For any l, x, y, the statement formPerm (y :: l) x = y is equivalent to x = getLast (y :: l).

Русский

Для любых l, x, y: formPerm (y :: l) x = y эквивалентно x = getLast (y :: l).

LaTeX

$$$\forall \alpha\, [\DecidableEq\ \alpha],\forall l:\,\mathrm{List}\ \alpha,\forall x:\,\alpha,\forall y:\,\alpha,\ formPerm (y :: l) x = y \iff x = (y :: l).getLast\ (cons_ne_nil\ _\ _)$$$

Lean4

theorem formPerm_eq_head_iff_eq_getLast (x y : α) : formPerm (y :: l) x = y ↔ x = getLast (y :: l) (cons_ne_nil _ _) :=
  Iff.trans (by rw [formPerm_apply_getLast]) (formPerm (y :: l)).injective.eq_iff

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