Multiset.dedup_cons_of_not_mem
theorem Multiset.dedup_cons_of_not_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∉ s → (a ::ₘ s).dedup = a ::ₘ s.dedup := by
sorry
The theorem `Multiset.dedup_cons_of_not_mem` states that for all types `α` that have decidable equality, for each element `a` of type `α`, and for each multiset `s` of type `α`, if `a` does not belong to `s`, then removing duplicates from the multiset that results from consing `a` onto `s` is equivalent to consing `a` onto the multiset that results from removing duplicates from `s`. In other words, if `a` is not already in `s`, then we can add `a` to `s` either before or after removing duplicates from `s`, and we will get the same result.
More concisely: If `α` has decidable equality, for all `a` not in multiset `s` of type `α`, the multisets `{a} ∪ M.dedup s` and `M.dedup (s ∪ {a})` are equal.
|
Multiset.dedup_le
theorem Multiset.dedup_le : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.dedup ≤ s
The theorem `Multiset.dedup_le` states that for any type `α` that has decidable equality, and for any multiset `s` of type `α`, the multiset obtained by deduplicating `s` (`Multiset.dedup s`) is a sub-multiset of `s`. In other words, the multiset that results from removing duplicates from `s` contains only elements that originally existed in `s`, and thus, it must be less than or equal to `s`.
More concisely: For any type `α` with decidable equality and any multiset `s` of type `α`, `Multiset.dedup s` is a sub-multiset of `s`.
|
Multiset.dedup_ext
theorem Multiset.dedup_ext :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s.dedup = t.dedup ↔ ∀ (a : α), a ∈ s ↔ a ∈ t
This theorem states that for any type `α` with decidable equality and for any two multisets `s` and `t` of type `α`, the operation `Multiset.dedup` results in identical multisets for `s` and `t` if and only if each element `a` of type `α` is a member of `s` if and only if it is a member of `t`. In other words, two multisets have the same elements after removing duplicates if and only if they contain the same elements before removing duplicates.
More concisely: For any type `α` with decidable equality, two multisets `s` and `t` of type `α` have identical `Multiset.dedup` outputs if and only if they have the same elements before duplicates are removed.
|
Multiset.Nodup.dedup
theorem Multiset.Nodup.dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s.Nodup → s.dedup = s := by
sorry
This theorem, referred to as an alias of the reverse direction of `Multiset.dedup_eq_self`, asserts that for any type `α` with a decidable equality and for any multiset `s` of type `α`, if `s` has no duplicates (i.e., `Multiset.Nodup s` is true), then removing duplicates from `s` (i.e., `Multiset.dedup s`) results in `s` itself. In other words, if a multiset is already a set with no duplicates, then the process of removing duplicates will not alter the multiset.
More concisely: For any type `α` with decidable equality and any multiset `s` of type `α` with no duplicates, `Multiset.dedup s = s`.
|
Multiset.dedup_cons_of_mem
theorem Multiset.dedup_cons_of_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s → (a ::ₘ s).dedup = s.dedup
The theorem `Multiset.dedup_cons_of_mem` states that for any type `α` with a decidable equality relation, and for any element `a` of type `α` and multiset `s` of type `α`, if `a` is a member of `s`, then removing duplicates from the multiset that results from consing `a` onto `s` (i.e., adding `a` to `s`) is equal to just removing duplicates from `s`. In other words, if `a` is already in `s`, adding another `a` to `s` before removing duplicates doesn't change the end result.
More concisely: For any type `α` with decidable equality and any multiset `s` of type `α` and element `a` in `s`, the multisets obtained by removing duplicates from `s` and from `s.insert a` are equal.
|
Multiset.dedup_eq_self
theorem Multiset.dedup_eq_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s.dedup = s ↔ s.Nodup := by
sorry
This theorem states that for any type `α` with decidable equality and any multiset `s` of type `α`, the `Multiset.dedup` operation applied to `s` results in `s` itself if and only if `s` has no duplicates (satisfies `Multiset.Nodup`). In other words, a multiset is the same as its deduplicated version if and only if it does not contain repeated elements.
More concisely: For any type `α` with decidable equality, a multiset `s` of type `α` is equal to `Multiset.dedup s` if and only if `s` is a multiset without repetitions.
|
Multiset.nodup_dedup
theorem Multiset.nodup_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.dedup.Nodup
The theorem `Multiset.nodup_dedup` asserts that for any multiset `s` of a type `α`, where `α` has decidable equality, the operation `Multiset.dedup s` results in a multiset with no duplicates. In other words, when duplicates are removed from a given multiset `s` using the `Multiset.dedup` function, the resulting multiset satisfies the `Multiset.Nodup` property.
More concisely: For any decidably equal multiset `s` of type `α`, `Multiset.dedup s` is a multiset with no duplicate elements.
|
Mathlib.Data.Multiset.Dedup._auxLemma.1
theorem Mathlib.Data.Multiset.Dedup._auxLemma.1 :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, (a ∈ s.dedup) = (a ∈ s)
This theorem states that for any given type `α` which has decidable equality, and any specific element `a` of type `α` and multiset `s` of the same type, checking if `a` belongs to the deduplicated version of `s` is equivalent to checking if `a` belongs to `s` itself. In simpler terms, the presence of an element in a multiset is not affected by the operation of removing duplicates from the multiset.
More concisely: For any decidably equated type `α`, and multiset `s` and element `a` of type `α`, the decidability of `a ∈ s` implies the decidability of `a ∈ set.dedup s`.
|
Multiset.subset_dedup
theorem Multiset.subset_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s ⊆ s.dedup
This theorem states that for any given multiset `s` of an arbitrary type `α` with decidable equality, `s` is a subset of the deduplicated version of `s`. In other words, every element in the original multiset `s` also appears in the multiset resulting from the `dedup` operation on `s`. This makes sense as `dedup` operation only eliminates duplicate elements and does not add or remove unique elements.
More concisely: For any decidably equal multiset `s` of type `α`, every element in `s` is contained in the multiset obtained by applying the `dedup` operation to `s`.
|