Erasing duplicates, keeping first occurrences

Core List.eraseDups keeps the first occurrence of each entry, in order, and core proves that it keeps every entry (List.mem_eraseDups). This file adds that the result is a duplicate-free sublist, that it fixes exactly the duplicate-free lists, and that its length is the number of distinct entries.

Main results

• List.eraseDups_sublist, List.nodup_eraseDups, List.eraseDups_eq_self.
• List.toFinset_eraseDups, List.length_eraseDups.

theorem List.eraseDups_sublist {α : Type u_1} [BEq α] (l : List α) : l.eraseDups.Sublist l

eraseDups keeps a sublist.

theorem List.nodup_eraseDups {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) : l.eraseDups.Nodup

eraseDups leaves no duplicates.

theorem List.eraseDups_eq_self {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} : l.eraseDups = l ↔ l.Nodup

eraseDups fixes exactly the duplicate-free lists.

@[simp]

theorem List.toFinset_eraseDups {α : Type u_1} [DecidableEq α] (l : List α) : l.eraseDups.toFinset = l.toFinset

theorem List.length_eraseDups {α : Type u_1} [DecidableEq α] (l : List α) : l.eraseDups.length = l.toFinset.card

The length of eraseDups is the number of distinct entries.