Multiset.inj_on_of_nodup_map
theorem Multiset.inj_on_of_nodup_map :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Multiset α},
(Multiset.map f s).Nodup → ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
This theorem states that for any multiset `s` of type `α`, function `f` mapping from `α` to `β`, and any elements `x` and `y` in `s`, if there are no duplicates in the multiset obtained by applying `f` to each element of `s`, then if `f x` equals `f y`, `x` must equal `y`. In other words, under the condition of no duplicates in the mapped multiset, the function `f` is injective (one-to-one) on the elements of the original multiset `s`.
More concisely: If `s` is a multiset, `f` is a function from `s.elem type` to `β`, and the multiset `{f x | x ∈ s}` has no duplicates, then `f x = f y` implies `x = y`.
|
Multiset.Nodup.map_on
theorem Multiset.Nodup.map_on :
∀ {α : Type u_1} {β : Type u_2} {s : Multiset α} {f : α → β},
(∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → s.Nodup → (Multiset.map f s).Nodup
The theorem `Multiset.Nodup.map_on` states that for any type `α` and `β`, a multiset `s` of type `α`, and a function `f` from `α` to `β`, if for all elements `x` and `y` in the multiset `s`, `f(x)` equals `f(y)` implies `x` equals `y`, then if the multiset `s` has no duplicates (`Multiset.Nodup s`), the multiset resulting from mapping `f` over `s` (`Multiset.map f s`) also has no duplicates. In other words, if a function gives distinct outputs for distinct inputs and is applied to a duplicate-free multiset, the resulting multiset will also be free from duplicates.
More concisely: If `f` is a function such that `x ≠ y` implies `f(x) ≠ f(y)` and `s` is a multiset with no duplicates, then `Multiset.map f s` is also a multiset with no duplicates.
|
Multiset.coe_nodup
theorem Multiset.coe_nodup : ∀ {α : Type u_1} {l : List α}, (↑l).Nodup ↔ l.Nodup
The theorem `Multiset.coe_nodup` establishes an equivalence between the property of a list not having any duplicate elements and the corresponding multiset (created from the list by disregarding order of elements) not having any duplicate elements. For any given type `α` and a list `l` of type `α`, if `l` has no duplicates, i.e., every element in `l` appears at most once, then the multiset created from `l` also has no duplicates, and vice versa.
More concisely: For any type `α` and list `l` of length `n` over `α`, the list `l` has no duplicate elements if and only if the multiset obtained from `l` by disregarding order has cardinality equal to `n`.
|
Multiset.Nodup.map
theorem Multiset.Nodup.map :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Multiset α},
Function.Injective f → s.Nodup → (Multiset.map f s).Nodup
This theorem states that for any types `α` and `β`, any function `f` from `α` to `β`, and any multiset `s` of type `α`, if the function `f` is injective and the multiset `s` has no duplicates (i.e., all elements in `s` are unique), then the multiset obtained by mapping `f` over `s` also has no duplicates. In other words, applying an injective function to a multiset with unique elements results in a new multiset with unique elements.
More concisely: If `f: α -> β` is an injective function and `s: set α` has no duplicates, then `map f s: set β` also has no duplicates.
|
Multiset.Nodup.pmap
theorem Multiset.Nodup.pmap :
∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : ∀ a ∈ s, p a},
(∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b) → s.Nodup → (Multiset.pmap f s H).Nodup
The theorem `Multiset.Nodup.pmap` asserts that for any types `α` and `β`, a property `p : α → Prop`, a function `f : (a : α) → p a → β` mapping elements of the type `α` satisfying the property `p` to elements of the type `β`, and a multiset `s : Multiset α` where every element satisfies property `p`, if the function `f` guarantees that, whenever it maps two different elements satisfying property `p` to the same value, then those two elements were identical in the first place, and if the multiset `s` does not contain any duplicate elements, then the multiset obtained by mapping `f` over `s` (denoted `Multiset.pmap f s H`) also does not contain any duplicate elements. In simpler terms, if you start with a set without duplicates and apply a function that doesn't collapse different values to the same result, then the transformed set will also not have any duplicates.
More concisely: Given a multiset of distinct elements from type `α` and a function `f : α → β` such that `f` maps distinct elements satisfying `p(x)` to distinct values, the multiset obtained by applying `f` to the elements of the original multiset (with the property `p` as hypothesis) also does not contain any duplicate elements.
|
Multiset.count_eq_one_of_mem
theorem Multiset.count_eq_one_of_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, s.Nodup → a ∈ s → Multiset.count a s = 1 := by
sorry
The theorem `Multiset.count_eq_one_of_mem` states that for any type `α` with decidable equality, any element `a` of type `α`, and any multiset `s` of type `α`, if the multiset `s` has no duplicates (i.e., every element appears at most once), and the element `a` is an element of `s`, then the multiplicity of `a` in `s` (i.e., the number of times `a` appears in `s`) is exactly 1. In other words, each element of a duplicate-free multiset appears exactly once.
More concisely: If `α` is a type with decidable equality, `a` is an element of a multiset `s` of type `α` with no duplicates, then the multiplicity of `a` in `s` is equal to 1.
|
Multiset.nodup_of_le
theorem Multiset.nodup_of_le : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → t.Nodup → s.Nodup
The theorem `Multiset.nodup_of_le` states that for any types `α` and multisets `s` and `t` of type `α`, if `s` is a sub-multiset of `t` (denoted by `s ≤ t`) and `t` is a set with no duplicates (denoted by `Multiset.Nodup t`), then `s` should also be a set with no duplicates (denoted by `Multiset.Nodup s`). In other words, a subset of a duplicate-free set is also duplicate-free.
More concisely: If `s` is a sub-multiset of the duplicate-free multiset `t`, then `s` is also a duplicate-free multiset.
|
Multiset.Nodup.attach
theorem Multiset.Nodup.attach : ∀ {α : Type u_1} {s : Multiset α}, s.Nodup → s.attach.Nodup
The theorem `Multiset.Nodup.attach` states that for any type `α` and any multiset `s` of type `α`, if `s` does not contain any duplicate elements (i.e., `s.Nodup`), then the "attached" multiset `s.attach` also does not contain any duplicate elements. Here, "attached" refers to a specific operation in Lean on multisets. This theorem is essentially the reverse direction of another theorem named `Multiset.nodup_attach`.
More concisely: If `s` is a multiset of type `α` with no duplicates, then `s.attach` also has no duplicates.
|
Multiset.Nodup.of_map
theorem Multiset.Nodup.of_map :
∀ {α : Type u_1} {β : Type u_2} {s : Multiset α} (f : α → β), (Multiset.map f s).Nodup → s.Nodup
The theorem `Multiset.Nodup.of_map` states that for any types `α` and `β`, any multiset `s` of type `α`, and any function `f` mapping from `α` to `β`, if the multiset resulting from mapping the function `f` over `s` has no duplicates (i.e., `Multiset.Nodup (Multiset.map f s)`), then the original multiset `s` must also have no duplicates (i.e., `Multiset.Nodup s`). In simpler terms, if applying a function to each element of a multiset results in a set with no duplicate values, then the original set also had no duplicates.
More concisely: If `s` is a multiset with no duplicates and `f` is a function such that `Multiset.map f s` has no duplicates, then `α = β` and `s = {x | ∃! y, f x = y}`. (This statement assumes that the function `f` is injective, i.e., distinct inputs map to distinct outputs.)
|
Multiset.nodup_iff_count_le_one
theorem Multiset.nodup_iff_count_le_one :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s.Nodup ↔ ∀ (a : α), Multiset.count a s ≤ 1
The theorem `Multiset.nodup_iff_count_le_one` states that for any type `α` with decidable equality and any multiset `s` of type `α`, the property that `s` has no duplicates (denoted by `Multiset.Nodup s`) is equivalent to the property that the count of any element `a` in `s` is less than or equal to one. This provides a characterization of a multiset with no duplicates in terms of the multiplicity of its elements.
More concisely: For any type `α` with decidable equality and any multiset `s` of type `α`, `Multiset.Nodup s` if and only if for all `a` in `α`, the count of `a` in `s` is less than or equal to one.
|
Mathlib.Data.Multiset.Nodup._auxLemma.4
theorem Mathlib.Data.Multiset.Nodup._auxLemma.4 : ∀ {α : Type u_1} (a : α), {a}.Nodup = True
This theorem states that for any type `α` and an element `a` of that type, a multiset containing just the element `a` has no duplicates. In other words, a single-element multiset is always considered to have no duplicates, regardless of the type or value of the element.
More concisely: For any type `α` and element `a` of type `α`, the multiset {`a`} has no duplicates.
|
Multiset.le_iff_subset
theorem Multiset.le_iff_subset : ∀ {α : Type u_1} {s t : Multiset α}, s.Nodup → (s ≤ t ↔ s ⊆ t)
This theorem states that for any types `α` and multisets `s` and `t` of type `α`, if `s` has no duplicates (formally defined by `Multiset.Nodup s`), then `s` is less than or equal to `t` if and only if `s` is a subset of `t`. Here, the less than or equal relation (≤) for multisets is defined in terms of the multiplicity of elements in `s` not exceeding their multiplicity in `t`. The subset relation (⊆) means every element of `s` is also an element of `t`. In essence, the theorem is about an equivalence between these two relations when `s` doesn't contain duplicate elements.
More concisely: For multisets `s` and `t` of type `α`, `s ≤ t` if and only if `s ⊆ t` when `s` has no duplicates.
|
Mathlib.Data.Multiset.Nodup._auxLemma.1
theorem Mathlib.Data.Multiset.Nodup._auxLemma.1 : ∀ {α : Type u_1} {l : List α}, (↑l).Nodup = l.Nodup
The theorem `Mathlib.Data.Multiset.Nodup._auxLemma.1` states that for all types `α` and for any list `l` of that type, the property of the multiset associated to `l` having no duplicates (i.e., `Multiset.Nodup ↑l`) is equivalent to the property of the list `l` having no duplicates (i.e., `List.Nodup l`). In other words, a list and its corresponding multiset share the same "no duplicates" property.
More concisely: The theorem asserts that for any type `α` and list `l` of length `n` over `α`, `Multiset.Nodup (List.map fromList (List.take n (List.repeat x (nat.succ (n - 1)))）) ≡ List.nodup l`, where `x` is any element of type `α` and `fromList` is the function mapping a multiset to its underlying list.
|
Multiset.nodup_cons
theorem Multiset.nodup_cons : ∀ {α : Type u_1} {a : α} {s : Multiset α}, (a ::ₘ s).Nodup ↔ a ∉ s ∧ s.Nodup
This theorem states that for any type `α`, any element `a` of type `α`, and any multiset `s` of type `α`, the multiset `s` has no duplicates (the condition expressed by `Multiset.Nodup`) after prepending with the element `a` (denoted by `a ::ₘ s`) if and only if two conditions hold: the element `a` is not already in `s` (`a ∉ s`), and `s` itself has no duplicates (`Multiset.Nodup s`).
More concisely: For any type `α` and element `a` not in a multiset `s` of type `α`, the multiset `a :: s` has no duplicates if and only if `s` itself has no duplicates.
|
Mathlib.Data.Multiset.Nodup._auxLemma.3
theorem Mathlib.Data.Multiset.Nodup._auxLemma.3 :
∀ {α : Type u_1} {a : α} {s : Multiset α}, (a ::ₘ s).Nodup = (a ∉ s ∧ s.Nodup)
This theorem states that, for all types `α`, elements `a` of type `α`, and multisets `s` of type `α`, the multiset `s` has no duplicates (represented by `Multiset.Nodup`) when `a` is added to `s` (expressed as `a ::ₘ s`) if and only if `a` is not already an element in `s` (denoted by `a ∉ s`) and `s` itself has no duplicates.
More concisely: For all types `α` and multisets `s` of type `α`, the multiset `s` has no duplicates after adding an element `a` not in `s` (`a ::ₘ s`) if and only if `s` initially had no duplicates (`Multiset.Nodup s`).
|