support_formPerm_of_nodup — Mathlib

English

If l is Nodup and the hypothesis h' holds (∀x, l ≠ [x]), then the support of formPerm l equals l.toFinset.

Русский

Если l без повторов и выполняется условие h', то поддержка formPerm l равна l.toFinset.

LaTeX

$$$\{x \mid \mathrm{formPerm}\ l\ x \neq x\} = l^{\mathrm{toFinset}}$$$

Lean4

theorem support_formPerm_of_nodup [Fintype α] (l : List α) (h : Nodup l) (h' : ∀ x : α, l ≠ [x]) :
    support (formPerm l) = l.toFinset := by
  rw [← Finset.coe_inj]
  convert support_formPerm_of_nodup' _ h h'
  simp [Set.ext_iff]

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