mem_of_formPerm_apply_mem — Mathlib

English

Let l be a finite list in a type α equipped with decidable equality. If applying the permutation formPerm l to x yields an element of l, then x already lies in l.

Русский

Пусть l — конечный список элементов типа α, у которого есть разрешимое равенство. Если образ x под перестановкой formPerm l принадлежит списку l, то и сам x принадлежит l.

LaTeX

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

Lean4

theorem mem_of_formPerm_apply_mem (h : l.formPerm x ∈ l) : x ∈ l :=
  by
  contrapose h
  rwa [formPerm_apply_of_notMem h]

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