English
The pi construction on the Multiset underlying l corresponds to the Multiset of the dependent product pi l fs.
Русский
Операция π над мультисетой, соответствующей списку l, эквивалентна мультисетe зависимого произведения π l fs.
LaTeX
$$$(l : \text{Multiset } ι).pi (fs ·) = (↑(\pi l fs) : \text{Multiset } (∀ i ∈ l, α i))$$$
Lean4
theorem _root_.Multiset.pi_coe (l : List ι) (fs : ∀ i, List (α i)) :
(l : Multiset ι).pi (fs ·) = (↑(pi l fs) : Multiset (∀ i ∈ l, α i)) := by
induction l with
| nil =>
simp only [Multiset.coe_nil, Multiset.pi_zero, pi_nil, Multiset.coe_singleton, Multiset.singleton_inj]
ext i hi
simp at hi
| cons i l ih => simp [ih, Multiset.coe_bind, ← Multiset.cons_coe]
