English
For any list s, nodup(s.permutations) holds if and only if nodup(s).
Русский
Для любого списка s выполняется равенство nodup(s.permutations) ⇔ nodup(s).
LaTeX
$$$\forall s:\\ List \alpha, \\ Nodup(s.permutations) \iff \\ Nodup(s)$$$
Lean4
@[simp]
theorem nodup_permutations_iff {s : List α} : Nodup s.permutations ↔ Nodup s :=
by
refine ⟨?_, nodup_permutations s⟩
contrapose
rw [← exists_duplicate_iff_not_nodup]
intro ⟨x, hs⟩
rw [duplicate_iff_sublist] at hs
obtain ⟨l, ht⟩ := List.Sublist.exists_perm_append hs
rw [List.Perm.nodup_iff (List.Perm.permutations ht), ← exists_duplicate_iff_not_nodup]
use x :: x :: l
rw [List.duplicate_iff_sublist, ← permutations_take_two]
exact
take_sublist 2
_
-- TODO: `count s s.permutations = (zipWith count s s.tails).prod`
