Mathlib.Data.Multiset.Powerset._auxLemma.4
theorem Mathlib.Data.Multiset.Powerset._auxLemma.4 : ∀ {α : Type u_1} {s t : Multiset α}, (s ∈ t.powerset) = (s ≤ t)
This theorem states that for all types `α` and multisets `s` and `t` of type `α`, `s` is in the power set of `t` if and only if `s` is a subset of `t`. In other words, a multiset `s` is included in the power set of another multiset `t` exactly when every element of `s` is also an element of `t`. This is a common property of power sets in set theory, extended here to multisets, which are like sets but allow duplicate elements.
More concisely: A multiset is a subset of another multiset if and only if it is an element of that multiset's power set.
|
Multiset.powersetCard_coe
theorem Multiset.powersetCard_coe :
∀ {α : Type u_1} (n : ℕ) (l : List α),
Multiset.powersetCard n ↑l = ↑(List.map Multiset.ofList (List.sublistsLen n l))
The theorem `Multiset.powersetCard_coe` states that for any type `α`, any natural number `n`, and any list `l` of elements of type `α`, the multiset of all submultisets of the multiset formed from `l` that have length `n` is equal to the multiset formed from mapping the function `Multiset.ofList` (which converts lists to multisets) over the list of all sublists of `l` of length `n`. In essence, it relates the powerset of a multiset of a fixed size to the sublists of the corresponding list.
More concisely: For any type `α` and natural number `n`, the multiset of submultisets of size `n` from a multiset formed by `α` values is equal to the multiset of multisets obtained by applying `Multiset.ofList` to all sublists of length `n` from any list representing that multiset.
|
Multiset.mem_powersetCard
theorem Multiset.mem_powersetCard :
∀ {α : Type u_1} {n : ℕ} {s t : Multiset α}, s ∈ Multiset.powersetCard n t ↔ s ≤ t ∧ Multiset.card s = n
The theorem `Multiset.mem_powersetCard` states that for any type `α`, natural number `n`, and multisets `s` and `t` of type `α`, a multiset `s` is a member of the powerset of `t` of cardinality `n` if and only if `s` is a sub-multiset of `t` and the cardinality of `s` equals `n`. In simpler terms, it tells us that a set `s` is in the collection of all subsets of `t` of size `n` only when `s` is indeed a subset of `t` and the size of `s` is `n`. It essentially characterizes the membership in the `n`-sized powerset of a multiset.
More concisely: A multiset is an element of the powerset of another multiset with a specific cardinality if and only if it is a sub-multiset of that set and has the given cardinality.
|
Multiset.revzip_powersetAux_lemma
theorem Multiset.revzip_powersetAux_lemma :
∀ {α : Type u_2} [inst : DecidableEq α] (l : List α) {l' : List (Multiset α)},
(∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l) →
l'.revzip = List.map (fun x => (x, ↑l - x)) l'
This theorem states that for any type `α` with a decidable equality and given a list `l` of type `α` and a list `l'` of multisets of `α`, if every pair `(x1, x2)` in the reverse zip of `l'` satisfies that the sum of `x1` and `x2` is equal to the multiset representation of `l`, then the reverse zip of `l'` is equal to the mapping of `l'` where each element `x` is mapped to a pair `(x, ↑l - x)`. In other words, it relates the operations of reverse-zipping and mapping on the list `l'` under the condition that the sum of the elements of each pair in the reverse zip equals to the original list `l` converted to a multiset.
More concisely: If `l` is a list with decidable equality and `l'` is a list of multisets of `α` such that for all pairs `(x1, x2)` in the reverse zip of `l'`, we have `x1 + x2 = multiset.to_set l`, then the reverse zip of `l'` is equal to the mapping of `l'` where each `x` is mapped to `(x, l - x)`.
|
Multiset.powersetCardAux_eq_map_coe
theorem Multiset.powersetCardAux_eq_map_coe :
∀ {α : Type u_1} {n : ℕ} {l : List α},
Multiset.powersetCardAux n l = List.map Multiset.ofList (List.sublistsLen n l)
The theorem `Multiset.powersetCardAux_eq_map_coe` states that for any given type `α`, natural number `n`, and list `l` of type `α`, the function `Multiset.powersetCardAux n l` which returns a list of all sublists of `l` of length `n` as multisets, is equal to applying the function `Multiset.ofList` to each element of the list returned by `List.sublistsLen n l`, which is the list of all sublists of `l` of length `n`. In other words, it shows the equivalence between generating multisets from sublists of a certain length and converting such sublists into multisets.
More concisely: For any type `α` and natural number `n`, the multiset of all sublists of length `n` from a list `l` of type `α` is equal to the multiset obtained by applying `Multiset.ofList` to each sublist in `List.sublistsLen n l`.
|
Multiset.revzip_powersetAux
theorem Multiset.revzip_powersetAux :
∀ {α : Type u_1} {l : List α} ⦃x : Multiset α × Multiset α⦄, x ∈ (Multiset.powersetAux l).revzip → x.1 + x.2 = ↑l
The theorem `Multiset.revzip_powersetAux` states that for any type `α`, any list `l` of that type, and any pair of multisets `x`, if `x` is an element of the list obtained by applying the function `List.revzip` to the powerset of `l`, then the sum of the two multisets in the pair `x` is equal to the multiset associated with the list `l`. In simpler terms, it states that each pair of subsets in the reverse-zipped powerset of a list sums up to the original list when considered as multisets, allowing for reordering and repetition of elements.
More concisely: For any type `α` and list `l` of length `n` over `α`, if multisets `x` and `y` are paired in the reverse-zipped powerset of `l`, then `x ⊎ y = ∫i=0
|
Multiset.Nodup.powerset
theorem Multiset.Nodup.powerset : ∀ {α : Type u_1} {s : Multiset α}, s.Nodup → s.powerset.Nodup
The theorem `Multiset.Nodup.powerset` states that for any type `α` and for any multiset `s` of type `α`, if the multiset `s` does not contain any duplicate elements, then the powerset of `s` also does not contain any duplicate elements. Here, a powerset of a multiset is the set of all possible subsets of the multiset, and the `Nodup` property ensures that a multiset or a powerset does not contain any repeat elements.
More concisely: If `s` is a multiset of type `α` without duplicates, then the powerset of `s` also does not contain any duplicate elements.
|
Multiset.map_single_le_powerset
theorem Multiset.map_single_le_powerset : ∀ {α : Type u_1} (s : Multiset α), Multiset.map singleton s ≤ s.powerset := by
sorry
This theorem states that for any given multiset `s` of an arbitrary type `α`, the multiset obtained by applying the function `singleton` to each element of `s` (which is equivalent to mapping each element of `s` to a singleton set containing only that element) is a subset (or is less than or equal) to the power set of `s`. This means that every singleton set created from each element of the original multiset `s` is indeed a member of the power set of `s`.
More concisely: For any multiset `s` of type `α`, the multiset of singletons formed by applying `singleton` to each element of `s` is a subset of the power set of `s`.
|
Multiset.powerset_coe'
theorem Multiset.powerset_coe' :
∀ {α : Type u_1} (l : List α), (↑l).powerset = ↑(List.map Multiset.ofList l.sublists')
This theorem states that, for any type `α` and list of that type, the powerset of the multiset created from that list is equal to the multiset created from mapping the function `Multiset.ofList` (which converts a list to a multiset) over all the sublists of the original list. The sublists are generated in a specific order where the first element of the list is treated as the most significant bit (MSB). This theorem essentially defines the relationship between the powerset of a multiset and the sublists of the original list.
More concisely: For any type `α`, the powerset of the multiset obtained from a list of `α` using `Multiset.ofList` is equal to the multiset obtained from mapping `Multiset.ofList` over all sublists of that list treated as binary sequences with the first element as the most significant bit.
|
Mathlib.Data.Multiset.Powerset._auxLemma.16
theorem Mathlib.Data.Multiset.Powerset._auxLemma.16 : ∀ {α : Type u_1} {l : List α}, (↑l).Nodup = l.Nodup
This theorem, `Mathlib.Data.Multiset.Powerset._auxLemma.16`, states that for every type `α` and for any list `l` of type `α`, the property of having no duplicates in the list's multiset representation (`Multiset.Nodup ↑l`) is the same as the property of the list itself having no duplicates (`List.Nodup l`). In other words, a list has no duplicate elements if and only if its corresponding multiset also has no duplicate elements.
More concisely: For any type `α` and list `l` of type `α`, the multiset representation of `l` having no duplicates if and only if `l` itself has no duplicates. In Lean notation: `(Multiset.Nodup ↑l) ↔ List.Nodup l`.
|
Multiset.Nodup.ofPowerset
theorem Multiset.Nodup.ofPowerset : ∀ {α : Type u_1} {s : Multiset α}, s.powerset.Nodup → s.Nodup
This theorem, which is an alias of the forward direction of `Multiset.nodup_powerset`, states that for any type `α` and any multiset `s` of type `α`, if the powerset of `s` has no duplicate elements (denoted by `s.powerset.Nodup`), then the multiset `s` itself also has no duplicate elements (denoted by `s.Nodup`). In other words, the property of having no duplicate elements is preserved when going from a powerset to the set itself.
More concisely: If a multiset's power set has no duplicate elements, then the original multiset also has no duplicate elements.
|
Multiset.powersetAux_eq_map_coe
theorem Multiset.powersetAux_eq_map_coe :
∀ {α : Type u_1} {l : List α}, Multiset.powersetAux l = List.map Multiset.ofList l.sublists
The theorem `Multiset.powersetAux_eq_map_coe` states that for all types `α` and for all lists `l` of type `α`, the function `Multiset.powersetAux`, when applied to `l`, is equivalent to mapping the function `Multiset.ofList` over all the sublists of `l`. This means that the powerset of a multiset, generated by `Multiset.powersetAux`, can be generated by taking all the sublists of the original list and converting each sublist into a multiset.
More concisely: For all types α and lists l of α, the function Multiset.powersetAux(l) is equivalent to mapping Multiset.ofList over all sublists of l, i.e., Multiset.powersetAux(l) = {Multiset.ofList(s) : s ⊆ l}.
|
Multiset.powersetAux_perm_powersetAux'
theorem Multiset.powersetAux_perm_powersetAux' :
∀ {α : Type u_1} {l : List α}, (Multiset.powersetAux l).Perm (Multiset.powersetAux' l)
The theorem `Multiset.powersetAux_perm_powersetAux'` asserts that for any type `α` and any list `l` of elements of type `α`, the list of multisets derived from the sublists of `l` by function `Multiset.powersetAux` is a permutation of the list of multisets derived by function `Multiset.powersetAux'`. In other words, both functions `Multiset.powersetAux` and `Multiset.powersetAux'` generate the same set of sub-multisets, possibly in different orders.
More concisely: The multisets derived from sublists of a list `α` using `Multiset.powersetAux` and `Multiset.powersetAux'` are permutations of each other.
|