toFinset_toList — Mathlib

English

If a list ℓ has no duplicates, then converting it to a Finset and back to a List yields a permutation of ℓ.

Русский

Если список ℓ не содержит повторов, то преобразование в Finset и обратно в список дает перестановку ℓ.

LaTeX

$$$ [ [DecidableEq \alpha] {s : List \alpha} (hs : s.Nodup) : s.toFinset.toList.Perm s $$$

Lean4

theorem _root_.List.toFinset_toList [DecidableEq α] {s : List α} (hs : s.Nodup) : s.toFinset.toList.Perm s :=
  by
  apply List.perm_of_nodup_nodup_toFinset_eq (nodup_toList _) hs
  rw [toList_toFinset]

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