Module docstring
{"# Sections of a multiset "}
Multiset.Sections
definition
(s : Multiset (Multiset α)) : Multiset (Multiset α)
Full source
/-- The sections of a multiset of multisets `s` consists of all those multisets
which can be put in bijection with `s`, so each element is a member of the corresponding multiset.
-/
def Sections (s : Multiset (Multiset α)) : Multiset (Multiset α) :=
Multiset.recOn s {0} (fun s _ c => s.bind fun a => c.map (Multiset.cons a)) fun a₀ a₁ _ pi => by
simp [map_bind, bind_bind a₀ a₁, cons_swap]Informal description
Given a multiset $s$ of multisets over a type $\alpha$, the sections of $s$ consist of all multisets that can be put in bijection with $s$ such that each element belongs to the corresponding multiset in $s$. More precisely, for each multiset $m$ in $s$, the section contains an element from $m$.
The sections are constructed recursively:
- The sections of the empty multiset $\{0\}$ is the multiset containing only the empty multiset $\{0\}$.
- For a multiset $s$ with an additional multiset $m$ (i.e., $m ::ₘ s$), the sections are obtained by taking each element $a$ from $m$ and prepending it to each section of $s$.
Multiset.sections_zero
theorem
: Sections (0 : Multiset (Multiset α)) = {0}
Informal description
The sections of the empty multiset of multisets is the multiset containing only the empty multiset, i.e., $\text{Sections}(0) = \{0\}$.
Multiset.sections_cons
theorem
(s : Multiset (Multiset α)) (m : Multiset α) : Sections (m ::ₘ s) = m.bind fun a => (Sections s).map (Multiset.cons a)
Full source
@[simp]
theorem sections_cons (s : Multiset (Multiset α)) (m : Multiset α) :
Sections (m ::ₘ s) = m.bind fun a => (Sections s).map (Multiset.cons a) :=
recOn_cons m sInformal description
Given a multiset $s$ of multisets over a type $\alpha$ and another multiset $m$ over $\alpha$, the sections of the multiset obtained by adding $m$ to $s$ (denoted $m ::ₘ s$) are equal to the union over all elements $a$ in $m$ of the sections of $s$ with $a$ prepended to each section.
More formally, we have:
\[ \text{Sections}(m ::ₘ s) = \bigcup_{a \in m} \{ a ::ₘ t \mid t \in \text{Sections}(s) \} \]
where $a ::ₘ t$ denotes the multiset obtained by adding one occurrence of $a$ to $t$.
Multiset.coe_sections
theorem
:
∀ l : List (List α),
Sections (l.map fun l : List α => (l : Multiset α) : Multiset (Multiset α)) =
(l.sections.map fun l : List α => (l : Multiset α) : Multiset (Multiset α))
Full source
theorem coe_sections :
∀ l : List (List α),
Sections (l.map fun l : List α => (l : Multiset α) : Multiset (Multiset α)) =
(l.sections.map fun l : List α => (l : Multiset α) : Multiset (Multiset α))
| [] => rfl
| a :: l => by
simp only [List.map_cons, List.sections]
rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l]
simp [List.sections, Function.comp_def, List.flatMap]Informal description
For any list of lists $l$ over a type $\alpha$, the sections of the multiset obtained by converting each list in $l$ to a multiset are equal to the multiset obtained by converting each section of $l$ to a multiset.
In symbols:
\[ \text{Sections}\left(\left\{ l_i : \text{Multiset} \alpha \mid l_i \in l \right\}\right) = \left\{ t : \text{Multiset} \alpha \mid t \in l.\text{sections} \right\} \]
where $l.\text{sections}$ denotes the list of all possible sections of $l$ (i.e., lists formed by taking one element from each sublist of $l$).
Multiset.sections_add
theorem
(s t : Multiset (Multiset α)) : Sections (s + t) = (Sections s).bind fun m => (Sections t).map (m + ·)
Full source
@[simp]
theorem sections_add (s t : Multiset (Multiset α)) :
Sections (s + t) = (Sections s).bind fun m => (Sections t).map (m + ·) :=
Multiset.induction_on s (by simp) fun a s ih => by
simp [ih, bind_assoc, map_bind, bind_map]Informal description
For any two multisets $s$ and $t$ of multisets over a type $\alpha$, the sections of their sum $s + t$ are given by the union over all sections $m$ of $s$ of the sections of $t$ with $m$ added to each section.
More formally:
\[ \text{Sections}(s + t) = \bigcup_{m \in \text{Sections}(s)} \{ m + t' \mid t' \in \text{Sections}(t) \} \]
where $m + t'$ denotes the multiset sum of $m$ and $t'$.
Multiset.mem_sections
theorem
{s : Multiset (Multiset α)} : ∀ {a}, a ∈ Sections s ↔ s.Rel (fun s a => a ∈ s) a
Full source
theorem mem_sections {s : Multiset (Multiset α)} :
∀ {a}, a ∈ Sections sa ∈ Sections s ↔ s.Rel (fun s a => a ∈ s) a := by
induction s using Multiset.induction_on with
| empty => simp
| cons _ _ ih => simp [ih, rel_cons_left, eq_comm]Informal description
For any multiset $s$ of multisets over a type $\alpha$ and any multiset $a$, $a$ is a section of $s$ if and only if there exists a relation between $s$ and $a$ such that for every pair of corresponding elements $(m, b) \in s \times a$, the element $b$ belongs to the multiset $m$. In other words, $a \in \text{Sections}(s)$ if and only if $\text{Rel} (\lambda m b, b \in m) s a$.
Multiset.card_sections
theorem
{s : Multiset (Multiset α)} : card (Sections s) = prod (s.map card)
Full source
theorem card_sections {s : Multiset (Multiset α)} : card (Sections s) = prod (s.map card) :=
Multiset.induction_on s (by simp) (by simp +contextual)Informal description
For any multiset $s$ of multisets over a type $\alpha$, the cardinality of the sections of $s$ is equal to the product of the cardinalities of the multisets in $s$. That is,
\[ |\text{Sections}(s)| = \prod_{m \in s} |m|. \]