Theorems · Theorem · combinatorics

Multiset.powersetCardAux_cons

∀ {α : Type u_1} (n : ℕ) (a : α) (l : List α),
  Multiset.powersetCardAux (n + 1) (a :: l) =
    Multiset.powersetCardAux (n + 1) l ++ List.map (Multiset.cons a) (Multiset.powersetCardAux n l)

Defined in

Mathlib.Data.Multiset.Powerset

Cited by

2 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Quot.sound