Documentation

Mathlib.Data.Multiset.Powerset

The powerset of a multiset #

powerset #

def Multiset.powersetAux {α : Type u_1} (l : List α) :

A helper function for the powerset of a multiset. Given a list l, returns a list of sublists of l as multisets.

Equations
Instances For
    theorem Multiset.powersetAux_eq_map_coe {α : Type u_1} {l : List α} :
    Multiset.powersetAux l = List.map Multiset.ofList l.sublists
    @[simp]
    theorem Multiset.mem_powersetAux {α : Type u_1} {l : List α} {s : Multiset α} :
    def Multiset.powersetAux' {α : Type u_1} (l : List α) :

    Helper function for the powerset of a multiset. Given a list l, returns a list of sublists of l (using sublists'), as multisets.

    Equations
    Instances For
      @[simp]
      theorem Multiset.powerset_aux'_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
      theorem Multiset.powersetAux_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
      def Multiset.powerset {α : Type u_1} (s : Multiset α) :

      The power set of a multiset.

      Equations
      Instances For
        theorem Multiset.powerset_coe {α : Type u_1} (l : List α) :
        (↑l).powerset = (List.map Multiset.ofList l.sublists)
        @[simp]
        theorem Multiset.powerset_coe' {α : Type u_1} (l : List α) :
        (↑l).powerset = (List.map Multiset.ofList l.sublists')
        @[simp]
        @[simp]
        theorem Multiset.powerset_cons {α : Type u_1} (a : α) (s : Multiset α) :
        (a ::ₘ s).powerset = s.powerset + Multiset.map (Multiset.cons a) s.powerset
        @[simp]
        theorem Multiset.mem_powerset {α : Type u_1} {s : Multiset α} {t : Multiset α} :
        s t.powerset s t
        theorem Multiset.map_single_le_powerset {α : Type u_1} (s : Multiset α) :
        Multiset.map singleton s s.powerset
        @[simp]
        theorem Multiset.card_powerset {α : Type u_1} (s : Multiset α) :
        Multiset.card s.powerset = 2 ^ Multiset.card s
        theorem Multiset.revzip_powersetAux {α : Type u_1} {l : List α} ⦃x : Multiset α × Multiset α (h : x (Multiset.powersetAux l).revzip) :
        x.1 + x.2 = l
        theorem Multiset.revzip_powersetAux' {α : Type u_1} {l : List α} ⦃x : Multiset α × Multiset α (h : x (Multiset.powersetAux' l).revzip) :
        x.1 + x.2 = l
        theorem Multiset.revzip_powersetAux_lemma {α : Type u_2} [DecidableEq α] (l : List α) {l' : List (Multiset α)} (H : ∀ ⦃x : Multiset α × Multiset α⦄, x l'.revzipx.1 + x.2 = l) :
        l'.revzip = List.map (fun (x : Multiset α) => (x, l - x)) l'
        theorem Multiset.revzip_powersetAux_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
        (Multiset.powersetAux l₁).revzip.Perm (Multiset.powersetAux l₂).revzip

        powersetCard #

        def Multiset.powersetCardAux {α : Type u_1} (n : ) (l : List α) :

        Helper function for powersetCard. Given a list l, powersetCardAux n l is the list of sublists of length n, as multisets.

        Equations
        Instances For
          theorem Multiset.powersetCardAux_eq_map_coe {α : Type u_1} {n : } {l : List α} :
          @[simp]
          theorem Multiset.mem_powersetCardAux {α : Type u_1} {n : } {l : List α} {s : Multiset α} :
          s Multiset.powersetCardAux n l s l Multiset.card s = n
          @[simp]
          @[simp]
          theorem Multiset.powersetCardAux_nil {α : Type u_1} (n : ) :
          theorem Multiset.powersetCardAux_perm {α : Type u_1} {n : } {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
          def Multiset.powersetCard {α : Type u_1} (n : ) (s : Multiset α) :

          powersetCard n s is the multiset of all submultisets of s of length n.

          Equations
          Instances For
            theorem Multiset.powersetCard_coe {α : Type u_1} (n : ) (l : List α) :
            Multiset.powersetCard n l = (List.map Multiset.ofList (List.sublistsLen n l))
            @[simp]
            @[simp]
            theorem Multiset.mem_powersetCard {α : Type u_1} {n : } {s : Multiset α} {t : Multiset α} :
            s Multiset.powersetCard n t s t Multiset.card s = n
            @[simp]
            theorem Multiset.card_powersetCard {α : Type u_1} (n : ) (s : Multiset α) :
            Multiset.card (Multiset.powersetCard n s) = (Multiset.card s).choose n
            theorem Multiset.powersetCard_le_powerset {α : Type u_1} (n : ) (s : Multiset α) :
            Multiset.powersetCard n s s.powerset
            theorem Multiset.powersetCard_mono {α : Type u_1} (n : ) {s : Multiset α} {t : Multiset α} (h : s t) :
            @[simp]
            theorem Multiset.powersetCard_eq_empty {α : Type u_2} (n : ) {s : Multiset α} (h : Multiset.card s < n) :
            @[simp]
            theorem Multiset.powersetCard_card_add {α : Type u_1} (s : Multiset α) {i : } (hi : 0 < i) :
            Multiset.powersetCard (Multiset.card s + i) s = 0
            theorem Multiset.powersetCard_map {α : Type u_1} {β : Type u_2} (f : αβ) (n : ) (s : Multiset α) :
            theorem Multiset.bind_powerset_len {α : Type u_2} (S : Multiset α) :
            ((Multiset.range (Multiset.card S + 1)).bind fun (k : ) => Multiset.powersetCard k S) = S.powerset
            @[simp]
            theorem Multiset.nodup_powerset {α : Type u_1} {s : Multiset α} :
            s.powerset.Nodup s.Nodup
            theorem Multiset.Nodup.powerset {α : Type u_1} {s : Multiset α} :
            s.Nodups.powerset.Nodup

            Alias of the reverse direction of Multiset.nodup_powerset.

            theorem Multiset.Nodup.ofPowerset {α : Type u_1} {s : Multiset α} :
            s.powerset.Nodups.Nodup

            Alias of the forward direction of Multiset.nodup_powerset.

            theorem Multiset.Nodup.powersetCard {α : Type u_1} {n : } {s : Multiset α} (h : s.Nodup) :