List.dedup_cons_of_not_mem
theorem List.dedup_cons_of_not_mem :
∀ {α : Type u} [inst : DecidableEq α] {a : α} {l : List α}, a ∉ l → (a :: l).dedup = a :: l.dedup
The theorem `List.dedup_cons_of_not_mem` states that for any type `α` with decidable equality, any element `a` of type `α`, and any list `l` of elements of type `α`, if `a` is not a member of `l`, then the operation of removing duplicates from the list formed by consing `a` onto `l` results in a list that starts with `a` and is followed by the list obtained by removing duplicates from `l`. In other words, if `a` is not in `l`, then removing duplicates from `a :: l` gives `a :: (dedup l)`.
More concisely: If `α` is a type with decidable equality, `a` is not an element of list `l` of type `α`, then the list obtained by removing duplicates from `a :: l` equals `a :: (removeDuplicates l)`.
|
List.nodup_dedup
theorem List.nodup_dedup : ∀ {α : Type u} [inst : DecidableEq α] (l : List α), l.dedup.Nodup
The theorem `List.nodup_dedup` states that for any type `α` which has decidable equality, given any list `l` of type `α`, the list obtained by removing duplicates from `l` using the `List.dedup` function has no duplicates. In other words, for every list, it's guaranteed that the deduplicated version of that list won't contain any repeated elements.
More concisely: Given any list `l` of type `α` with decidable equality, the list `List.dedup l` has no repeated elements.
|
List.Nodup.dedup
theorem List.Nodup.dedup : ∀ {α : Type u} [inst : DecidableEq α] {l : List α}, l.Nodup → l.dedup = l
The theorem `List.Nodup.dedup` states that for any type `α` that has decidable equality, and any list `l` of type `α`, if the list `l` has no duplicate elements (defined by `List.Nodup l`), then removing duplicates from `l` (using `List.dedup l`) results in a list that is identical to the original list `l`. In other words, if a list already has no duplicates, then running a duplicate-removal function on it has no effect.
More concisely: If `α` has decidable equality and `l : List α` has no duplicates, then `List.dedup l = l`.
|
List.dedup_cons_of_mem
theorem List.dedup_cons_of_mem :
∀ {α : Type u} [inst : DecidableEq α] {a : α} {l : List α}, a ∈ l → (a :: l).dedup = l.dedup
This theorem states that for any type `α` with decidable equality, given an element `a` of the type `α` and a list `l` of type `List α`, if `a` is an element of the list `l`, then the operation of removing duplicates from the list obtained by prepending `a` to `l` (`a :: l`) results in the same list as simply removing duplicates from the original list `l`. In other words, if the list already contains `a`, adding another `a` at the beginning doesn't change the list after removing duplicates.
More concisely: For any type `α` with decidable equality and list `l` of `α`, if `a ∈ l`, then removing duplicates from `a :: l` equals removing duplicates from `l`.
|
List.dedup_eq_self
theorem List.dedup_eq_self : ∀ {α : Type u} [inst : DecidableEq α] {l : List α}, l.dedup = l ↔ l.Nodup
The theorem `List.dedup_eq_self` states that for any list `l` of elements of type `α`, which has a decidable equality, the list `l` is equal to its deduplicated version if and only if the list `l` has no duplicates. In other words, if all elements in the list `l` are unique (i.e., each element appears at most once), then removing duplicates from the list `l` does not change the list. Conversely, if removing duplicates from the list `l` leads to the same list, it implies that there were no duplicates in `l` to begin with.
More concisely: For any list `l` of uniquely equal elements of type `α`, the deduplicated list `List.dedup l` equals `l`.
|
List.mem_dedup
theorem List.mem_dedup : ∀ {α : Type u} [inst : DecidableEq α] {a : α} {l : List α}, a ∈ l.dedup ↔ a ∈ l
The theorem `List.mem_dedup` states that for any type `α` that has decidable equality and for any element `a` of type `α` and list `l` of type `α`, `a` is a member of the deduplicated list `l` if and only if `a` is a member of the original list `l`. In other words, deduplicating a list using the `List.dedup` function does not change the membership of any element in the list.
More concisely: For any type `α` with decidable equality and any list `l` of elements `α`, the deduplicated list `List.dedup l` contains an element `a` if and only if `l` contains `a`.
|
Mathlib.Data.List.Dedup._auxLemma.1
theorem Mathlib.Data.List.Dedup._auxLemma.1 : ∀ {α : Type u} {a : α} {l : List α}, (∀ a' ∈ l, ¬a = a') = (a ∉ l) := by
sorry
This theorem, named `Mathlib.Data.List.Dedup._auxLemma.1`, states that for any type `α`, any element `a` of type `α`, and any list `l` of type `α`, the statement "for all elements `a'` in the list `l`, `a` is not equal to `a'`" is equivalent to the statement "`a` is not an element of the list `l`". In other words, `a` not being equal to any element in `l` is the same as `a` not being in `l`.
More concisely: For any type `α` and element `a` of type `α`, `a` is not in list `l` of type `α` if and only if `a` is not equal to any element in `l`.
|
Mathlib.Data.List.Dedup._auxLemma.3
theorem Mathlib.Data.List.Dedup._auxLemma.3 :
∀ {α : Type u} [inst : DecidableEq α] {a : α} {l : List α}, (a ∈ l.dedup) = (a ∈ l)
The theorem `Mathlib.Data.List.Dedup._auxLemma.3` states that for any type `α` that has decidable equality, and for any element `a` of type `α` and any list `l` of type `α`, the presence of `a` in the list `l` from which duplicates have been removed (by `List.dedup`) is equivalent to the presence of `a` in the original list `l`. In other words, an element is in the de-duplicated list if and only if it is in the original list.
More concisely: For any type `α` with decidable equality and any list `l` of `α`, the element `a` is in the de-duplicated list `List.dedup l` if and only if it is in the original list `l`.
|