formPerm_mem_iff_mem — Mathlib

English

For any l: List α and x: α, formPerm l x ∈ l if and only if x ∈ l.

Русский

Для любого списка l и элемента x из α выполняется: formPerm l x ∈ l тогда и только тогда, когда x ∈ l.

LaTeX

$$$\forall \alpha\, [\DecidableEq\ \alpha],\ \forall l:\,\mathrm{List}\ \alpha,\ \forall x:\,\alpha,\ (\mathrm{formPerm}\ l\ x)\in l \iff x\in l$$$

Lean4

@[simp]
theorem formPerm_mem_iff_mem : l.formPerm x ∈ l ↔ x ∈ l :=
  ⟨l.mem_of_formPerm_apply_mem, l.formPerm_apply_mem_of_mem⟩

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