Multiset.exists_mem_of_rel_of_mem
theorem Multiset.exists_mem_of_rel_of_mem :
∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β},
Multiset.Rel r s t → ∀ {a : α}, a ∈ s → ∃ b ∈ t, r a b
This theorem states that for all types `α` and `β`, and a relation `r` between `α` and `β`, if there is a `Multiset.Rel r` relationship between a multiset `s` of type `α` and a multiset `t` of type `β`, then, for any element `a` in multiset `s`, there exists an element `b` in multiset `t` such that the relation `r` holds between `a` and `b`. In other words, if two multisets are related by a certain relationship, then any element in the first multiset is related by this relationship to some element in the second multiset.
More concisely: For all types `α`, `β` and relations `r` between `α` and `β`, if there is a multiset inclusion `s ⊆ t` of multisets `s` of type `α` and `t` of type `β` such that `Multiset.Rel r s t`, then for all `a` in `s`, there exists `b` in `t` with `r a b`.
|
Multiset.eq_replicate
theorem Multiset.eq_replicate :
∀ {α : Type u_1} {a : α} {n : ℕ} {s : Multiset α},
s = Multiset.replicate n a ↔ Multiset.card s = n ∧ ∀ b ∈ s, b = a
The theorem `Multiset.eq_replicate` in Lean 4 states that for any given type `α`, element `a` of type `α`, natural number `n`, and a multiset `s` of type `α`, the multiset `s` is equal to the multiset produced by `Multiset.replicate n a` (which is a multiset containing only `a` with multiplicity `n`) if and only if the cardinality (number of elements, including duplicates) of `s` is `n` and every element `b` in `s` is equal to `a`.
More concisely: A multiset `s` of type `α` equals the multiset `Multiset.replicate n a` if and only if `s` has cardinality `n` and consists only of elements equal to `a`.
|
Multiset.count_pos
theorem Multiset.count_pos :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, 0 < Multiset.count a s ↔ a ∈ s
The theorem `Multiset.count_pos` states that for any type `α` with decidable equality and for any element `a` of type `α` and multiset `s` of type `α`, the count of `a` in `s` is greater than zero if and only if `a` is an element of `s`. It essentially establishes a connection between the multiplicity of an element in a multiset and its membership in that multiset.
More concisely: For any type `α` with decidable equality, element `a` of type `α`, and multiset `s` of type `α`, `Multiset.count a s > 0 if and only if a ∈ s`.
|
Multiset.mem_singleton
theorem Multiset.mem_singleton : ∀ {α : Type u_1} {a b : α}, b ∈ {a} ↔ b = a
This theorem, `Multiset.mem_singleton`, is stating that for any type `α` and any two instances of that type, `a` and `b`, `b` is a member of the singleton multiset containing only `a` if and only if `b` is equal to `a`. In other words, in a multiset with only one element, an element is present if it is equal to the single member of the set.
More concisely: For any type `α` and any two elements `a` and `b` of type `α`, the element `b` is in the singleton multiset `{a}:` Multiset `α` if and only if `a` is equal to `b`.
|
Multiset.foldr_cons
theorem Multiset.foldr_cons :
∀ {α : Type u_1} {β : Type v} (f : α → β → β) (H : LeftCommutative f) (b : β) (a : α) (s : Multiset α),
Multiset.foldr f H b (a ::ₘ s) = f a (Multiset.foldr f H b s)
The theorem `Multiset.foldr_cons` states that for any types α and β, if a function `f` from α to β is left-commutative, and for any element `b` of type β, any element `a` of type α, and any multiset `s` of type α, the result of folding `f` over the multiset obtained by consing `a` onto `s` (written as `a ::ₘ s` in Lean) with base value `b` is the same as applying `f` to `a` and the result of folding `f` over `s` with base value `b`. In other words, folding over a multiset with a left-commutative function behaves as expected when an element is added to the front of the multiset.
More concisely: For any left-commutative function `f` from type `α` to type `β` and any multiset `s` of type `α`, the expression `f a (Multiset.foldr f b s)` equals `Multiset.foldr f b (a ::ₘ s)`, where `a` is an element of type `α` and `b` is a base value of type `β`.
|
Multiset.map_id'
theorem Multiset.map_id' : ∀ {α : Type u_1} (s : Multiset α), Multiset.map (fun x => x) s = s
The theorem `Multiset.map_id'` asserts that for any type `α` and any multiset `s` of `α`, applying the identity function to each element of `s` through the function `Multiset.map` returns the multiset `s` itself. In other words, `Multiset.map` with the identity function leaves the multiset unchanged. This is akin to the mathematical principle that applying the identity function to each element of a set yields the set itself.
More concisely: For any type α and multiset s of α, the application of the identity function through Multiset.map leaves the multiset s unchanged.
|
Multiset.mem_add
theorem Multiset.mem_add : ∀ {α : Type u_1} {a : α} {s t : Multiset α}, a ∈ s + t ↔ a ∈ s ∨ a ∈ t
This theorem states that for any type `α`, a given element `a` of type `α`, and two multisets `s` and `t` of type `α`, `a` is a member of the multiset resulting from the addition of `s` and `t` if and only if `a` is a member of either `s` or `t`. Here, the addition of two multisets is analogous to the union operation in set theory, but allows for duplicates.
More concisely: For any type `α` and elements `a` of type `α`, the multiset `s ± t` contains `a` if and only if `s` or `t` contains `a`. (Here, `±` denotes multiset addition in Lean 4.)
|
Multiset.le_cons_self
theorem Multiset.le_cons_self : ∀ {α : Type u_1} (s : Multiset α) (a : α), s ≤ a ::ₘ s
This theorem states that for any type `α` and a multiset `s` of `α`, along with any element `a` of `α`, the multiset `s` is less than or equal to the multiset obtained by prepending `a` to `s`. In other words, adding an element to the multiset does not decrease its size, in the sense of the multiset size order relation.
More concisely: For any type `α` and multisets `s` and `t` of `α` where `t` is obtained by adding an element `a` to `s`, we have `s ≤ t` in the multiset order relation.
|
Multiset.subset_zero
theorem Multiset.subset_zero : ∀ {α : Type u_1} {s : Multiset α}, s ⊆ 0 ↔ s = 0
The theorem `Multiset.subset_zero` states that for any type `α` and any multiset `s` of type `α`, `s` is a subset of the empty multiset if and only if `s` is the empty multiset itself. Here, the empty multiset is represented by `0`. This theorem essentially says that the only subset of the empty multiset is the empty multiset itself.
More concisely: A multiset `s` of type `α` is equal to the empty multiset (represented by `0`) if and only if `s` is a subset of the empty multiset.
|
Mathlib.Data.Multiset.Basic._auxLemma.22
theorem Mathlib.Data.Multiset.Basic._auxLemma.22 :
∀ {α : Type u_1} {s t : Multiset α}, (s ⊆ t) = ∀ ⦃x : α⦄, x ∈ s → x ∈ t
This theorem states that for any type `α` and multisets `s` and `t` of type `α`, the condition that `s` is a subset of `t` is equivalent to the property that every element `x` of `s` is also an element of `t`. In other words, a multiset `s` is a subset of another multiset `t` if and only if every element in `s` also appears in `t`.
More concisely: For any type `α` and multisets `s` and `t` of type `α`, `s ⊆ t` if and only if for all `x ∈ s`, `x ∈ t`.
|
Multiset.coe_reverse
theorem Multiset.coe_reverse : ∀ {α : Type u_1} (l : List α), ↑l.reverse = ↑l
This theorem states that for any type `α` and any list `l` of elements of type `α`, the multiset representation of the reversed list `l` is equal to the multiset representation of the original list `l`. In other words, reversing the order of elements in the list does not change its multiset representation, as multisets are collections of elements where order does not matter.
More concisely: For any type `α` and list `l` of elements of type `α`, the multiset representation of list `l` is equal to the multiset representation of its reverse.
|
Multiset.rel_map_left
theorem Multiset.rel_map_left :
∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {r : α → β → Prop} {s : Multiset γ} {f : γ → α} {t : Multiset β},
Multiset.Rel r (Multiset.map f s) t ↔ Multiset.Rel (fun a b => r (f a) b) s t
The theorem `Multiset.rel_map_left` states that for any types `α`, `β`, and `γ`, any relation `r` from `α` to `β`, any multiset `s` of elements of type `γ`, any function `f` from `γ` to `α`, and any multiset `t` of elements of type `β`, there is an equivalence between the assertion that the multiset resulting from mapping the function `f` over `s` is related to `t` by the multiset relation induced by `r`, and the assertion that `s` is related to `t` by the multiset relation induced by the composition of `f` and `r`. In other words, mapping a function over a multiset and then relating it to another multiset is equivalent to relating the original multiset to the other multiset by a relation that incorporates the function.
More concisely: For any types α, β, γ, relation r from α to β, multiset s of γ, function f from γ to α, and multiset t of β, the multisets f[s] and r[t] are equivalent if and only if s and t are equivalent with respect to the relation r composited with f.
|
Multiset.card_le_of_le
theorem Multiset.card_le_of_le : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → Multiset.card s ≤ Multiset.card t := by
sorry
This theorem, referred to as an alias of `Multiset.card_le_card`, declares that for any two multisets `s` and `t` of any type `α`, if `s` is less than or equal to `t` (in terms of multiset order), then the cardinality of `s` is less than or equal to the cardinality of `t`. In other words, if multiset `s` is a sub-multiset of `t`, then the number of elements (including repetitions) in `s` is less than or equal to the number of elements in `t`.
More concisely: For any multisets $s$ and $t$ of type $\alpha$, if $s$ is subset of $t$ (in terms of multiset order), then $|s| \leq |t|$. Here, $|s|$ and $|t|$ denote the cardinalities of multisets $s$ and $t$, respectively.
|
Multiset.bot_eq_zero
theorem Multiset.bot_eq_zero : ∀ {α : Type u_1}, ⊥ = 0
This theorem is stating that for any given type `α`, the bottom element of the multiset of that type (`⊥`) is equal to zero (`0`). It is a version of the `bot_eq_zero` theorem that uses reflexivity (`rfl`) and simplification (`simp`).
More concisely: The theorem asserts that the bottom element `⊥` of any type `α` in Lean equals the natural number zero `0`.
|
Multiset.le_add_right
theorem Multiset.le_add_right : ∀ {α : Type u_1} (s t : Multiset α), s ≤ s + t
The theorem `Multiset.le_add_right` states that, for any type `α` and any two multisets `s` and `t` of type `α`, `s` is less than or equal to the multiset obtained by adding `s` and `t`. In other words, a multiset `s` is always less than or equal to the union of `s` and any other multiset `t`. This is a property of the partially ordered set structure on multisets, where the order is defined by multiset inclusion.
More concisely: For any type `α` and multisets `s` and `t` of type `α`, `s ⊆ s ++ t`, where `++` denotes multiset union.
|
Mathlib.Data.Multiset.Basic._auxLemma.2
theorem Mathlib.Data.Multiset.Basic._auxLemma.2 : ∀ {α : Type u_1} (l : List α), (↑l = 0) = (l = [])
This theorem states that for any list `l` of arbitrary type `α`, the list `l` is equivalent to an empty list if and only if the cardinality (or size) of `l` is zero. In other words, a list `l` in Lean 4 is empty if its size is zero.
More concisely: For any list `l` in Lean 4, the list `l` is empty if and only if its cardinality is zero.
|
Multiset.card_replicate
theorem Multiset.card_replicate : ∀ {α : Type u_1} (n : ℕ) (a : α), Multiset.card (Multiset.replicate n a) = n := by
sorry
The theorem `Multiset.card_replicate` states that for any type `α`, any natural number `n`, and any element `a` of type `α`, the cardinality of a multiset created by replicating the element `a` `n` times (`Multiset.replicate n a`) is equal to `n`. In other words, if you create a multiset by repeating a particular element `n` times, the total count of elements in that multiset will also be `n`.
More concisely: For any type `α` and natural number `n`, the cardinality of the multiset obtained by replicating an element `a` of type `α` `n` times equals `n`.
|
Multiset.eq_of_mem_replicate
theorem Multiset.eq_of_mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ Multiset.replicate n a → b = a := by
sorry
This theorem states that for any type `α`, any elements `a` and `b` of type `α`, and any natural number `n`, if `b` is an element of the multiset obtained by replicating `a` `n` times, then `b` must be equal to `a`. Essentially, this theorem affirms that any element in a multiset created from multiple copies of a single element is equal to that original element.
More concisely: For any type `α`, any natural number `n`, and any elements `a` and `b` of type `α`, if `b` is an element of the multiset of `n` copies of `a`, then `a = b`.
|
Multiset.replicate_one
theorem Multiset.replicate_one : ∀ {α : Type u_1} (a : α), Multiset.replicate 1 a = {a}
The theorem `Multiset.replicate_one` states that for any type `α` and for any element `a` of that type, the multiset that results from replicating `a` exactly once (i.e., `Multiset.replicate 1 a`) is simply a multiset containing the element `a` itself. This means that the multiset of replicating any element once is a multiset containing only that particular element.
More concisely: For any type `α` and element `a` of that type, `Multiset.replicate 1 a` equals the multiset `{a}` containing exactly one copy of `a`.
|
Multiset.rel_refl_of_refl_on
theorem Multiset.rel_refl_of_refl_on :
∀ {α : Type u_1} {m : Multiset α} {r : α → α → Prop}, (∀ x ∈ m, r x x) → Multiset.Rel r m m
This theorem states that for any type `α`, any multiset `m` of that type, and any binary relation `r` defined on `α`, if the relation `r` is reflexive on every element in the multiset `m` (i.e., `r x x` holds for every `x` in `m`), then the multiset `m` is related to itself under the multiset relation induced by `r`. This is equivalent to saying that the multiset `m` is reflexive with respect to the relation `r`.
More concisely: If for every element `x` in a multiset `m` of type `α`, the binary relation `r` on `α` is reflexive at `x` (i.e., `r x x` holds), then `m` is a reflexive multiset with respect to `r`.
|
Multiset.attach.proof_1
theorem Multiset.attach.proof_1 : ∀ {α : Type u_1} (s : Multiset α), ∀ _a ∈ s, _a ∈ s
The theorem `Multiset.attach.proof_1` states that for any type `α`, and any multiset `s` of that type, any element `_a` that is in `s` will still be in `s`. It guarantees that if an element is part of a multiset, it remains in that multiset, underlining the permanence of elements in multisets. This is a fundamental property of multisets, equivalent to saying that if an object is in a bag, it remains in that bag unless removed.
More concisely: For any type `α` and multiset `s` of type `α`, if an element `a` is in `s`, then `a` is still in `s`.
|
Multiset.count_filter_of_pos
theorem Multiset.count_filter_of_pos :
∀ {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} [inst_1 : DecidablePred p] {a : α} {s : Multiset α},
p a → Multiset.count a (Multiset.filter p s) = Multiset.count a s
The theorem `Multiset.count_filter_of_pos` states that for any type `α` with decidable equality, any decidable predicate `p`, any element `a` of type `α`, and any multiset `s` of elements of type `α`, if `p a` is true, then the multiplicity of `a` in the multiset obtained by filtering `s` with `p` is equal to the multiplicity of `a` in `s`. In other words, if `p a` is true, then the process of filtering does not change the count of `a` in the multiset.
More concisely: For any decidable type `α`, decidable predicate `p` on `α`, element `a` of `α`, and multiset `s` of `α`, if `p a` holds, then the number of occurrences of `a` in the filtered multiset `Multiset.filter s p` is equal to the number of occurrences of `a` in `s`.
|
Multiset.induction
theorem Multiset.induction :
∀ {α : Type u_1} {p : Multiset α → Prop},
p 0 → (∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) → ∀ (s : Multiset α), p s
The theorem `Multiset.induction` describes a method of induction on multisets. Given any type `α`, a property `p` that applies to multisets of `α`, we can prove that this property holds for all multisets of `α` if we can demonstrate two things. First, that the property `p` holds for the empty multiset (denoted by `0`). Second, if we can show that for any given element `a` of type `α` and any multiset `s` of `α`, if the property `p` holds for `s`, then it also holds for the multiset formed by prepending `a` to `s` (denoted by `a ::ₘ s`).
More concisely: If a property holds for the empty multiset and is closed under prepending an element to a multiset, then it holds for all multisets.
|
Multiset.mem_cons_self
theorem Multiset.mem_cons_self : ∀ {α : Type u_1} (a : α) (s : Multiset α), a ∈ a ::ₘ s
This theorem states that for any type `α`, any element `a` of type `α`, and any multiset `s` of type `α`, the element `a` is a member of the multiset formed by prepending `a` to `s`. In other words, if we add an element to the multiset, then that element is definitely in the multiset.
More concisely: For any type `α`, any element `a` of type `α`, and any multiset `s` of type `α`, `a` is a member of the multiset obtained by adding `a` to `s`.
|
Mathlib.Data.Multiset.Basic._auxLemma.23
theorem Mathlib.Data.Multiset.Basic._auxLemma.23 : ∀ {a b c : Prop}, (a ∨ b → c) = ((a → c) ∧ (b → c))
This theorem states that for any three propositions `a`, `b` and `c`, the proposition that "`a` OR `b` implies `c`" is equivalent to the conjunction "`a` implies `c` AND `b` implies `c`". In other words, if `c` follows from either `a` or `b`, then `c` should follow from `a` and also from `b`.
More concisely: (`a ∨ b ↔ a → c ∧ b → c`) states that `a` OR `b` implies `c` if and only if `a` implies `c` and `b` implies `c`.
|
Multiset.count_union
theorem Multiset.count_union :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α),
Multiset.count a (s ∪ t) = max (Multiset.count a s) (Multiset.count a t)
The theorem `Multiset.count_union` states that for any type `α` with a decidable equality, given an element `a` of type `α` and two multisets `s` and `t` of type `α`, the multiplicity of `a` in the union of `s` and `t` is equal to the maximum of the multiplicity of `a` in `s` and the multiplicity of `a` in `t`. In other words, it's expressing that when you unite two multisets, the count of an element in the resulting multiset is the maximum of the counts of that element in the original multisets. This is just like saying that the number of times an element appears in the combination of two collections is the most number of times it appears in either one.
More concisely: For any type `α` with decidable equality, the multiplicity of an element `a` in the union of multisets `s` and `t` is the maximum of the multiplicities of `a` in `s` and `t`.
|
Multiset.exists_mem_of_ne_zero
theorem Multiset.exists_mem_of_ne_zero : ∀ {α : Type u_1} {s : Multiset α}, s ≠ 0 → ∃ a, a ∈ s
The theorem `Multiset.exists_mem_of_ne_zero` states that for any type `α` and any multiset `s` of that type, if the multiset `s` is not empty (i.e., `s ≠ 0`), then there exists an element `a` such that `a` is a member of `s`. This is essentially saying that a non-empty multiset always contains at least one element.
More concisely: If `s` is a non-empty multiset, then there exists an element `a` such that `a ∈ s`.
|
Multiset.replicate_le_coe
theorem Multiset.replicate_le_coe :
∀ {α : Type u_1} {a : α} {n : ℕ} {l : List α}, Multiset.replicate n a ≤ ↑l ↔ (List.replicate n a).Sublist l := by
sorry
This theorem states that for any type `α`, any element `a` of type `α`, any natural number `n`, and any list `l` of elements of type `α`, the multiset created by replicating `a` `n` times is a subset of the multiset derived from `l` if and only if the list created by replicating `a` `n` times is a sublist of `l`. This is a way of linking the concept of sublist on lists with the concept of subset on multisets.
More concisely: For any type `α`, any natural number `n`, any element `a` of type `α`, and any list `l` of elements of type `α`, the multiset formed by `n` replicas of `a` is a subset of the multiset formed from list `l` if and only if `l` contains `n` copies of `a` as sublist.
|
Multiset.le_add_left
theorem Multiset.le_add_left : ∀ {α : Type u_1} (s t : Multiset α), s ≤ t + s
The theorem `Multiset.le_add_left` states that for any type `α` and for any two multisets `s` and `t` of type `α`, `s` is less than or equal to the sum of `t` and `s`. Here, the sum of two multisets is the multiset containing all elements of both sets, possibly with duplication, and the order of elements does not matter. The less than or equal operation `≤` for multisets is defined in a sense analogous to subset relation for sets, but considering the number of occurrences of each element.
More concisely: For any type `α` and multisets `s` and `t` of type `α`, `s ≤ s + t`. (That is, the multiset `s` is less than or equal to the sum of `s` and `t`.)
|
Mathlib.Data.Multiset.Basic._auxLemma.72
theorem Mathlib.Data.Multiset.Basic._auxLemma.72 :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} {s : Multiset α},
(a ∈ Multiset.filter p s) = (a ∈ s ∧ p a)
The theorem `Mathlib.Data.Multiset.Basic._auxLemma.72` states that for any type `α`, any decidable predicate `p` on `α`, any item `a` of type `α`, and any `Multiset` `s` of type `α`, the item `a` is in the filtered multiset (where the filter is given by the predicate `p`) if and only if `a` is in the original multiset `s` and `a` satisfies the predicate `p`. In other words, filtering a multiset by a predicate does not introduce new elements, and it only retains those elements from the original multiset that satisfy the predicate.
More concisely: For any type `α`, decidable predicate `p` on `α`, item `a` of type `α`, and `Multiset` `s` of type `α`, the item `a` is in the filtered multiset (defined as the multiset of elements in `s` that satisfy `p`) if and only if `a` is in `s` and `p(a)` holds.
|
Multiset.disjoint_comm
theorem Multiset.disjoint_comm : ∀ {α : Type u_1} {s t : Multiset α}, s.Disjoint t ↔ t.Disjoint s
The theorem `Multiset.disjoint_comm` states that for any type `α` and any two multisets `s` and `t` of that type, `s` and `t` are disjoint if and only if `t` and `s` are disjoint. In other words, the property of disjointness is commutative for multisets; the order in which we consider the two multisets does not affect whether or not they are disjoint. Disjointness here means that there is no element that belongs to both multisets.
More concisely: For any type `α`, two multisets `s` and `t` of type `α` are disjoint if and only if `t` and `s` are disjoint. (That is, `s.disjoint t <--> t.disjoint s`.)
|
Mathlib.Data.Multiset.Basic._auxLemma.34
theorem Mathlib.Data.Multiset.Basic._auxLemma.34 : ∀ {α : Type u_1} {l₁ l₂ : List α}, (↑l₁ ≤ ↑l₂) = l₁.Subperm l₂ := by
sorry
This theorem states that for any type `α` and any two lists `l₁` and `l₂` of type `α`, the statement that the multiset generated from `l₁` is a subset of the multiset generated from `l₂` (denoted as `↑l₁ ≤ ↑l₂`) is equivalent to the statement that `l₁` is a sublist of a permutation of `l₂` (denoted as `List.Subperm l₁ l₂`). In other words, it establishes an equivalence between subset relationships in multisets and the `Subperm` relation for lists, which is a sublist relationship that respects multiplicities of elements.
More concisely: The multiset generated by a list is a subset of another multiset if and only if the first list is a sublist of a permutation of the second list.
|
Multiset.filter_eq
theorem Multiset.filter_eq :
∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (b : α),
Multiset.filter (Eq b) s = Multiset.replicate (Multiset.count b s) b
This theorem, named `Multiset.filter_eq`, is stating a property about multisets in a given type `α` where equality is decidable. Specifically, it says that if we filter a multiset `s` with the equality predicate `Eq b`, effectively keeping only the elements equal to `b`, the result is the same as replicating `b` exactly as many times as it appears in `s`. In other words, the filtered multiset where we keep only the elements equal to `b` is exactly the same as creating a multiset consisting of only `b`, replicated `count b s` times. This theorem is universally quantified over all types `α` with decidable equality and all multisets `s` and elements `b` in `α`.
More concisely: For all types `α` with decidable equality and for all multisets `s` and elements `b` in `α`, the multiset obtained by filtering `s` using the equality predicate `Eq b` is equal to the multiset with `b` replicated `count b s` times.
|
Multiset.count_eq_zero
theorem Multiset.count_eq_zero :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {a : α}, Multiset.count a s = 0 ↔ a ∉ s
This theorem states that for any type `α` with a decidable equality and any element `a` of type `α` and multiset `s` of type `α`, the count of `a` in `s` is zero if and only if `a` is not in `s`. In other words, the multiplicity of an element in a multiset being zero is equivalent to the element not being present in the multiset.
More concisely: For any type `α` with decidable equality, element `a` of type `α`, and multiset `s` of type `α`, the number of occurrences of `a` in `s` is zero if and only if `a` is not an element of `s`.
|
Multiset.map_zero
theorem Multiset.map_zero : ∀ {α : Type u_1} {β : Type v} (f : α → β), Multiset.map f 0 = 0
The theorem `Multiset.map_zero` states that for any function `f` mapping elements from type `α` to type `β`, the multiset obtained by mapping `f` over an empty multiset (denoted as 0) is also an empty multiset. In other words, if you apply a function to every element of an empty multiset, you get back an empty multiset.
More concisely: The theorem asserts that the image of the empty multiset under any function is the empty multiset.
|
Multiset.lt_cons_self
theorem Multiset.lt_cons_self : ∀ {α : Type u_1} (s : Multiset α) (a : α), s < a ::ₘ s
The theorem `Multiset.lt_cons_self` states that for any type `α` and for any multiset `s` of type `α` and any element `a` of type `α`, the multiset `s` is strictly less than the multiset formed by prepending `a` to `s`. Here, `<` is the multiset strict subset relation, and `::ₘ` is the multiset cons operator. This theorem establishes that adding an element to a multiset will always create a multiset that is strictly larger than the original.
More concisely: For any type `α` and multisets `s` and `t` of type `α` where `t = a ::ₘ s`, we have `s < t`.
|
Multiset.nsmul_singleton
theorem Multiset.nsmul_singleton : ∀ {α : Type u_1} (a : α) (n : ℕ), n • {a} = Multiset.replicate n a
This theorem states that for any type `α`, any value `a` of type `α`, and any natural number `n`, the scalar multiplication of `n` and the singleton multiset containing only `a` is equal to the multiset containing `a` with multiplicity `n`. In other words, multiplying a singleton multiset `{a}` by `n` results in a multiset with `n` copies of `a`.
More concisely: For any type `α`, the scalar multiplication of a natural number `n` with the singleton multiset `{a : α}` is the multiset with `n` copies of `a`.
|
Multiset.erase_subset
theorem Multiset.erase_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), s.erase a ⊆ s := by
sorry
The theorem `Multiset.erase_subset` states that for any type `α` that has decidable equality, and any element `a` of type `α` and multiset `s` of elements of type `α`, the multiset resulting from erasing `a` from `s` is a subset of `s`. In other words, removing an element from a multiset always results in a multiset that is a subset of the original one.
More concisely: For any type `α` with decidable equality and any multiset `s` of `α` and element `a` in `α`, the multiset obtained by erasing `a` from `s` is a subset of `s`.
|
Multiset.insert_eq_cons
theorem Multiset.insert_eq_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α), insert a s = a ::ₘ s
The theorem `Multiset.insert_eq_cons` states that for any type `α` and for any element `a` of this type and any multiset `s` of this type, inserting the element `a` into the multiset `s` is equivalent to adding the element `a` to the front of the multiset `s`. Here, a multiset is a type of finite sets where duplicates are allowed, and the operation `a ::ₘ s` adds the element `a` to the front of the multiset `s`.
More concisely: For any type `α` and any multiset `s` of type `α`, the multiset obtained by inserting an element `a` of type `α` into `s` is equal to the multiset obtained by adding `a` to the front of `s` using the multiset cons operator `::ₘ`.
|
Multiset.map_add
theorem Multiset.map_add :
∀ {α : Type u_1} {β : Type v} (f : α → β) (s t : Multiset α),
Multiset.map f (s + t) = Multiset.map f s + Multiset.map f t
The theorem `Multiset.map_add` states that for any type `α` and `β`, any function `f` from `α` to `β`, and any multiset `s` and `t` of `α`, the map of the function `f` onto the union of the multisets `s` and `t` is equal to the union of the map of `f` onto `s` and the map of `f` onto `t`. In other words, mapping a function over the addition (union) of two multisets is the same as adding (union) the maps of the function over the individual multisets. This property reflects the distributive nature of the map operation over multiset addition.
More concisely: For any type α, function f from α to β, and multisets s and t of α, the map of f onto the union of s and t equals the union of the maps of f onto s and t. (Multiset.map\_add)
|
Mathlib.Data.Multiset.Basic._auxLemma.6
theorem Mathlib.Data.Multiset.Basic._auxLemma.6 :
∀ {α : Type u_1} {a b : α} {s : Multiset α}, (a ∈ b ::ₘ s) = (a = b ∨ a ∈ s)
This theorem states that for any type `α`, and any elements `a` and `b` of `α`, and any multiset `s` of `α`, the condition of `a` being an element of the multiset formed by adjoining `b` to `s` is equivalent to the disjunction of `a` being equal to `b` or `a` being an element of `s`. In other words, an element `a` is in a multiset formed by adding an element `b` to another multiset `s` if and only if `a` equals `b` or `a` is in `s`.
More concisely: For any type `α`, and any elements `a`, `b` of `α`, and multiset `s` of `α`, `a` is in the multiset `s ∪ {b}` if and only if `a = b` or `a` is in `s`.
|
Multiset.cons_add
theorem Multiset.cons_add : ∀ {α : Type u_1} (a : α) (s t : Multiset α), a ::ₘ s + t = a ::ₘ (s + t)
The theorem `Multiset.cons_add` asserts that for all types `α`, for any element `a` of type `α`, and for any two multisets `s` and `t` of type `α`, the operation of prepending `a` to the multiset `s` and then adding the multiset `t` is equivalent to the operation of prepending `a` to the sum of `s` and `t`. In other words, the operations of prepending and adding multisets are associative, symbolically represented as `(a ::ₘ s) + t = a ::ₘ (s + t)`.
More concisely: For all types `α` and multisets `s` and `t` of type `α`, prepending an element `a` to the sum of `s` and `t` is equivalent to first prepending `a` to `s` and then adding `t`, i.e., `(a :: s) + t = a :: (s + t)`.
|
Multiset.sub_le_iff_le_add
theorem Multiset.sub_le_iff_le_add :
∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s - t ≤ u ↔ s ≤ u + t
The theorem `Multiset.sub_le_iff_le_add` is a statement about multisets in Lean 4. Specifically, for any type `α` that has decidable equality, and for any three multisets `s`, `t`, and `u` of type `α`, the multiset `s - t` is less than or equal to `u` if and only if `s` is less than or equal to `u + t`. This is a special case of the more general theorem `tsub_le_iff_right` and is necessary for proving properties of ordered subtraction on multisets.
More concisely: For multisets $s, t, u$ over a type with decidable equality, $s - t \leq u$ if and only if $s \leq u + t$.
|
Multiset.map_count_True_eq_filter_card
theorem Multiset.map_count_True_eq_filter_card :
∀ {α : Type u_1} (s : Multiset α) (p : α → Prop) [inst : DecidablePred p],
Multiset.count True (Multiset.map p s) = Multiset.card (Multiset.filter p s)
The theorem `Multiset.map_count_True_eq_filter_card` states that for any multiset `s` of a certain type `α`, and any predicate `p` that can be decided for every element of `α`, the count of `True` in the multiset obtained by mapping `p` over `s` is equal to the cardinality of the multiset obtained by filtering `s` with `p`. This essentially means the number of times `p` returns `True` when applied to the elements of `s` is the same as the number of elements in `s` that satisfy `p`. Note that the decidability instances on both sides of the equation are not the same due to the requirements of the `count` method.
More concisely: For any multiset `s` of type `α` and predicate `p` on `α`, the number of elements in `s` that satisfy `p` equals the count of `True` values obtained by applying `p` to the elements of `s`.
|
Multiset.le_inter
theorem Multiset.le_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
The theorem `Multiset.le_inter` states that for any type `α` which has decidable equality, given three multisets `s`, `t`, and `u` of type `α`, if `s` is a subset of or equal to `t` and `s` is a subset of or equal to `u`, then `s` is also a subset of or equal to the intersection of `t` and `u`. The intersection of two multisets is a multiset which contains all elements that are present in both multisets. Thus, if all elements of `s` are in `t` and `u`, they must also be in the intersection of `t` and `u`.
More concisely: If `s subseteq/eq s1` and `s subseteq/eq s2`, then `s subseteq/eq s1 inter s2`. (Here, `s`, `s1`, `s2`, and `s1 inter s2` are multisets of type `α` with decidable equality.)
|
Multiset.count_add
theorem Multiset.count_add :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α),
Multiset.count a (s + t) = Multiset.count a s + Multiset.count a t
The theorem `Multiset.count_add` states that for any type `α` that has decidable equality, and for any element `a` of type `α` and any two multisets `s` and `t` of type `α`, the multiplicity of `a` in the multiset obtained by adding `s` and `t` is equal to the sum of the multiplicity of `a` in `s` and the multiplicity of `a` in `t`. In other words, the count of an element in the union of two multisets is the sum of the counts of that element in each of the multisets. This is akin to saying that the number of occurrences of a particular element in the union of two collections is the sum of the number of occurrences of that element in each individual collection.
More concisely: For multisets `s` and `t` over decidably equal type `α`, the count of an element `a` in the multiset `s ++ t` is equal to the count of `a` in `s` plus the count of `a` in `t`.
|
Multiset.map_id
theorem Multiset.map_id : ∀ {α : Type u_1} (s : Multiset α), Multiset.map id s = s
The theorem `Multiset.map_id` states that for any multiset `s` of any type `α`, applying the identity function `id` to each element of `s` via the function `Multiset.map` leaves the multiset unchanged. In other words, if we map each element of a multiset to itself, the resulting multiset is the same as the original. This is a multiset analogue of the familiar list property that mapping the identity over a list does not change the list.
More concisely: For any multiset `s` of type `α`, `Multiset.map id s = s`.
|
Multiset.pmap_eq_map
theorem Multiset.pmap_eq_map :
∀ {α : Type u_1} {β : Type v} (p : α → Prop) (f : α → β) (s : Multiset α) (H : ∀ a ∈ s, p a),
Multiset.pmap (fun a x => f a) s H = Multiset.map f s
This theorem states that for any type `α` and `β`, a predicate `p` on `α`, a function `f` from `α` to `β`, and a multiset `s` of type `α` such that all elements `a` in `s` satisfy the predicate `p`, the operation `Multiset.pmap` using the function `f` (ignoring the proof of the predicate) on `s` is equivalent to the `Multiset.map` of function `f` on `s`. Simply put, if we have a function that applies to all elements of a multiset, partial mapping and full mapping of that function produce the same result.
More concisely: For any type `α`, `β`, predicate `p` on `α`, function `f` from `α` to `β`, and multiset `s` of type `α` where all elements satisfy `p`, `Multiset.pmap f s = Multiset.map f s`.
|
Mathlib.Data.Multiset.Basic._auxLemma.5
theorem Mathlib.Data.Multiset.Basic._auxLemma.5 : ∀ {α : Type u_1} {a : α} {l : List α}, (a ∈ ↑l) = (a ∈ l)
This theorem states that for any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, the predicate stating that `a` is in the `l` when `l` is coerced (or "upcast") to a multiset is equivalent to the predicate stating that `a` is in the `l` as a list. In other words, an element is in a list if and only if it is in the multiset obtained from the list.
More concisely: For any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, `a` is in the multiset obtained from list `l` if and only if `a` is in list `l` as a regular list element.
|
Multiset.card_eq_zero
theorem Multiset.card_eq_zero : ∀ {α : Type u_1} {s : Multiset α}, Multiset.card s = 0 ↔ s = 0
This theorem states that for any multiset `s` of any type `α`, the cardinality (or size) of the multiset `s` is equal to zero if and only if the multiset itself is the zero multiset. In other words, a multiset `s` is empty (is the zero multiset) if and only if the count of its elements is zero.
More concisely: The theorem asserts that a multiset of type `α` has cardinality zero if and only if it is the empty multiset.
|
Mathlib.Data.Multiset.Basic._auxLemma.24
theorem Mathlib.Data.Multiset.Basic._auxLemma.24 :
∀ {α : Sort u_1} {p q : α → Prop}, (∀ (x : α), p x ∧ q x) = ((∀ (x : α), p x) ∧ ∀ (x : α), q x)
This theorem, `Mathlib.Data.Multiset.Basic._auxLemma.24`, states that for any type `α` and for any two predicates `p` and `q` on that type, the proposition that every `x` of type `α` satisfies both `p` and `q` is equivalent to the conjunction of the propositions that every `x` of type `α` satisfies `p` and every `x` of type `α` satisfies `q`. In other words, saying "every element has properties P and Q" is the same as saying "every element has property P and every element has property Q".
More concisely: For any type `α` and predicates `p` and `q` on `α`, `(∀ x : α, p x) ↔ (p : Prop) ∧ (q : Prop) ∧ (∀ x : α, q x)` (The proposition that every element of a type `α` satisfies both predicates `p` and `q` is equivalent to the conjunction of the propositions that every element satisfies `p` and every element satisfies `q`.)
|
Multiset.coe_count
theorem Multiset.coe_count :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), Multiset.count a ↑l = List.count a l
The theorem `Multiset.coe_count` states that, for any type `α` with a decidable equality, and any element `a` of type `α` and list `l` of type `α`, the multiplicity of `a` in the multiset representation of `l` (i.e., `Multiset.count a ↑l`) is equal to the number of occurrences of `a` in `l` itself (i.e., `List.count a l`). In other words, converting a list to a multiset does not change the count of any specific element in the collection.
More concisely: For any type `α` with decidable equality and list `l` of elements from `α`, the number of occurrences of an element `a` in the list equals the multiplicity of `a` in the multiset representation of `l`. (i.e., `List.count a l = Multiset.count a (Multiset.ofList l)`)
|
Multiset.filter_add
theorem Multiset.filter_add :
∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s t : Multiset α),
Multiset.filter p (s + t) = Multiset.filter p s + Multiset.filter p t
The theorem `Multiset.filter_add` states that for any type `α`, a predicate `p` (that can be decided for every element of type `α`), and two multisets `s` and `t` of type `α`, the result of filtering (i.e., keeping only those elements that satisfy the predicate `p`) the multiset formed by adding `s` and `t` (denoted as `s + t`) is the same as the result of adding the multisets obtained by filtering `s` and `t` separately (denoted as `Multiset.filter p s + Multiset.filter p t`). In simpler words, filtering a combined multiset is the same as combining the filtered multisets.
More concisely: For any type `α` and predicate `p`, the multiset obtained by filtering `p` on the sum of two multisets `s` and `t` equals the sum of the multisets obtained by filtering `p` on `s` and `t` separately.
|
Multiset.mem_of_subset
theorem Multiset.mem_of_subset : ∀ {α : Type u_1} {s t : Multiset α} {a : α}, s ⊆ t → a ∈ s → a ∈ t
The theorem `Multiset.mem_of_subset` states that for any type `α`, and for any two multiset `s` and `t` of type `α`, if `s` is a subset of `t` and if an element `a` of type `α` is in `s`, then `a` is also in `t`. In other words, if a multiset is a subset of another multiset, then any element in the subset is also an element of the larger set. This is a basic property of subset relationships in set theory.
More concisely: If `s` is a subset of `t` and `a` is in `s`, then `a` is in `t`. (In the context of multisets, "a is in `s`" means that `s` contains `a` with some multiplicity.)
|
Multiset.map_injective
theorem Multiset.map_injective :
∀ {α : Type u_1} {β : Type v} {f : α → β}, Function.Injective f → Function.Injective (Multiset.map f)
The theorem `Multiset.map_injective` states that for any types `α` and `β`, and any function `f` from `α` to `β`, if `f` is injective (i.e., it never maps different elements of `α` to the same element of `β`), then the function `Multiset.map f`, which applies `f` to each element of a multiset, is also injective. In other words, if `f` never produces the same output from different inputs, then neither does `Multiset.map f` when applied to multisets.
More concisely: If `f: α → β` is an injective function, then `Multiset.map f` preserves the injectivity property on multisets of type `α`.
|
Multiset.card_map
theorem Multiset.card_map :
∀ {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α), Multiset.card (Multiset.map f s) = Multiset.card s := by
sorry
The theorem `Multiset.card_map` states that for any function `f` of type `α → β` and any multiset `s` of type `α`, the cardinality of the multiset obtained by mapping `f` over `s` is equal to the cardinality of the original multiset `s`. In other words, applying a function to each element of a multiset does not change its size or cardinality.
More concisely: For any function `f` and multiset `s`, the cardinality of the multiset obtained by mapping `f` over `s` is equal to the cardinality of `s`.
|
Multiset.add_eq_union_iff_disjoint
theorem Multiset.add_eq_union_iff_disjoint :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s + t = s ∪ t ↔ s.Disjoint t
The theorem `Multiset.add_eq_union_iff_disjoint` states that for any type `α` with decidable equality and any two multisets `s` and `t` of type `α`, the sum of `s` and `t` is equal to the union of `s` and `t` if and only if `s` and `t` are disjoint. Here, a multiset is a generalization of a set that allows multiple instances of the elements, and two multisets are said to be disjoint if they don't have any element in common. The sum of two multisets includes all elements from both, potentially with duplicates, while their union includes each element only once. Therefore, their sum and union are equal if and only if there are no common elements, i.e., they are disjoint.
More concisely: For any type `α` with decidable equality, two multisets `s` and `t` of type `α` have equal sum and union if and only if they are disjoint.
|
Multiset.map_const
theorem Multiset.map_const :
∀ {α : Type u_1} {β : Type v} (s : Multiset α) (b : β),
Multiset.map (Function.const α b) s = Multiset.replicate (Multiset.card s) b
This theorem states that for any multiset `s` of type `α` and any value `b` of type `β`, if we apply `Multiset.map` to `s` using the constant function with value `b` (`Function.const α b`), then the resulting multiset is equivalent to a multiset that contains only the value `b` repeated `Multiset.card s` times (`Multiset.replicate (Multiset.card s) b`). In other words, mapping a constant function over a multiset simply replaces every element in the multiset with the constant value, yielding a new multiset where the constant value is repeated as many times as the original multiset's cardinality.
More concisely: For any multiset `s` and value `b`, `Multiset.map (Function.const _ _) s = Multiset.replicate (Multiset.card s) b`.
|
Multiset.Subset.trans
theorem Multiset.Subset.trans : ∀ {α : Type u_1} {s t u : Multiset α}, s ⊆ t → t ⊆ u → s ⊆ u
This theorem states that for any type `α` and for any three multisets `s`, `t`, and `u` of that type, if `s` is a subset of `t` and `t` is a subset of `u`, then `s` is a subset of `u`. In other words, the subset relationship is transitive on multisets. This is analogous to the principle in set theory that if $A \subseteq B$ and $B \subseteq C$, then $A \subseteq C$.
More concisely: If `α` is a type and `s`, `t`, and `u` are multisets of `α` with `s ⊆ t` and `t ⊆ u`, then `s ⊆ u`.
|
Multiset.map_map
theorem Multiset.map_map :
∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (g : β → γ) (f : α → β) (s : Multiset α),
Multiset.map g (Multiset.map f s) = Multiset.map (g ∘ f) s
The theorem `Multiset.map_map` is about the composition and association of functions with the `map` operation in the context of multisets. Given three types `α`, `β`, and `γ`, and two functions `f : α → β` and `g : β → γ`, this theorem states that for any multiset `s` of type `α`, mapping `f` over `s` first and then mapping `g` over the result is equivalent to mapping the composition of `g` and `f` (i.e., `g ∘ f`) over `s` directly. This can be seen as a kind of associativity property for the `map` operation on multisets, aligning with the common intuition from functional programming.
More concisely: For any multisets `s` of type `α`, the application of functions `g ∘ f` and `g ∘ Map (f) s` to `s` is equal.
|
Multiset.exists_cons_of_mem
theorem Multiset.exists_cons_of_mem : ∀ {α : Type u_1} {s : Multiset α} {a : α}, a ∈ s → ∃ t, s = a ::ₘ t
This theorem states that for any type `α`, multiset `s` of type `α`, and element `a` of type `α`, if `a` is an element of `s`, then there exists a multiset `t` (also of type `α`) such that `s` is equivalent to the multiset obtained by adding `a` to `t` (denoted as `a ::ₘ t`). In other words, if an element is in a multiset, then we can express that multiset as the "cons" of that element and another multiset.
More concisely: For any type `α`, multiset `s` of type `α`, and element `a` of type `α` in `s`, there exists a multiset `t` such that `s` equals the multiset obtained by adding `a` to `t` (denoted as `a :: t`).
|
Multiset.eq_of_le_of_card_le
theorem Multiset.eq_of_le_of_card_le :
∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → Multiset.card t ≤ Multiset.card s → s = t
This theorem states that for any two multisets `s` and `t` of any type `α`, if `s` is a sub-multiset of `t` (denoted by `s ≤ t`) and the cardinality of `t` (i.e., the total number of elements in `t`, including duplicates) is less than or equal to the cardinality of `s`, then `s` is equal to `t`. This essentially means that if a multiset is a subset of another and they have the same cardinality, they must be the same multiset.
More concisely: If two multisets `s` and `t` of type `α` satisfy `s ≤ t` and the cardinality of `t` is less than or equal to that of `s`, then `s = t`.
|
Multiset.attach_map_val
theorem Multiset.attach_map_val : ∀ {α : Type u_1} (s : Multiset α), Multiset.map Subtype.val s.attach = s
The theorem `Multiset.attach_map_val` states that for all types `α` and for every multiset `s` of that type, when we "attach" a proof that each element `a` belongs to `s` (via `Multiset.attach`) and then map the `Subtype.val` function (which retrieves the underlying element from the subtype) over this attached multiset, we recover the original multiset `s`. In other words, attaching proofs of membership to elements of the multiset and then stripping them away effectively acts as an identity operation on the original multiset.
More concisely: For all types `α` and multisets `s` of `α`, `Multiset.attach s (λ a h := h) = s`.
|
Multiset.cons_coe
theorem Multiset.cons_coe : ∀ {α : Type u_1} (a : α) (l : List α), a ::ₘ ↑l = ↑(a :: l)
This theorem, `Multiset.cons_coe`, states that for any given type `α` and any element `a` of type `α` and list `l` of type `α`, prepending (`cons`) the element `a` to the multiset that results from coercing (`↑`) the list `l` to a multiset equals the multiset that results from coercing the list obtained by prepending `a` to `l`. In other words, prepending an element to a list and then converting it to a multiset is the same as converting the list to a multiset and then prepending the element.
More concisely: For any type `α` and element `a` of type `α` and list `l` of type `α`, the multiset obtained by prepending `a` to the multiset of `l` is equal to the multiset obtained by coercing the list obtained by prepending `a` to `l`.
|
Multiset.toList_eq_nil
theorem Multiset.toList_eq_nil : ∀ {α : Type u_1} {s : Multiset α}, s.toList = [] ↔ s = 0
This theorem states that for any type `α` and any multiset `s` of type `α`, the list derived from `s` using `Multiset.toList` is empty if and only if `s` itself is the zero multiset. In other words, a multiset `s` is considered empty (equivalent to the zero multiset) if the list obtained from `s` is an empty list.
More concisely: For any type `α`, the multiset `s` of type `α` is the zero multiset if and only if `Multiset.toList s` is an empty list.
|
Multiset.sub_zero
theorem Multiset.sub_zero : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s - 0 = s
This theorem states a special case of `tsub_zero`, and it's recommended to use `tsub_zero` instead of this theorem. However, this theorem is necessary for proving `OrderedSub (Multiset α)`. The theorem explicitly states that for any type `α` that has decidable equality (i.e., for any two values of type `α`, it is decidable whether they are equal), and for any multiset `s` of type `α`, the result of subtracting the zero multiset (`0`) from `s` is `s` itself. In other words, the subtraction of an empty multiset from any multiset `s` leaves `s` unchanged.
More concisely: For any type `α` with decidable equality and any multiset `s` of type `α`, `s - 0 = s` holds. (Here, `-` denotes multiset subtraction and `0` denotes the zero multiset.)
|
Multiset.countP_eq_card_filter
theorem Multiset.countP_eq_card_filter :
∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α),
Multiset.countP p s = Multiset.card (Multiset.filter p s)
This theorem states that for any type `α`, any predicate `p` on `α` that's decidable, and any multiset `s` of elements of type `α`, the count of elements in `s` that satisfy the predicate `p` (`Multiset.countP p s`) is equal to the cardinality or size (`Multiset.card`) of the multiset obtained by filtering `s` to only include elements that satisfy `p` (`Multiset.filter p s`). In other words, counting elements in the original multiset that satisfy a certain property is the same as filtering the multiset for that property and counting the elements in the resulting multiset.
More concisely: For any type `α`, decidable predicate `p` on `α`, and multiset `s` of elements from `α`, the number of elements in `s` satisfying `p` equals the cardinality of the multiset `Multiset.filter p s`.
|
Mathlib.Data.Multiset.Basic._auxLemma.17
theorem Mathlib.Data.Multiset.Basic._auxLemma.17 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem states that for any type `α` and any two elements `a` and `b` of that type, the proposition `a = b` is equivalent to the proposition `b = a`. In other words, equality is symmetric in Lean 4, meaning if `a` equals `b`, then `b` also equals `a`.
More concisely: For any type `α` and elements `a, b : α`, the proposition `a = b` is equivalent to `b = a`. (Equality is reflexive and symmetric.)
|
Multiset.eq_zero_iff_forall_not_mem
theorem Multiset.eq_zero_iff_forall_not_mem : ∀ {α : Type u_1} {s : Multiset α}, s = 0 ↔ ∀ (a : α), a ∉ s
This theorem states that for any type `α` and any multiset `s` of type `α`, `s` is equivalent to zero if and only if for all elements `a` of type `α`, `a` does not belong to `s`. In other words, a multiset is empty if and only if no element of the underlying type is a member of the multiset.
More concisely: A multiset of type `α` is equivalent to the empty multiset if and only if no element of type `α` is in the multiset.
|
Multiset.recOn_cons
theorem Multiset.recOn_cons :
∀ {α : Type u_1} {C : Multiset α → Sort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)}
{C_cons_heq :
∀ (a a' : α) (m : Multiset α) (b : C m),
HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))}
(a : α) (m : Multiset α), (a ::ₘ m).recOn C_0 C_cons C_cons_heq = C_cons a m (m.recOn C_0 C_cons C_cons_heq)
The theorem `Multiset.recOn_cons` is about the recursion on multisets in Lean 4. For any type `α` and a function `C` from multisets of `α` to some type, along with a base case `C_0` for the empty multiset, a construction function `C_cons` for adding an element to a multiset, and a proof `C_cons_heq` of the compatibility of `C_cons` with the equivalence relation on multisets, this theorem states that the recursion on a multiset constructed by adding an element `a` to a multiset `m` is equal to applying `C_cons` to `a`, `m`, and the recursion on `m`. In more intuitive terms, it says that performing the recursion operation on a multiset `a ::ₘ m` is the same as first performing the recursion on `m` and then adding `a` to the result.
More concisely: For any function `C` from multisets to a type with base case `C_0` and recursion step `C_cons` satisfying `C_cons_heq`, the recursion on a multiset `m` extended by an element `a` is equal to applying `C_cons` to `a`, `m`, and the recursion result on `m`. In mathematical notation: `(C _ _).rec (a ::ₘ m) = C_cons a (C _ m)`.
|
Multiset.le_iff_count
theorem Multiset.le_iff_count :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α},
s ≤ t ↔ ∀ (a : α), Multiset.count a s ≤ Multiset.count a t
This theorem establishes a condition for determining the partial order (`≤`) between two multisets `s` and `t` of type `α`. Here, `α` is any type for which equality is decidable. The theorem asserts that `s` is less than or equal to `t` if and only if for every element `a` of type `α`, the multiplicity of `a` in `s` (i.e., the number of times `a` appears in `s`) is less than or equal to the multiplicity of `a` in `t`. In other words, `s` is a sub-multiset of `t` if every element in `s` occurs in `t` at least as many times as in `s`.
More concisely: For any type `α` where equality is decidable, two multisets `s` and `t` of type `α` satisfy `s ≤ t` if and only if for all `a` in `α`, the multiplicity of `a` in `s` is less than or equal to the multiplicity of `a` in `t`.
|
Multiset.not_mem_zero
theorem Multiset.not_mem_zero : ∀ {α : Type u_1} (a : α), a ∉ 0
This theorem states that for any type `α` and any element `a` of type `α`, `a` is not a member of the empty multiset (`0`). In other words, no element can be found in an empty multiset, regardless of its type.
More concisely: For any type `α` and any empty multiset `M` of type `multiset α`, it is not the case that `a ∈ M` for any `a : α`.
|
Multiset.coe_replicate
theorem Multiset.coe_replicate : ∀ {α : Type u_1} (n : ℕ) (a : α), ↑(List.replicate n a) = Multiset.replicate n a := by
sorry
The theorem `Multiset.coe_replicate` states that for any type `α`, any natural number `n`, and any element `a` of type `α`, converting a list that is generated by replicating `a` `n` times to a multiset results in the same multiset as directly replicating `a` `n` times in a multiset. In other words, the list replication followed by conversion to multiset is the same as multiset replication.
More concisely: For any type `α`, natural number `n`, and element `a` of type `α`, the multiset obtained from replicating `a` `n` times in a list and then converting to a multiset equals the multiset obtained by directly replicating `a` `n` times in a multiset.
|
Multiset.le_union_left
theorem Multiset.le_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ≤ s ∪ t
The theorem `Multiset.le_union_left` states that for any type `α` which has a decidable equality relation, and for any two multisets `s` and `t` of type `α`, the multiset `s` is a sub-multiset of the union of `s` and `t`. This means that all elements in `s` are also found in the union of `s` and `t`. This is a fundamental property of union operations in the context of multisets (or sets, generally).
More concisely: For any decidably equal type `α` and multisets `s` and `t` of type `α`, `s` is a sub-multiset of the union `s ∪ t`.
|
Multiset.of_mem_filter
theorem Multiset.of_mem_filter :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} {s : Multiset α}, a ∈ Multiset.filter p s → p a
This theorem states that for any type `α`, any decidable predicate `p` on `α`, any element `a` of type `α`, and any multiset `s` of `α`, if `a` is an element of the multiset obtained by filtering `s` with `p`, then `a` must satisfy the predicate `p`. In simpler terms, any element that remains in a multiset after applying a filter must satisfy the condition imposed by the filter.
More concisely: If `α` is a type, `p` is a decidable predicate on `α`, `a` is an element of `α`, and `s` is a multiset of `α` such that `a` is an element of the multiset obtained by filtering `s` with `p`, then `p(a)` holds.
|
Multiset.filter_eq_self
theorem Multiset.filter_eq_self :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α}, Multiset.filter p s = s ↔ ∀ a ∈ s, p a
The theorem `Multiset.filter_eq_self` states that for any type `α`, any decidable predicate `p` on `α`, and any multiset `s` of `α`, the multiset resulting from filtering `s` with the predicate `p` is equal to `s` if and only if every element `a` of `s` satisfies the predicate `p`. In other words, the multiset obtained by keeping only the elements of `s` that satisfy `p` is the same as `s` precisely when all elements of `s` satisfy `p`.
More concisely: For any type `α`, decidable predicate `p` on `α`, and multiset `s` of `α`, `Multiset.filter p s = s` if and only if `∀ a ∈ s, p a`.
|
Multiset.erase_le
theorem Multiset.erase_le : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), s.erase a ≤ s
This theorem states that for any given type `α` which has decidable equality, for any element `a` of type `α`, and for any multiset `s` of elements of type `α`, the multiset that results from erasing `a` from `s` is always less than or equal to the original multiset `s`. In other words, removing an element from a multiset will not result in a multiset larger than the original one.
More concisely: For any decidably equal type `α` and multiset `s` of elements from `α`, the multiset obtained by removing any element `a` from `s` is a sub-multiset of `s`.
|
Multiset.map_congr
theorem Multiset.map_congr :
∀ {α : Type u_1} {β : Type v} {f g : α → β} {s t : Multiset α},
s = t → (∀ x ∈ t, f x = g x) → Multiset.map f s = Multiset.map g t
The theorem `Multiset.map_congr` states that for any types `α`, `β` and any two functions `f` and `g` from `α` to `β`, and any two multisets `s` and `t` of type `α`, if `s` equals `t` and for every element `x` in `t`, `f(x)` equals `g(x)`, then the multiset obtained by mapping `f` over `s` is equal to the multiset obtained by mapping `g` over `t`. This is just a way of saying that the mapping of equivalent functions over equal multisets produces equal results.
More concisely: If `α` is a type, `f` and `g` are functions from `α` to `β`, `s` and `t` are multisets of `α`, `s = t`, and `f(x) = g(x)` for all `x ∈ t`, then `Multiset.map f s = Multiset.map g t`.
|
Mathlib.Data.Multiset.Basic._auxLemma.4
theorem Mathlib.Data.Multiset.Basic._auxLemma.4 :
∀ {α : Type u_1} (a : α) {s t : Multiset α}, (a ::ₘ s = a ::ₘ t) = (s = t)
This theorem states that for any type `α`, and any given element `a` of that type, as well as any two multisets `s` and `t` of the same type, the condition that prepending `a` to `s` results in the same multiset as prepending `a` to `t` is equivalent to `s` and `t` being the same multiset. Here, the operator `::ₘ` represents the operation of prepending an element to a multiset.
More concisely: For any type `α` and elements `a` of type `α`, the multisets `s` and `t` of type `set α` are equal if and only if prepending `a` to `s` results in the same multiset as prepending `a` to `t`, denoted by `(a :: s) = (a :: t)`.
|
Multiset.rel_flip
theorem Multiset.rel_flip :
∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset β} {t : Multiset α},
Multiset.Rel (flip r) s t ↔ Multiset.Rel r t s
This theorem is about the relation between multisets and a flipped relation. For any types `α` and `β` and any relation `r` from `α` to `β`, and any multiset `s` of type `β` and `t` of type `α`, the multiset relation of the flipped relation `r` and the multisets `s` and `t` is equivalent to the multiset relation of `r` and the multisets `t` and `s`. In other words, flipping the inputs of the relation `r` does not change the way it relates the multisets `s` and `t` in the context of `Multiset.Rel`.
More concisely: For any relations $r$ from type $\alpha$ to type $\beta$, multisets $s$ of type $\beta$, and $t$ of type $\alpha$, the multiset relations $s \multimap r \multimap t$ and $t \multimap r \multimap s$ are equal in the context of multisets.
|
Multiset.mem_of_mem_erase
theorem Multiset.mem_of_mem_erase :
∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Multiset α}, a ∈ s.erase b → a ∈ s
This theorem states that for any type `α` that has decidable equality, any given elements `a` and `b` of `α`, and any multiset `s` of `α`, if `a` is an element of the multiset obtained by erasing `b` from `s` (`Multiset.erase s b`), then `a` is also an element of the original multiset `s`. In other words, erasing an element from a multiset doesn't indicate the presence of other elements in the modified multiset.
More concisely: If `α` has decidable equality, `a` is an element of the multiset `s` implies `a` is an element of `Multiset.erase s b`.
|
Mathlib.Data.Multiset.Basic._auxLemma.56
theorem Mathlib.Data.Multiset.Basic._auxLemma.56 :
∀ {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β}, (Multiset.map f s = 0) = (s = 0)
This theorem states that for any type `α` and `β`, any multiset `s` of type `α`, and any function `f` from `α` to `β`, the multiset resulting from mapping function `f` over the multiset `s` is empty if and only if the original multiset `s` is empty. In other words, an operation of mapping a function over a multiset will yield an empty multiset if and only if the original multiset was empty.
More concisely: For any type `α`, any multiset `s` of type `α`, and any function `f` from `α` to any type `β`, if multiset `s` is empty then the multiset obtained by applying function `f` to every element in `s` is also empty.
|
Multiset.card_lt_of_lt
theorem Multiset.card_lt_of_lt : ∀ {α : Type u_1} {s t : Multiset α}, s < t → Multiset.card s < Multiset.card t := by
sorry
This theorem, referred to as an alias of `Multiset.card_lt_card`, states that for any type `α`, and for any two multisets `s` and `t` of this type, if `s` is less than `t`, then the cardinality of `s` (obtained using `Multiset.card s`) is also less than the cardinality of `t` (obtained using `Multiset.card t`). In other words, if one multiset is considered to be "less" than another, then the count of the elements in the first multiset is less than the count of the elements in the second multiset.
More concisely: For any type `α` and multisets `s` and `t` of type `Multiset α`, if `s` is less than `t` then `Multiset.card s` < `Multiset.card t`.
|
Multiset.rel_map
theorem Multiset.rel_map :
∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {δ : Type u_3} {p : γ → δ → Prop} {s : Multiset α} {t : Multiset β}
{f : α → γ} {g : β → δ},
Multiset.Rel p (Multiset.map f s) (Multiset.map g t) ↔ Multiset.Rel (fun a b => p (f a) (g b)) s t
The theorem `Multiset.rel_map` states that for any types `α`, `β`, `γ`, `δ`, a binary relation `p` between `γ` and `δ`, multisets `s` of type `α` and `t` of type `β`, and functions `f` from `α` to `γ` and `g` from `β` to `δ`, the relation `p` holds between the multisets obtained by mapping `f` and `g` over `s` and `t` respectively if and only if the relation `p` composed with `f` and `g` holds between `s` and `t`. In other words, mapping `f` and `g` over `s` and `t` and then applying the relation `p` is equivalent to directly applying the relation `p` composed with `f` and `g` to `s` and `t`.
More concisely: For multisets $s$ of type $\alpha$, $t$ of type $\beta$, functions $f:\alpha\to\gamma$, $g:\beta\to\delta$, and a binary relation $p$ between $\gamma$ and $\delta$, we have $s\mathbin{R}t$ if and only if $(f\circ s)\mathbin{R}(g\circ t)$, where $\mathbin{R}$ denotes the relation $p$.
|
Mathlib.Data.Multiset.Basic._auxLemma.7
theorem Mathlib.Data.Multiset.Basic._auxLemma.7 : ∀ {α : Type u_1} (a : α), (a ∈ 0) = False
This theorem states that for any type `α` and any element `a` of type `α`, `a` does not belong to the empty multiset. In terms of set theory, this is stating that no element belongs to the empty set.
More concisely: The theorem asserts that there is no element in an empty multiset. (Or equivalently, no element belongs to the empty set in set theory.)
|
Multiset.map_lt_map
theorem Multiset.map_lt_map :
∀ {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α}, s < t → Multiset.map f s < Multiset.map f t := by
sorry
The theorem `Multiset.map_lt_map` states that for any given types `α` and `β`, a function `f` from `α` to `β`, and multisets `s` and `t` of type `α`, if `s` is less than `t`, then the multiset obtained by mapping `f` over `s` is less than the multiset obtained by mapping `f` over `t`. In other words, if a multiset `s` is a proper subset of another multiset `t` (i.e., `s` has fewer elements than `t` or `s` is equal to `t` except for at least one additional element in `t`), applying a function to each element of `s` results in a multiset that is also a proper subset of the result of applying the same function to each element of `t`.
More concisely: For any types `α`, multisets `s` and `t` of `α`, and function `f` from `α` to `β`, if `s` is a proper subset of `t`, then `Map f s` is a proper subset of `Map f t`.
|
Multiset.lt_iff_cons_le
theorem Multiset.lt_iff_cons_le : ∀ {α : Type u_1} {s t : Multiset α}, s < t ↔ ∃ a, a ::ₘ s ≤ t
This theorem states that for any two multisets `s` and `t` of a type `α`, `s` is less than `t` if and only if there exists an element `a` of type `α` such that the multiset obtained by consing `a` onto `s` is less than or equal to `t`. In other words, a multiset `s` is less than another multiset `t` when there is an element `a` that can be added to `s` to create a multiset that is no greater than `t`. Here, `::ₘ` is the operation of adding an element to a multiset.
More concisely: For any multisets `s` and `t` of type `α`, `s` is less than `t` if and only if there exists an `α` element `a` such that `s :: a ≤ t`.
|
Multiset.filter_le_filter
theorem Multiset.filter_le_filter :
∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {s t : Multiset α},
s ≤ t → Multiset.filter p s ≤ Multiset.filter p t
The theorem `Multiset.filter_le_filter` states that for any type `α`, any decidable predicate `p` on `α`, and any two multisets `s` and `t` of type `α`, if `s` is a sub-multiset of `t` (that is, `s` is less than or equal to `t`), then the multiset obtained by filtering `s` with predicate `p` is also a sub-multiset of the multiset obtained by filtering `t` with the same predicate. This means that applying a filter to a subset of a multiset will yield a result that is a subset of the result of applying the same filter to the entire multiset.
More concisely: If `s` is a sub-multiset of `t` and `p` is a decidable predicate on type `α`, then `Multiset.filter p s` is a sub-multiset of `Multiset.filter p t`.
|
Multiset.forall_mem_map_iff
theorem Multiset.forall_mem_map_iff :
∀ {α : Type u_1} {β : Type v} {f : α → β} {p : β → Prop} {s : Multiset α},
(∀ y ∈ Multiset.map f s, p y) ↔ ∀ x ∈ s, p (f x)
This theorem states that for any type `α` and `β`, a function `f` from `α` to `β`, a predicate `p` on `β`, and a multiset `s` of type `α`, the property that every element `y` in the multiset obtained by mapping `f` over `s` satisfies the predicate `p` is equivalent to the property that for every element `x` in `s`, `p` is satisfied by `f x`. In other words, the predicate `p` holds for all elements in the image of `s` under `f` if and only if `p` holds for all images under `f` of elements in `s`.
More concisely: For any function $f: \alpha \to \beta$, predicate $p \subseteq \beta$, multiset $s \subseteq \alpha$, the property that for all $y \in \text{image}(f, s)$, $p(y)$ holds if and only if for all $x \in s$, $p(f(x))$ holds.
|
Multiset.inter_le_right
theorem Multiset.inter_le_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ∩ t ≤ t
The theorem `Multiset.inter_le_right` states that for any type `α` which has decidable equality (i.e., for any two elements `a` and `b` of type `α`, it is possible to decide whether `a = b`), and for any two multisets `s` and `t` of type `α`, the intersection of `s` and `t` is a sub-multiset of `t`. In other words, all elements of the intersection of `s` and `t` are also elements of `t`. This fits the intuitive understanding of intersection from set theory.
More concisely: For any decidably equal types `α` and any multisets `s` and `t` of type `α`, the intersection of `s` and `t` is a sub-multiset of `t`.
|
Multiset.mem_singleton_self
theorem Multiset.mem_singleton_self : ∀ {α : Type u_1} (a : α), a ∈ {a}
This theorem, `Multiset.mem_singleton_self`, states that for any type `α` and any element `a` of that type, `a` is an element of the singleton multiset that only contains `a`. In mathematical terms, for all `a` in `α`, `a` is in the multiset `{a}`. This is a fundamental property of singleton multisets, and it holds true for any type `α`.
More concisely: For any type `α` and element `a` in `α`, `a` belongs to the singleton multiset `{a}`.
|
Multiset.cons_erase
theorem Multiset.cons_erase :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {a : α}, a ∈ s → a ::ₘ s.erase a = s
The theorem `Multiset.cons_erase` states that for any type `α` that has decidable equality (`DecidableEq α`), any multiset `s` of elements of type `α`, and any element `a` of type `α`; if `a` belongs to `s`, then adding `a` to the multiset obtained from `s` by erasing one occurrence of `a` (`a ::ₘ Multiset.erase s a`) gives back the original multiset `s`. In other words, if an element is in a multiset, then removing it and adding it back results in the original multiset.
More concisely: For any type `α` with decidable equality and any multiset `s` of elements `α` with `a` being an element of `s`, `Multiset.erase (a :: s) a = s`.
|
Mathlib.Data.Multiset.Basic._auxLemma.65
theorem Mathlib.Data.Multiset.Basic._auxLemma.65 :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, (a ∈ s ∪ t) = (a ∈ s ∨ a ∈ t)
This theorem states that for any type `α` with decidable equality, and for any multisets `s` and `t` of type `α` and any element `a` of type `α`, the statement "`a` is in the union of `s` and `t`" is equivalent to the statement "`a` is in `s` or `a` is in `t`". Here, a multiset is a set with duplicate elements allowed, and the union of two multisets `s` and `t` is a multiset that contains all the elements from `s` and `t`, including duplicates.
More concisely: For any type `α` with decidable equality, and for any multisets `s` and `t` of type `α` and any element `a` of type `α`, `a` is in the union of `s` and `t` if and only if `a` is in `s` or `a` is in `t`.
|
Multiset.count_singleton
theorem Multiset.count_singleton :
∀ {α : Type u_1} [inst : DecidableEq α] (a b : α), Multiset.count a {b} = if a = b then 1 else 0
This theorem states that for any type `α` that has decidable equality (denoted by `DecidableEq α`), given any two elements `a` and `b` of type `α`, the count of `a` in a singleton multiset containing only `b` (denoted by `{b}`) is 1 if `a` is equal to `b` and 0 otherwise. In other words, if `a` and `b` are the same, `a` appears once in the multiset `{b}`, otherwise `a` does not appear in the multiset `{b}`.
More concisely: For any type `α` with decidable equality and any `a, b : α`, the size of `a` in the singleton multiset `{b}` equals 1 if `a = b`, and 0 otherwise.
|
Multiset.add_cons
theorem Multiset.add_cons : ∀ {α : Type u_1} (a : α) (s t : Multiset α), s + a ::ₘ t = a ::ₘ (s + t)
The theorem `Multiset.add_cons` states that for all types `α`, and for all elements `a` of type `α`, and multisets `s` and `t` of type `α`, appending an element `a` to the multiset `t`, and then adding the resulting multiset to `s`, is the same as adding `s` and `t` together and then prepending `a` to the resulting multiset. In other words, the order in which we add the single element `a` and the multiset `t` doesn't change the resulting multiset. This theorem captures a kind of commutativity property of adding a single element and a multiset in the context of multisets.
More concisely: For all types `α` and multisets `s` and `t` of type `α`, `Multiset.add_cons s a (Multiset.union s t) = Multiset.insert a (Multiset.union s t)`.
|
Multiset.cons_le_cons_iff
theorem Multiset.cons_le_cons_iff : ∀ {α : Type u_1} {s t : Multiset α} (a : α), a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t
This theorem states that for any type `α`, and for any multisets `s` and `t` of type `α`, and any element `a` of type `α`, adding `a` to the front of `s` gives a multiset that is less than or equal to (in the sense of multiset ordering) adding `a` to the front of `t` if and only if the multiset `s` is less than or equal to the multiset `t`.
More concisely: For any type `α` and multisets `s` and `t` of type `α`, `add_front a s ≤ add_front a t` if and only if `s ≤ t`, where `≤` denotes multiset ordering and `add_front` adds an element to the front of a multiset.
|
Multiset.mem_cons
theorem Multiset.mem_cons : ∀ {α : Type u_1} {a b : α} {s : Multiset α}, a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s
The theorem `Multiset.mem_cons` states that for any type `α`, and any elements `a` and `b` of type `α`, and any multiset `s` of type `α`, the element `a` belongs to the multiset formed by adding `b` to `s` if and only if `a` is equal to `b` or `a` belongs to `s`. In other words, an element `a` is in the multiset created by prefixing `b` to `s` exactly when `a` is either `b` or an element of `s`.
More concisely: For any type α and multiset s of α, an element a belongs to the multiset formed by adding an element b to s if and only if a is equal to b or is an element of s.
|
Multiset.filter_cons_of_pos
theorem Multiset.filter_cons_of_pos :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α),
p a → Multiset.filter p (a ::ₘ s) = a ::ₘ Multiset.filter p s
The theorem `Multiset.filter_cons_of_pos` states that for any type `α`, any decidable predicate `p` over `α`, any element `a` of type `α`, and any multiset `s` of type `α`, if `a` satisfies the predicate `p`, then filtering the multiset formed by adding `a` to `s` with the predicate `p` results in a multiset where `a` is added to the multiset obtained by filtering `s` with `p`. In other words, if we have a multiset `s` and an element `a` that satisfies a certain condition `p`, then the filtered multiset where `a` is added to `s` is the same as the multiset where `a` is added to the filtered `s`.
More concisely: For any type `α`, decidable predicate `p` over `α`, element `a` of type `α`, and multiset `s` of type `α`, if `a ∈ s.filter (p)`, then `a ∈ (s.filter (p) : set α).insert a`.
|
Multiset.card_add
theorem Multiset.card_add :
∀ {α : Type u_1} (s t : Multiset α), Multiset.card (s + t) = Multiset.card s + Multiset.card t
This theorem states that for any type `α` and two multisets `s` and `t` of that type, the cardinality of the multiset obtained by adding `s` and `t` is equal to the sum of the cardinalities of `s` and `t`. In other words, the number of elements in the combined multiset `s + t` is equal to the total number of elements in `s` and `t` combined. This mirrors the principle in basic arithmetic that the total count of elements in two combined sets is the sum of the counts of elements in each individual set.
More concisely: The cardinality of the sum of two multisets is equal to the sum of their cardinalities.
|
Multiset.count_ne_zero
theorem Multiset.count_ne_zero :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {a : α}, Multiset.count a s ≠ 0 ↔ a ∈ s
This theorem states that for any type `α` that has decidable equality and any `a` of type `α` and `s` which is a multiset of `α`, the count of `a` in `s` is not zero if and only if `a` is an element of `s`. In other words, an element `a` belongs to a multiset `s` precisely when its count in `s` is non-zero.
More concisely: For any type `α` with decidable equality and any multiset `s` of `α` and element `a` of `α`, the count of `a` in `s` is non-zero if and only if `a` is a member of `s`.
|
Multiset.count_eq_zero_of_not_mem
theorem Multiset.count_eq_zero_of_not_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∉ s → Multiset.count a s = 0
The theorem `Multiset.count_eq_zero_of_not_mem` states that for any type `α` with decidable equality, an element `a` of type `α`, and a multiset `s` of elements of type `α`, if `a` is not a member of the multiset `s`, then the count of `a` in `s` is zero. In other words, if an element is not in a multiset, then its multiplicity or count in that multiset is zero.
More concisely: If `a` is not an element of multiset `s` over type `α` with decidable equality, then the count of `a` in `s` is zero.
|
Multiset.singleton_add
theorem Multiset.singleton_add : ∀ {α : Type u_1} (a : α) (s : Multiset α), {a} + s = a ::ₘ s
This theorem, `Multiset.singleton_add`, states that for all types `α` and for all elements `a` of type `α` and multisets `s` of type `α`, the addition of the singleton multiset containing `a` and the multiset `s` is equivalent to prepending `a` to `s`. Here, `a ::ₘ s` denotes the multiset obtained by adding the element `a` to the multiset `s`. The symbol `+` denotes the operation of combining two multisets into a single multiset.
More concisely: For all types α and elements a of α, adding the singleton multiset {a} to a multiset s is equivalent to prepending a to s. In Lean notation, a ::ₘ s = s + {a}.
|
Mathlib.Data.Multiset.Basic._auxLemma.55
theorem Mathlib.Data.Multiset.Basic._auxLemma.55 :
∀ {α : Type u_1} {β : Type v} {f : α → β} {b : β} {s : Multiset α}, (b ∈ Multiset.map f s) = ∃ a ∈ s, f a = b := by
sorry
This theorem states that for any types `α` and `β`, a function `f` from `α` to `β`, a value `b` of type `β`, and a multiset `s` of type `α`, `b` is in the multiset obtained by mapping `f` over `s` if and only if there exists a value `a` in `s` such that `f(a)` equals `b`. In mathematical terms, this means that if $b \in \text{map}(f, s)$ then there exists an $a \in s$ such that $f(a) = b$, and vice versa.
More concisely: For any function $f$ from type $\alpha$ to type $\beta$, value $b$ of type $\beta$, and multiset $s$ of type $\alpha$, $b$ is in the image of $f$ under $s$ if and only if there exists an element $a$ in $s$ such that $f(a) = b$. In symbols, $\exists a \in s.\, f(a) = b \iff b \in \text{map}(f, s)$.
|
Multiset.cons_swap
theorem Multiset.cons_swap : ∀ {α : Type u_1} (a b : α) (s : Multiset α), a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s
The theorem `Multiset.cons_swap` states that for all types α, and for any elements `a` and `b` of that type, and a multiset `s` of that type, prepending the multiset `s` first with `a` and then with `b` results in the same multiset as prepending `s` first with `b` and then with `a`. In other words, the order of elements added to the beginning of a multiset does not affect the resulting multiset. This follows from the fact that a multiset is a type of finite sets with duplicates allowed, and sets do not consider the order of their elements.
More concisely: For all types α and elements a, b of type α, and any multiset s of type α, the multisets [a] ++ s and b ++ [a] are equal, where [a] and [b] denote the singleton multisets.
|
Multiset.ext
theorem Multiset.ext :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α},
s = t ↔ ∀ (a : α), Multiset.count a s = Multiset.count a t
The theorem `Multiset.ext` states that for any type `α` with decidable equality and any two multisets `s` and `t` of type `α`, the multisets `s` and `t` are equal if and only if, for every element `a` of type `α`, the count of `a` in `s` is equal to the count of `a` in `t`. In other words, two multisets are considered equal when they have the same elements with the same multiplicities.
More concisely: Two multisets of type `α` are equal if and only if they have the same multiplicity for each element `α`.
|
Multiset.mem_attach
theorem Multiset.mem_attach : ∀ {α : Type u_1} (s : Multiset α) (x : { x // x ∈ s }), x ∈ s.attach
This theorem, `Multiset.mem_attach`, states that for any type `α` and any multiset `s` of this type, any element `x` of the type `{ x // x ∈ s }` (which denotes elements `x` such that `x` belongs to `s` along with a proof of this property), `x` is a member of the multiset obtained by attaching the proofs to the elements of `s` using the `Multiset.attach` function. Essentially, this theorem ensures that any element `x` that comes with a proof of membership in `s` is indeed found in the multiset resulting from the `Multiset.attach` operation applied to `s`.
More concisely: For any type `α` and multiset `s` of `α`, if `x ∈ s` then `x` is an element of the multiset obtained by attaching proofs to `s` using `Multiset.attach`.
|
Multiset.ext'
theorem Multiset.ext' :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α},
(∀ (a : α), Multiset.count a s = Multiset.count a t) → s = t
The theorem states that for any type 'α' with decidable equality and any two multisets 's' and 't' of this type, if the count of each element 'a' of type 'α' is the same in both 's' and 't', then 's' and 't' are equal. In simpler terms, two multisets are identical if they have the same counts for each element.
More concisely: If two multisets of a type with decidable equality have equal counts for each element, then they are equal.
|
Multiset.Subset.refl
theorem Multiset.Subset.refl : ∀ {α : Type u_1} (s : Multiset α), s ⊆ s
The theorem `Multiset.Subset.refl` states that for any type `α` and for any multiset `s` of type `α`, `s` is a subset of itself. In other words, the theorem asserts the reflexivity of the subset relation on multisets. This is a basic property of the subset relation in set theory.
More concisely: For any multiset `s` of type `α`, `s` is a subset of `s`.
|
Mathlib.Data.Multiset.Basic._auxLemma.1
theorem Mathlib.Data.Multiset.Basic._auxLemma.1 : ∀ {α : Type u_1} {l₁ l₂ : List α}, (↑l₁ = ↑l₂) = l₁.Perm l₂ := by
sorry
This theorem states that for any type `α` and any two lists `l₁` and `l₂` of that type, the condition of the two lists being equal when converted into multisets is equivalent to the two lists being permutations of each other. In other words, two lists are considered equal as multisets if and only if they can be obtained from each other by reordering the elements.
More concisely: For any type `α`, lists `l₁` and `l₂` of type `list α` are equal as multisets if and only if they are permutations of each other.
|
Multiset.card_pmap
theorem Multiset.card_pmap :
∀ {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a),
Multiset.card (Multiset.pmap f s H) = Multiset.card s
The theorem `Multiset.card_pmap` states that for any type `α` and `β`, a predicate `p` on `α`, a function `f` from `a` of type `α` satisfying the predicate `p` to `β`, a multiset `s` of type `α`, and a proof `H` that all elements of `s` satisfy `p`, the cardinality of the multiset obtained by applying the partially mapped function `f` to `s` is equal to the cardinality of `s`. In other words, applying a function to each element of a multiset does not change its size.
More concisely: For any multiset `s` of type `α`, function `f` from `α` to `β`, and proof `H` that all elements of `s` satisfy `p(x): α -> Prop`, the cardinalities of `s` and `{x : β | ∃ (y : α), p(y) ∧ f(y) = x}` are equal.
|
Multiset.leInductionOn
theorem Multiset.leInductionOn :
∀ {α : Type u_1} {C : Multiset α → Multiset α → Prop} {s t : Multiset α},
s ≤ t → (∀ {l₁ l₂ : List α}, l₁.Sublist l₂ → C ↑l₁ ↑l₂) → C s t
This theorem, called `Multiset.leInductionOn`, states that for any type `α` and any property `C` that can relate two multisets of type `α`, if one multiset `s` is less than or equal to another multiset `t` (in terms of a multiset inequality), then under the condition that the property `C` holds for any two lists `l₁` and `l₂` (of type `α`) such that `l₁` is a sublist of `l₂`, the property `C` also holds for the multisets `s` and `t`. Essentially, this theorem allows us to generalize a property from lists to multisets.
More concisely: Given a type `α` and a property `C` relating multisets of `α`, if `C` holds for all sublists `l₁` and `l₂` and `s ⊇ s'` implies `∀ l₁ ⊆ l₂, C(l₁, l₂) → C(s, s')`, then `C` holds for all multisets `s` and `t` with `s �leq t`.
|
Multiset.mem_map
theorem Multiset.mem_map :
∀ {α : Type u_1} {β : Type v} {f : α → β} {b : β} {s : Multiset α}, b ∈ Multiset.map f s ↔ ∃ a ∈ s, f a = b := by
sorry
The theorem `Multiset.mem_map` states that for any types `α` and `β`, a function `f` from `α` to `β`, an element `b` of type `β`, and a multiset `s` of type `α`, `b` is an element of the multiset obtained by mapping `f` over `s` if and only if there exists an element `a` in multiset `s` such that `f(a) = b`. In other words, an element is in the image of a multiset under a function if and only if it is the image of some element in the original multiset under that function.
More concisely: For any function $f:\alpha \to \beta$ and multiset $s:\mathit{Multiset}\ \alpha$, $b \in \mathit{map}\ f\ s$ if and only if there exists $a \in s$ such that $f(a) = b$.
|
Multiset.mem_filter
theorem Multiset.mem_filter :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} {s : Multiset α},
a ∈ Multiset.filter p s ↔ a ∈ s ∧ p a
This theorem, `Multiset.mem_filter`, states a property about filtering a multiset. Specifically, for any type `α`, a predicate `p` that is decidable for members of type `α`, an element `a` of type `α`, and a multiset `s` of elements of type `α`, an element `a` is in the filtered multiset (where the multiset `s` is filtered by the predicate `p`) if and only if the element `a` is in the original multiset `s` and the predicate `p` is true for `a`. In other words, the theorem provides a condition for membership in a filtered multiset - an item appears in the filtered version if it appears in the original and satisfies the filter condition.
More concisely: For any type `α`, decidable predicate `p` on `α`, multiset `s` over `α`, and `a` in `α`, `a` is in the filtered multiset `Multiset.filter p s` if and only if `a` is in `s` and `p(a)` holds.
|
Multiset.le_cons_of_not_mem
theorem Multiset.le_cons_of_not_mem : ∀ {α : Type u_1} {s t : Multiset α} {a : α}, a ∉ s → (s ≤ a ::ₘ t ↔ s ≤ t) := by
sorry
This theorem is about multisets in the field of mathematics. It states that for any type `α`, and for any multisets `s` and `t` of this type, along with any element `a` of the same type, if `a` is not a member of the multiset `s`, then `s` is less than or equal to the multiset formed by appending `a` to `t` (`a ::ₘ t`) if and only if `s` is less than or equal to `t`. Here, `≤` denotes the multiset inclusion relation, meaning that all elements of `s` are also elements of `t` or `a ::ₘ t`.
More concisely: For any type `α` and multisets `s` and `t` of type `α`, if `a ∉ s` then `s ≤ t` if and only if `s ≤ a ::ₘ t`.
|
Multiset.erase_cons_tail
theorem Multiset.erase_cons_tail :
∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} (s : Multiset α), b ≠ a → (b ::ₘ s).erase a = b ::ₘ s.erase a
The theorem `Multiset.erase_cons_tail` states that for any type `α` that has decidable equality (meaning that equality between any two elements of the type can be decided), and for any two elements `a` and `b` of type `α`, and a multiset `s` of type `α`, if `b` is not equal to `a`, then erasing `a` from the multiset that results from adding `b` to `s` (denoted `b ::ₘ s`) is the same as adding `b` to the multiset that results from erasing `a` from `s`. In other words, if `b` is not equal to `a`, then the order of adding `b` and erasing `a` does not matter.
More concisely: For any type `α` with decidable equality and any multisets `s` of type `α` and elements `a, b` not equal to each other, `b ::ₘ (a ::ₘ s) = b ::ₘ (erase a (s ::ₘ b))`.
|
Multiset.coe_erase
theorem Multiset.coe_erase :
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (a : α), (↑l).erase a = ↑(l.erase a)
This theorem states that for any type `α` with decidable equality and for any list `l` of type `α` and any element `a` of type `α`, the operation of erasing `a` from the multiset formed by `l` is the same as the operation of erasing `a` from `l` and then forming a multiset. In other words, when an element `a` is removed from the list `l` and the resulting list is converted into a multiset, it yields the same result as if `a` was removed after the list `l` was converted into a multiset.
More concisely: For any decidably equated type `α` and list `l` of length `n+1` in `α`, removing an element `a` from the multiset formed by `l` is equivalent to first removing `a` from `l` and then forming the multiset of the resulting list. In mathematical notation, `(multiset.erase a (multiset.ofList l)) = multiset.erase a l`.
|
Multiset.card_erase_of_mem
theorem Multiset.card_erase_of_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α},
a ∈ s → Multiset.card (s.erase a) = (Multiset.card s).pred
The theorem `Multiset.card_erase_of_mem` states that for any type `α` that has decidable equality and any multiset `s` of type `α`, if an element `a` of type `α` is in `s`, then the cardinality (number of elements) of the multiset obtained by erasing `a` from `s` is equal to the predecessor of the cardinality of `s`. In other words, if `a` is in `s`, removing `a` from `s` decreases the size of `s` by one.
More concisely: If `α` has decidable equality and `a` is in the multiset `s` of type `α`, then `card (s without {a}) = Suc (card s)`.
|
Multiset.le_union_right
theorem Multiset.le_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), t ≤ s ∪ t
The theorem `Multiset.le_union_right` states that for any type `α` that has decidable equality and for any two multisets `s` and `t` of type `α`, `t` is less than or equal to the union of `s` and `t`. Here, "less than or equal to" is defined in terms of the subset relation: a multiset `a` is less than or equal to a multiset `b` if `a` is a subset of `b`. This theorem essentially formalizes the intuitive idea that any set (or multiset, in this case) is always a subset of its union with any other set.
More concisely: For any type `α` with decidable equality and multisets `s` and `t` of type `α`, `t` is a subset of `s ∪ t`.
|
Multiset.filter_le
theorem Multiset.filter_le :
∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α), Multiset.filter p s ≤ s
The theorem `Multiset.filter_le` asserts that for any type `α`, any given decidable predicate `p` on elements of `α`, and any multiset `s` of type `α`, the multiset obtained by filtering `s` using the predicate `p` is a subset of (or equal to) `s`. In other words, no new elements are introduced in the multiset by the filter operation, it only potentially removes elements that don't satisfy the predicate.
More concisely: For any type `α`, decidable predicate `p` on `α`, and multiset `s` of type `α`, the filtered multiset `Multiset.filter p s` is a subset of `s`.
|
Multiset.cons_inter_of_neg
theorem Multiset.cons_inter_of_neg :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α}, a ∉ t → (a ::ₘ s) ∩ t = s ∩ t
This theorem states that for any type `α` that has decidable equality, given an element `a` of type `α` and two multisets `s` and `t` of type `α`, if `a` is not an element of `t`, then the intersection of `t` with the multiset formed by adding `a` to `s` is the same as the intersection of `s` and `t`. This theorem essentially shows that adding an element to a multiset does not change its intersection with another multiset, if that element is not in the other multiset.
More concisely: If `α` has decidable equality and `a ∉ t`, then intersect (s ∪ {a}) t = intersect s t.
|
Multiset.count_inter
theorem Multiset.count_inter :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α),
Multiset.count a (s ∩ t) = min (Multiset.count a s) (Multiset.count a t)
This theorem is about multisets in a given type `α` which has decidable equality. It states that for any element `a` in type `α`, and any two multisets `s` and `t` of type `α`, the multiplicity of the element `a` in the intersection of `s` and `t` is equal to the minimum of its multiplicity in `s` and its multiplicity in `t`. In other words, the number of occurrences of the element `a` in the intersection of two multisets is the same as the smallest number of occurrences of `a` in either of the original multisets.
More concisely: For multisets $s$ and $t$ over a type $\alpha$ with decidable equality, the multiplicity of any element $a$ in their intersection equals the minimum of its multiplicity in $s$ and its multiplicity in $t$.
|
Multiset.card_lt_card
theorem Multiset.card_lt_card : ∀ {α : Type u_1} {s t : Multiset α}, s < t → Multiset.card s < Multiset.card t := by
sorry
This theorem, `Multiset.card_lt_card`, states that for any type `α` and any two multisets `s` and `t` of that type, if `s` is less than `t` then the cardinality of `s` (i.e., the sum of the multiplicities of all its elements, which is effectively the length of the list representing `s`) is less than the cardinality of `t`. In other words, if one multiset is smaller than another, then the number of elements (counting repeats) in the first multiset is less than the number of elements in the second.
More concisely: For any type α and multisets s and t of that type, if s < t then |s| < |t|, where |.| denotes the cardinality.
|
Multiset.card_attach
theorem Multiset.card_attach : ∀ {α : Type u_1} {m : Multiset α}, Multiset.card m.attach = Multiset.card m
The theorem `Multiset.card_attach` states that for any multiset `m` of a certain type `α`, the cardinality (or the number of elements) of the multiset obtained by attaching to each element `a` in `m` a proof that `a` belongs to `m` is equal to the cardinality of `m` itself. In other words, it specifies that the process of attaching proofs to the elements of a multiset does not affect its cardinality.
More concisely: The cardinality of a multiset and the multiset obtained by attaching proofs of membership to each element are equal.
|
Multiset.count_map_eq_count
theorem Multiset.count_map_eq_count :
∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → β) (s : Multiset α),
Set.InjOn f {x | x ∈ s} → ∀ x ∈ s, Multiset.count (f x) (Multiset.map f s) = Multiset.count x s
The theorem `Multiset.count_map_eq_count` states that for any types `α` and `β`, and any function `f` from `α` to `β`, if `f` is injective when restricted to the set of elements contained in a multiset `s` of type `α`, then for every element `x` in `s`, the multiplicity of `f(x)` in the multiset obtained by mapping `f` over `s` is equal to the multiplicity of `x` in `s`. Here the multiplicity of an element in a multiset refers to the number of times the element appears in the multiset. This theorem basically asserts that if a function is injective on a multiset, then applying the function does not change the multiplicity of the elements.
More concisely: If `f: α → β` is injective on the multiset `s` of type `α`, then for each `x` in `s`, the multiplicity of `f(x)` in the image multiset equals the multiplicity of `x` in `s`.
|
Multiset.card_cons
theorem Multiset.card_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α), Multiset.card (a ::ₘ s) = Multiset.card s + 1
The theorem `Multiset.card_cons` states that for any type `α`, any element `a` of type `α`, and any multiset `s` of type `α`, the cardinality (or size) of the multiset resulting from consing `a` onto `s` (`a ::ₘ s`) equals the cardinality of `s` plus one. This mirrors the behavior of adding an element to a list where the length of the list increases by one.
More concisely: For any type α and multiset s of α, the cardinality of the multiset obtained by adding an element a to s is one greater than the cardinality of s.
|
Multiset.map_pmap
theorem Multiset.map_pmap :
∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (s : Multiset α)
(H : ∀ a ∈ s, p a), Multiset.map g (Multiset.pmap f s H) = Multiset.pmap (fun a h => g (f a h)) s H
The theorem `Multiset.map_pmap` states that for any types `α`, `β`, and `γ`, and any property `p` from `α` to `Prop`, if we have a function `g` from `β` to `γ` and a partial function `f` from `α` where `p` applies to `β`, then for any multiset `s` of type `α` where `p` holds for all members of `s`, the map of `g` over the `pmap` of `f` over `s` (with respect to `p`) is equal to the `pmap` of the function that applies `g` after `f` over `s` (with respect to `p`). Essentially, this theorem establishes that the `map` and `pmap` operations on multisets commute under certain conditions.
More concisely: For any types α, β, γ, property p from α to Prop, function g from β to γ, and partial function f from α to β where p applies to the image of f, if s is a multiset of α where p holds for all members, then the map of g over the pmap of f on s equals the pmap of the function composing f and g on s.
|
Multiset.rel_eq
theorem Multiset.rel_eq : ∀ {α : Type u_1} {s t : Multiset α}, Multiset.Rel (fun x x_1 => x = x_1) s t ↔ s = t := by
sorry
This theorem states that for any type `α` and any two multisets `s` and `t` of type `α`, the relation `Multiset.Rel (fun x x_1 => x = x_1) s t` holds if and only if `s` and `t` are equal. In other words, the `Multiset.Rel` equivalence relation, which compares elements of two multisets based on simple equality of their elements, is equivalent to the equality of the multisets themselves.
More concisely: For any type `α` and multisets `s` and `t` of type `α`, `Multiset.Rel (fun x x_1 => x = x_1) s t` if and only if `s` equals `t`.
|
Multiset.subset_of_le
theorem Multiset.subset_of_le : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → s ⊆ t
This theorem states that for any type `α` and for any two multisets `s` and `t` of this type, if `s` is less than or equal to `t` (denoted as `s ≤ t`), then `s` is a subset of `t` (denoted as `s ⊆ t`). In the context of multisets, "less than or equal to" means that `s` can be obtained from `t` by deleting some elements. Hence, the theorem is asserting that if a multiset `s` can be formed by deleting some elements from another multiset `t`, then all elements of `s` are also in `t`.
More concisely: If two multisets of the same type are related by `s ≤ t` (i.e., `s` can be obtained from `t` by deleting some elements), then `s` is a subset of `t` (denoted as `s ⊆ t`).
|
Multiset.cons_inter_of_pos
theorem Multiset.cons_inter_of_pos :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α},
a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a
This theorem, `Multiset.cons_inter_of_pos`, states that for any type `α` with a decidable equality relation, any element `a` of this type, and any two multisets `s` and `t` of this type, if `a` is a member of multiset `t`, then the intersection of multiset `t` with the multiset formed by adding `a` to `s` (`a ::ₘ s`) is equal to the intersection of `s` with `t` after erasing `a` from `t`. In other words, when `a` is in `t`, adding `a` to `s` and then intersecting with `t` is the same as intersecting `s` with `t` after `a` has been removed from `t`.
More concisely: If `α` has decidable equality, `a` is in multiset `t`, then intersecting `a ::ₘ s` with `t` equals intersecting `s` with the multiset obtained by removing `a` from `t`.
|
Multiset.cons_zero
theorem Multiset.cons_zero : ∀ {α : Type u_1} (a : α), a ::ₘ 0 = {a}
This theorem states that for any type `α` and an instance `a` of that type, when `a` is prepended to an empty multiset (`0`), the resulting multiset is a singleton multiset containing only `a`. In other words, `a ::ₘ 0` is equivalent to `{a}`. Here, `::ₘ` represents the operation of adding an element to a multiset in the Lean 4 theorem prover.
More concisely: For any type `α` and element `a` of type `α`, appending `a` to the empty multiset is equivalent to creating a singleton multiset containing `a`. In Lean 4 notation, `a ::ₘ 0` is equivalent to `{a}`.
|
Multiset.mem_coe
theorem Multiset.mem_coe : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ ↑l ↔ a ∈ l
This theorem states that for any type `α`, any element `a` of type `α`, and any list `l` of type `α`, `a` is a member of the multiset corresponding to `l` if and only if `a` is a member of `l`. In other words, an element is in the multiset created from a list if and only if it is in the original list. The ↑ operator is used in Lean to denote the coercion of a list into a multiset.
More concisely: For any type `α` and list `l` of elements `α`, the multiset `↑l` contains an element `a` if and only if `a` is in `l`.
|
Multiset.count_sub
theorem Multiset.count_sub :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α),
Multiset.count a (s - t) = Multiset.count a s - Multiset.count a t
The theorem `Multiset.count_sub` states that for any given type `α` that has decidable equality, and any elements `a` of type `α` and multisets `s` and `t` of type `α`, the multiplicity of `a` in the difference of `s` and `t` (i.e., `s - t`) is equal to the difference of the multiplicity of `a` in `s` and the multiplicity of `a` in `t`. Here, a multiset is a finite set that allows duplicates, and the multiplicity of an element in a multiset is the count of how many times it appears in the set. The difference of two multisets is a multiset that contains every element of the first multiset that is not also an element of the second multiset.
More concisely: For any type `α` with decidable equality, the multiplicity of an element `a` in the difference of multisets `s` and `t` equals the multiplicity of `a` in `s` minus the multiplicity of `a` in `t`.
|
Multiset.card_singleton
theorem Multiset.card_singleton : ∀ {α : Type u_1} (a : α), Multiset.card {a} = 1
The theorem `Multiset.card_singleton` states that for any type `α` and any element `a` of that type, the cardinality (or size) of the multiset consisting of just that element `{a}` is 1. In other words, a multiset containing only one element has a cardinality of 1, regardless of the type or value of the element.
More concisely: For any type `α` and element `a` of type `α`, the multiset `{a}` has cardinality 1.
|
Multiset.count_le_of_le
theorem Multiset.count_le_of_le :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) {s t : Multiset α},
s ≤ t → Multiset.count a s ≤ Multiset.count a t
The theorem `Multiset.count_le_of_le` asserts that for any type `α` with a decidable equality and for any element `a` of type `α` and any two multisets `s` and `t` of type `α`, if `s` is a sub-multiset of `t` (i.e., `s ≤ t`), then the count of the element `a` in the multiset `s` is less than or equal to the count of the element `a` in the multiset `t`. In other words, the multiplicity of an element in a multiset cannot exceed the multiplicity of the same element in a super-multiset of that multiset.
More concisely: For any type `α` with decidable equality and for any element `a` of type `α` and multisets `s` and `t` of type `α` with `s ≤ t`, the count of `a` in `s` is less than or equal to the count of `a` in `t`.
|
Multiset.erase_of_not_mem
theorem Multiset.erase_of_not_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∉ s → s.erase a = s
This theorem states that for any type `α` with decidable equality, for any element `a` of `α`, and for any multiset `s` of elements of `α`, if `a` is not a member of `s`, then erasing `a` from `s` leaves `s` unchanged. In simpler terms, removing an element that doesn't exist in a multiset doesn't change the multiset.
More concisely: For any type `α` with decidable equality, and for any multiset `s` of elements from `α` and element `a` not in `s`, the multiset `s` is equal to the multiset obtained by erasing `a` from `s`.
|
Mathlib.Data.Multiset.Basic._auxLemma.48
theorem Mathlib.Data.Multiset.Basic._auxLemma.48 :
∀ {α : Type u_1} {a : α} {s t : Multiset α}, (a ∈ s + t) = (a ∈ s ∨ a ∈ t)
This theorem states that for any type `α`, any element `a` of type `α`, and any two multisets `s` and `t` of type `α`, the element `a` is in the multiset formed by adding `s` and `t` if and only if `a` is in `s` or `a` is in `t`. In other words, membership in the union of two multisets is equivalent to membership in at least one of the original multisets.
More concisely: For any type `α`, any element `a` of type `α`, and any multisets `s` and `t` of type `α`, `a` is in the multiset formed by `s ∪ t` if and only if `a` is in `s` or `a` is in `t`.
|
Multiset.eq_replicate_of_mem
theorem Multiset.eq_replicate_of_mem :
∀ {α : Type u_1} {a : α} {s : Multiset α}, (∀ b ∈ s, b = a) → s = Multiset.replicate (Multiset.card s) a
This theorem, referred to as an alias of the reverse direction of `Multiset.eq_replicate_card`, establishes that for any given type `α`, element `a` of type `α`, and multiset `s` of type `α`, if each element `b` in multiset `s` equals `a`, then multiset `s` is equivalent to the multiset generated by replicating `a` a number of times equal to the cardinality of `s`. In other words, if all elements in a multiset are the same, then the multiset can be recreated by replicating that particular element as often as the size of the multiset.
More concisely: If all elements in a multiset are equal to `a`, then the multiset is equal to the multiset of `a` repeated `card s` times.
|
Multiset.inter_le_left
theorem Multiset.inter_le_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ∩ t ≤ s
This theorem states that for any type `α` with decidable equality (denoted as `DecidableEq α`), and for any two multisets, `s` and `t`, of this type `α`, the intersection of `s` and `t` (denoted as `s ∩ t`) is always a sub-multiset of `s` (denoted as `s ∩ t ≤ s`). Here, a multiset is a generalization of a set that allows multiple instances of the set's elements. The `≤` operator is used to denote the sub-multiset relation, meaning that all elements of `s ∩ t` are also elements of `s`, potentially with fewer repetitions.
More concisely: For any type `α` with decidable equality and for any multisets `s` and `t` of type `α`, the intersection of `s` and `t` is a sub-multiset of `s`. (Or more mathematically, `s ∩ t ≤ s`.)
|
Multiset.filter_cons_of_neg
theorem Multiset.filter_cons_of_neg :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α),
¬p a → Multiset.filter p (a ::ₘ s) = Multiset.filter p s
The theorem `Multiset.filter_cons_of_neg` states that for any type `α`, any decidable predicate `p` on `α`, any element `a` of type `α`, and any multiset `s` of elements of type `α`, if `a` does not satisfy the predicate `p`, then the multiset obtained by filtering `p` on the multiset formed by adding `a` to `s` is identical to the multiset obtained by just filtering `p` on `s`. In simpler words, if an element doesn't satisfy the predicate, adding it to the multiset doesn't change the result of the filter operation.
More concisely: For any type `α`, decidable predicate `p` on `α`, element `a` of type `α`, and multiset `s` of elements of type `α`, if `a` does not satisfy `p`, then adding `a` to `s` does not affect the multiset obtained by filtering `p` on `s`. In other words, `Multiset.filter p (s : set α) = Multiset.filter p (a :: s)` whenever `p a` is false.
|
Multiset.eq_zero_of_subset_zero
theorem Multiset.eq_zero_of_subset_zero : ∀ {α : Type u_1} {s : Multiset α}, s ⊆ 0 → s = 0
This theorem states that for any type `α` and any multiset `s` of type `α`, if `s` is a subset of the empty multiset (denoted by `0`), then `s` must be equal to the empty multiset. In other words, the only subset of the empty multiset is the empty multiset itself.
More concisely: A multiset `s` of type `α` is equal to the empty multiset `0` if and only if `s` is a subset of `0`.
|
Multiset.count_map_eq_count'
theorem Multiset.count_map_eq_count' :
∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → β) (s : Multiset α),
Function.Injective f → ∀ (x : α), Multiset.count (f x) (Multiset.map f s) = Multiset.count x s
The theorem `Multiset.count_map_eq_count'` states that for any types `α` and `β` with decidable equality and any function `f` from `α` to `β`, if `f` is injective (meaning that different inputs produce different outputs), then the count of `f(x)` in the multiset obtained by mapping `f` over `s` is equal to the count of `x` in the original multiset `s`. In simpler words, an injective function preserves the count of elements when mapping over a multiset.
More concisely: If `f: α → β` is an injective function between types `α` and `β` with decidable equality, then for any multiset `s` over `α`, the count of `f(x)` in the image multiset of `s` under `f` equals the count of `x` in `s`.
|
Multiset.card_le_card
theorem Multiset.card_le_card : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → Multiset.card s ≤ Multiset.card t := by
sorry
The theorem `Multiset.card_le_card` states that for any two multisets `s` and `t` of any type `α`, if `s` is a sub-multiset of `t` (denoted by `s ≤ t`), then the cardinality of `s` (the sum of the multiplicities of all its elements or simply the length of the underlying list) is less than or equal to the cardinality of `t` (denoted by `Multiset.card s ≤ Multiset.card t`).
More concisely: If `s` is a sub-multiset of `t`, then the cardinality of `s` is less than or equal to the cardinality of `t`.
|
Mathlib.Data.Multiset.Basic._auxLemma.86
theorem Mathlib.Data.Multiset.Basic._auxLemma.86 :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {a : α}, (Multiset.count a s = 0) = (a ∉ s)
This theorem, named `Mathlib.Data.Multiset.Basic._auxLemma.86`, states that for any type `α` that has a decidable equality, and any element `a` of type `α` and any multiset `s` of type `α`, the count of `a` in `s` is zero if and only if `a` does not belong to `s`. In other words, an element `a` is not a member of a multiset `s` if its count in `s` is zero. The theorem employs a characteristic feature of multisets, which are essentially sets that allow duplicate elements. The count function is used to determine the multiplicity of an element in a multiset.
More concisely: For any type `α` with decidable equality and any multiset `s` of type `α`, the element `a` is not in `s` if and only if the count of `a` in `s` is zero.
|
Multiset.mem_cons_of_mem
theorem Multiset.mem_cons_of_mem : ∀ {α : Type u_1} {a b : α} {s : Multiset α}, a ∈ s → a ∈ b ::ₘ s
This theorem asserts that for any type `α`, and any elements `a` and `b` of type `α`, and any multiset `s` of type `α`, if `a` is an element of `s`, then `a` is also an element of the multiset formed by prepending `b` to `s`. In other words, adding an element to a multiset does not remove any existing elements.
More concisely: For any type `α`, any element `a` in `α`, and any multiset `s` of type `α`, if `a` is an element of `s`, then `a` is an element of the multiset obtained by adding any element `b` to `s`.
|
Multiset.mem_of_le
theorem Multiset.mem_of_le : ∀ {α : Type u_1} {s t : Multiset α} {a : α}, s ≤ t → a ∈ s → a ∈ t
This theorem states that for any type `α`, and any two multisets `s` and `t` of that type, and any element `a` of that type, if `s` is contained within or equal to `t` (denoted by `s ≤ t`), and `a` is an element of `s` (denoted by `a ∈ s`), then `a` must also be an element of `t` (denoted by `a ∈ t`). In other words, any element of a subset of a multiset is also an element of the multiset itself.
More concisely: If `s` is a multiset of type `α` and `a` is an element of `s` with `s ≤ t`, then `a` is an element of `t`.
|
Multiset.map_const'
theorem Multiset.map_const' :
∀ {α : Type u_1} {β : Type v} (s : Multiset α) (b : β),
Multiset.map (fun x => b) s = Multiset.replicate (Multiset.card s) b
This theorem states that for any multiset `s` of type `α` and any value `b` of type `β`, the result of mapping the function `(fun x => b)` over `s` is equivalent to a multiset that only contains the value `b` with the multiplicity equal to the cardinality (number of elements) of `s`. In mathematical terms, the theorem states that applying a constant function to each element of a multiset yields a new multiset where all elements are that constant and the number of times the constant appears is equal to the size of the initial multiset.
More concisely: For any multiset `s` of type `α` and any value `b` of type `β`, the function `(map s fun x => b)` is a multiset of size equal to the cardinality of `s` consisting only of the value `b`.
|
Multiset.map_le_map
theorem Multiset.map_le_map :
∀ {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α}, s ≤ t → Multiset.map f s ≤ Multiset.map f t := by
sorry
The theorem `Multiset.map_le_map` asserts that for any two multisets `s` and `t` of an arbitrary type `α`, and a function `f` from `α` to another arbitrary type `β`, if `s` is a sub-multiset of `t`, then the multiset obtained by mapping `f` over `s` is also a sub-multiset of the multiset obtained by mapping `f` over `t`. In mathematical terms, if $s$ and $t$ are multisets from a set $A$ and $f: A \rightarrow B$ is a function, then $s \subseteq t$ implies that $f(s) \subseteq f(t)$. The multiplicity of an element in a multiset is preserved during this mapping operation.
More concisely: If `s` is a sub-multiset of `t` in type `α` and `f` is a function from `α` to `β`, then `f(s)` is a sub-multiset of `f(t)`.
|
Multiset.mem_pmap
theorem Multiset.mem_pmap :
∀ {α : Type u_1} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : ∀ a ∈ s, p a} {b : β},
b ∈ Multiset.pmap f s H ↔ ∃ a, ∃ (h : a ∈ s), f a ⋯ = b
The theorem `Multiset.mem_pmap` states that for any types `α` and `β`, a property `p` on `α`, a function `f` from `α` (satisfying property `p`) to `β`, a multiset `s` consisting of elements of type `α` (where all elements satisfy `p`), and any element `b` of type `β`, the element `b` is in the multiset obtained by applying the partially mapped function `f` to multiset `s` if and only if there exists an element `a` in `s` such that applying the function `f` to `a` (and the proof of `a` satisfying `p`) gives `b`. In other words, an element is in the output of the partial map operation on a multiset if and only if it is the image of an element of the initial multiset under the function in the partial map operation.
More concisely: For any types `α`, `β`, property `p` on `α`, function `f : α →β` satisfying `p`, multiset `s` of `α` elements satisfying `p`, and `β` element `b`, `b` is in the multiset obtained by applying `f` to `s` if and only if there exists an `α` element `a` in `s` with `f(a) = b` and `p(a)` holds.
|
Multiset.union_le
theorem Multiset.union_le : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s ≤ u → t ≤ u → s ∪ t ≤ u
This theorem states that for any type `α` with decidable equality, and any three multisets `s`, `t`, and `u` of type `α`, if `s` and `t` are both subsets of `u` (represented by `s ≤ u` and `t ≤ u`), then the union of `s` and `t` (represented by `s ∪ t`) is also a subset of `u`. In other words, this theorem asserts the property that the union of two subsets of a multiset is still a subset of the original multiset.
More concisely: For any type `α` with decidable equality, if `s`, `t` are multisets of type `α` with `s ≤ u` and `t ≤ u`, then `s ∪ t ≤ u`. (The union of two subsets of a multiset is a subset of the multiset.)
|
Mathlib.Data.Multiset.Basic._auxLemma.14
theorem Mathlib.Data.Multiset.Basic._auxLemma.14 : ∀ {α : Type u_1} {a b : α}, (b ∈ {a}) = (b = a)
This theorem states that for any type `α` and any two elements `a` and `b` of this type, `b` is an element of the single-element multiset `{a}` if and only if `b` is equal to `a`. This is basically saying that the only way for an element to be in a single-element multiset is for it to be equal to that single element.
More concisely: For any type `α` and any elements `a, b : α`, `b` is an element of the single-element multiset `{a}` if and only if `a = b`.
|
Multiset.map_cons
theorem Multiset.map_cons :
∀ {α : Type u_1} {β : Type v} (f : α → β) (a : α) (s : Multiset α),
Multiset.map f (a ::ₘ s) = f a ::ₘ Multiset.map f s
The theorem `Multiset.map_cons` states that for all types `α` and `β`, for any function `f` from `α` to `β`, for any element `a` of type `α`, and for any multiset `s` of type `α`, mapping function `f` over a multiset that has `a` consed to `s` (`a ::ₘ s`) is the same as consing the function `f` applied to `a` to the multiset obtained by mapping `f` over `s` (i.e., `f a ::ₘ Multiset.map f s`). In other words, it asserts that the `map` operation distributes over the `cons` operation for multisets. This is an analogue to the familiar property in list theory where mapping a function over a list that has an element consed to it is equivalent to consing the function applied to the element to the mapped list.
More concisely: For all types `α` and `β`, and functions `f` from `α` to `β`, the operation of mapping `f` over a multiset `s` and consing `f(a)` to the result is equivalent to consing `a` to the multiset obtained by mapping `f` over `s`. In symbols, `(∀αβ (f : α → β) (a : α) (s : MultiSet α), f a ::ₘ (Multiset.map f s) ≡ a ::ₘ (Multiset.map f (s : MultiSet α)))`.
|
Multiset.zero_inter
theorem Multiset.zero_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), 0 ∩ s = 0
This theorem states that for any type `α` with decidable equality and for any multiset `s` of type `α`, the intersection of the empty multiset (notated as `0`) and `s` is always the empty multiset. Essentially, it's stating that when you intersect any collection with an empty collection, the result is always an empty collection.
More concisely: For any type `α` with decidable equality, the intersection of an empty multiset `s` of type `α` with any multiset `s'` is the empty multiset.
|
Multiset.coe_eq_coe
theorem Multiset.coe_eq_coe : ∀ {α : Type u_1} {l₁ l₂ : List α}, ↑l₁ = ↑l₂ ↔ l₁.Perm l₂
This theorem states that for any two lists `l₁` and `l₂` of any type `α`, the multisets obtained from `l₁` and `l₂` are equal if and only if `l₁` and `l₂` are permutations of each other. In other words, two lists generate the same multiset exactly when they contain the same elements, possibly in different orders.
More concisely: For any lists `l₁` and `l₂` of type `α`, `multiset l₁ = multiset l₂` if and only if `l₁` is a permutation of `l₂`.
|
Multiset.coe_card
theorem Multiset.coe_card : ∀ {α : Type u_1} (l : List α), Multiset.card ↑l = l.length
The theorem `Multiset.coe_card` states that for any given list `l` of any type `α`, the cardinality of the multiset obtained by converting this list into a multiset (`↑l`) is equal to the length of the original list `l`. This effectively means that the operation of converting a list to a multiset does not change the number of elements in the collection, considering each repetition in the list as a distinct element in the multiset.
More concisely: The cardinality of the multiset obtained from a list is equal to the length of the list.
|
Multiset.mem_map_of_mem
theorem Multiset.mem_map_of_mem :
∀ {α : Type u_1} {β : Type v} (f : α → β) {a : α} {s : Multiset α}, a ∈ s → f a ∈ Multiset.map f s
The theorem `Multiset.mem_map_of_mem` states that for any types `α` and `β`, a function `f` from `α` to `β`, and a multiset `s` of type `α`, if an element `a` of type `α` is in the multiset `s`, then the result of applying the function `f` to `a` is in the multiset obtained by applying `f` to each element of `s`. In other words, if an element is in the original multiset, its transformed version through the function `f` will be in the transformed multiset.
More concisely: If `a` is an element of multiset `s` over type `α`, then the image `f(a)` is in the multiset `map f s` over type `β`.
|
Multiset.cons_le_cons
theorem Multiset.cons_le_cons : ∀ {α : Type u_1} {s t : Multiset α} (a : α), s ≤ t → a ::ₘ s ≤ a ::ₘ t
The theorem `Multiset.cons_le_cons` states that for any type `α`, and for any multiset `s` and `t` of that type, and for any element `a` of type `α`, if `s` is less than or equal to `t`, then the multiset formed by adding `a` to `s` (denoted as `a ::ₘ s`) is less than or equal to the multiset formed by adding `a` to `t` (denoted as `a ::ₘ t`). This theorem is about the order preservation of the `cons` operation in the context of multisets.
More concisely: For any type `α` and multisets `s` and `t` of type `α`, if `s ≤ t`, then `a ::ₘ s ≤ a ::ₘ t` for all `a` of type `α`.
|
Multiset.mem_toList
theorem Multiset.mem_toList : ∀ {α : Type u_1} {a : α} {s : Multiset α}, a ∈ s.toList ↔ a ∈ s
This theorem states that for any type `α`, any element `a` of type `α`, and any multiset `s` of type `α`, the element `a` is a member of the list obtained by converting the multiset `s` to a list if and only if `a` is a member of the multiset `s`. In other words, the membership of an element in the multiset is preserved when the multiset is converted to a list.
More concisely: For any type `α`, any element `a` in multiset `s` of type `α`, `a` is an element of the list obtained from `s` if and only if `a` is an element of `s`.
|
Multiset.eq_zero_of_forall_not_mem
theorem Multiset.eq_zero_of_forall_not_mem : ∀ {α : Type u_1} {s : Multiset α}, (∀ (x : α), x ∉ s) → s = 0
This theorem states that for any type `α` and any multiset `s` of type `α`, if it holds for every element `x` of type `α` that `x` is not a member of the multiset `s`, then the multiset `s` must be the empty multiset. In other words, if no elements of the given type are in the multiset, the multiset is empty.
More concisely: If a multiset of type `α` contains no elements of type `α`, then it is the empty multiset.
|
Multiset.induction_on
theorem Multiset.induction_on :
∀ {α : Type u_1} {p : Multiset α → Prop} (s : Multiset α),
p 0 → (∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)) → p s
This theorem, `Multiset.induction_on`, provides an induction principle for multisets in Lean 4. Given any type `α`, a predicate `p` on multisets of `α`, and a multiset `s` of `α`, it states that if the predicate holds for the empty multiset (denoted by `0`), and if for any element `a` of type `α` and any multiset `s`, the predicate holding for `s` implies that the predicate holds for the multiset obtained by adding `a` to `s` (denoted by `a ::ₘ s`), then the predicate `p` holds for the multiset `s`. Essentially, this theorem allows us to prove a property about all multisets by showing it for the empty multiset and showing that if it holds for a particular multiset, then it also holds when an element is added to that multiset.
More concisely: If a predicate `p` on multisets of type `α` holds for the empty multiset and is closed under adding elements, then it holds for any given multiset of type `α`.
|
Multiset.Le.subset
theorem Multiset.Le.subset : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → s ⊆ t
This theorem, denoted as `Multiset.Le.subset`, states that for any type `α` and for any two multisets `s` and `t` of this type `α`, if the multiset `s` is less than or equal to the multiset `t` (i.e., `s ≤ t`), then `s` is a subset of `t` (i.e., `s ⊆ t`). This theorem acts as an alias of the theorem `Multiset.subset_of_le` in Lean 4. In terms of mathematics, it expresses the fact that partial order (≤) implies subset relation (⊆) for multisets.
More concisely: If `s` is less than or equal to `t` in the multiset ordering, then `s` is a subset of `t`. (i.e., `s ≤ t` implies `s ⊆ t`)
|
Multiset.coe_add
theorem Multiset.coe_add : ∀ {α : Type u_1} (s t : List α), ↑s + ↑t = ↑(s ++ t)
This theorem states that for any two lists `s` and `t` of a certain type `α`, the multiset union of the multisets corresponding to `s` and `t` is equal to the multiset corresponding to the concatenation of `s` and `t`. In other words, converting each list to a multiset and then taking their union is the same as concatenating the lists first and then converting the result to a multiset.
More concisely: For any lists `s` and `t` of type `α`, the multiset union of the multisets from `s` and `t` equals the multiset of the concatenation of `s` and `t`.
|
Multiset.coe_toList
theorem Multiset.coe_toList : ∀ {α : Type u_1} (s : Multiset α), ↑s.toList = s
This theorem states that for any type `α` and any multiset `s` of type `α`, when you convert `s` to a list using the `Multiset.toList` function and then convert it back to a multiset (`↑` is the Lean notation for this conversion), you get the original multiset `s` back. In other words, the process of converting a multiset to a list and back again is lossless; no information about the multiset is lost in this process.
More concisely: For any type `α` and multiset `s` of type `α`, the conversion from `s` to the list obtained by `Multiset.toList s` and back to a multiset using the lift operation (`↑`) results in the original multiset: `Multiset.toList ↑s = ↑(Multiset.toList s)`.
|
Multiset.zero_le
theorem Multiset.zero_le : ∀ {α : Type u_1} (s : Multiset α), 0 ≤ s
The theorem `Multiset.zero_le` states that for all multiset `s` of any type `α`, the empty multiset `0` is less than or equal to `s`. In other words, this theorem asserts that any multiset, may it be empty or not, is always greater than or equal to the empty multiset.
More concisely: For all multisets `s` of type `α`, the empty multiset `0` is less than or equal to `s`. (In mathematical notation: `0 ≤ s` for all multisets `s`.)
|
Multiset.erase_cons_head
theorem Multiset.erase_cons_head :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), (a ::ₘ s).erase a = s
The theorem `Multiset.erase_cons_head` states that for any type `α` with a decidable equality and any multiset `s` of type `α`, if an element `a` of type `α` is added to the front of the multiset `s` to form a new multiset, then removing `a` from this new multiset will return the original multiset `s`. This means that the `Multiset.erase` function will remove the first occurrence of an element from the multiset.
More concisely: For any type `α` with decidable equality and any multiset `s` of type `α`, adding an element `a` to `s` and then erasing `a` results in `s`.
|
Multiset.quot_mk_to_coe
theorem Multiset.quot_mk_to_coe : ∀ {α : Type u_1} (l : List α), ⟦l⟧ = ↑l
This theorem is stating that for any list `l` of an arbitrary type `α`, the multiset that `l` is embedded into (denoted by ⟦l⟧) is equivalent to the coe of `l`, where coe is a coercion function that converts the list into a multiset. Essentially, this theorem is asserting that any list can be viewed as a multiset and vice versa.
More concisely: For any list `l` of type `α`, the multiset ⟦l⟧ is equivalent to the coerced multiset of `l`.
|