Theorems · Theorem · combinatorics

Multiset.pi_cons

∀ {α : Type u_1} [inst : DecidableEq α] {β : α → Type u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)) (a : α),
  (a ::ₘ m).pi t = (t a).bind fun b => Multiset.map (Multiset.Pi.cons m a b) (m.pi t)

Defined in

Mathlib.Data.Multiset.Pi

Cited by

5 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq