English
The deduplicated Sym2 of a list is empty if and only if the deduplicated list is empty.
Русский
Упрощённая (dedup) Sym2 пустая тогда и только тогда, когда упрощённый список пуст.
LaTeX
$$$$ xs.sym2.dedup = [] \\iff xs.dedup = [] $$$$
Lean4
theorem dedup_sym2 [DecidableEq α] (xs : List α) : xs.sym2.dedup = xs.dedup.sym2 := by
induction xs with
| nil => simp only [List.sym2, dedup_nil]
| cons x xs ih =>
simp only [List.sym2, map_cons, cons_append]
obtain hm | hm := Decidable.em (x ∈ xs)
· rw [dedup_cons_of_mem hm, ← ih, dedup_cons_of_mem,
List.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset]
refine mem_append_left _ ?_
rw [mem_map]
exact ⟨_, hm, Sym2.eq_swap⟩
· rw [dedup_cons_of_notMem hm, List.sym2, map_cons, ← ih, dedup_cons_of_notMem, cons_append,
List.Disjoint.dedup_append, dedup_map_of_injective]
· exact (Sym2.mkEmbedding _).injective
· exact map_mk_disjoint_sym2 x xs hm
· simp [hm, mem_sym2_iff]
