Documentation

Mathlib.Data.Multiset.Basic

Multisets #

These are implemented as the quotient of a list by permutations.

Notation #

We define the global infix notation ::ₘ for Multiset.cons.

def Multiset (α : Type u) :

Multiset α is the quotient of List α by list permutation. The result is a type of finite sets with duplicates allowed.

Equations
Instances For
    def Multiset.ofList {α : Type u_1} :
    List αMultiset α

    The quotient map from List α to Multiset α.

    Equations
    Instances For
      instance Multiset.instCoeListMultiset {α : Type u_1} :
      Coe (List α) (Multiset α)
      Equations
      • Multiset.instCoeListMultiset = { coe := Multiset.ofList }
      @[simp]
      theorem Multiset.quot_mk_to_coe {α : Type u_1} (l : List α) :
      l = l
      @[simp]
      theorem Multiset.quot_mk_to_coe' {α : Type u_1} (l : List α) :
      Quot.mk (fun (x x_1 : List α) => x x_1) l = l
      @[simp]
      theorem Multiset.quot_mk_to_coe'' {α : Type u_1} (l : List α) :
      Quot.mk Setoid.r l = l
      @[simp]
      theorem Multiset.coe_eq_coe {α : Type u_1} {l₁ : List α} {l₂ : List α} :
      l₁ = l₂ List.Perm l₁ l₂
      Equations
      def Multiset.sizeOf {α : Type u_1} [SizeOf α] (s : Multiset α) :

      defines a size for a multiset by referring to the size of the underlying list

      Equations
      Instances For
        instance Multiset.instSizeOfMultiset {α : Type u_1} [SizeOf α] :
        Equations
        • Multiset.instSizeOfMultiset = { sizeOf := Multiset.sizeOf }

        Empty multiset #

        def Multiset.zero {α : Type u_1} :

        0 : Multiset α is the empty set

        Equations
        • Multiset.zero = []
        Instances For
          instance Multiset.instZeroMultiset {α : Type u_1} :
          Equations
          • Multiset.instZeroMultiset = { zero := Multiset.zero }
          Equations
          • Multiset.instEmptyCollectionMultiset = { emptyCollection := 0 }
          Equations
          • Multiset.inhabitedMultiset = { default := 0 }
          instance Multiset.instUniqueMultiset {α : Type u_1} [IsEmpty α] :
          Equations
          • Multiset.instUniqueMultiset = { toInhabited := { default := 0 }, uniq := }
          @[simp]
          theorem Multiset.coe_nil {α : Type u_1} :
          [] = 0
          @[simp]
          theorem Multiset.empty_eq_zero {α : Type u_1} :
          = 0
          @[simp]
          theorem Multiset.coe_eq_zero {α : Type u_1} (l : List α) :
          l = 0 l = []
          theorem Multiset.coe_eq_zero_iff_isEmpty {α : Type u_1} (l : List α) :

          Multiset.cons #

          def Multiset.cons {α : Type u_1} (a : α) (s : Multiset α) :

          cons a s is the multiset which contains s plus one more instance of a.

          Equations
          Instances For

            cons a s is the multiset which contains s plus one more instance of a.

            Equations
            Instances For
              instance Multiset.instInsertMultiset {α : Type u_1} :
              Equations
              • Multiset.instInsertMultiset = { insert := Multiset.cons }
              @[simp]
              theorem Multiset.insert_eq_cons {α : Type u_1} (a : α) (s : Multiset α) :
              insert a s = a ::ₘ s
              @[simp]
              theorem Multiset.cons_coe {α : Type u_1} (a : α) (l : List α) :
              a ::ₘ l = (a :: l)
              @[simp]
              theorem Multiset.cons_inj_left {α : Type u_1} {a : α} {b : α} (s : Multiset α) :
              a ::ₘ s = b ::ₘ s a = b
              @[simp]
              theorem Multiset.cons_inj_right {α : Type u_1} (a : α) {s : Multiset α} {t : Multiset α} :
              a ::ₘ s = a ::ₘ t s = t
              theorem Multiset.induction {α : Type u_1} {p : Multiset αProp} (empty : p 0) (cons : ∀ ⦃a : α⦄ {s : Multiset α}, p sp (a ::ₘ s)) (s : Multiset α) :
              p s
              theorem Multiset.induction_on {α : Type u_1} {p : Multiset αProp} (s : Multiset α) (empty : p 0) (cons : ∀ ⦃a : α⦄ {s : Multiset α}, p sp (a ::ₘ s)) :
              p s
              theorem Multiset.cons_swap {α : Type u_1} (a : α) (b : α) (s : Multiset α) :
              a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s
              def Multiset.rec {α : Type u_1} {C : Multiset αSort u_3} (C_0 : C 0) (C_cons : (a : α) → (m : Multiset α) → C mC (a ::ₘ m)) (C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))) (m : Multiset α) :
              C m

              Dependent recursor on multisets. TODO: should be @[recursor 6], but then the definition of Multiset.pi fails with a stack overflow in whnf.

              Equations
              Instances For
                def Multiset.recOn {α : Type u_1} {C : Multiset αSort u_3} (m : Multiset α) (C_0 : C 0) (C_cons : (a : α) → (m : Multiset α) → C mC (a ::ₘ m)) (C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))) :
                C m

                Companion to Multiset.rec with more convenient argument order.

                Equations
                Instances For
                  @[simp]
                  theorem Multiset.recOn_0 {α : Type u_1} {C : Multiset αSort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C mC (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))} :
                  Multiset.recOn 0 C_0 C_cons C_cons_heq = C_0
                  @[simp]
                  theorem Multiset.recOn_cons {α : Type u_1} {C : Multiset αSort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C mC (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))} (a : α) (m : Multiset α) :
                  Multiset.recOn (a ::ₘ m) C_0 C_cons C_cons_heq = C_cons a m (Multiset.recOn m C_0 C_cons C_cons_heq)
                  def Multiset.Mem {α : Type u_1} (a : α) (s : Multiset α) :

                  a ∈ s means that a has nonzero multiplicity in s.

                  Equations
                  Instances For
                    Equations
                    • Multiset.instMembershipMultiset = { mem := Multiset.Mem }
                    @[simp]
                    theorem Multiset.mem_coe {α : Type u_1} {a : α} {l : List α} :
                    a l a l
                    instance Multiset.decidableMem {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
                    Equations
                    @[simp]
                    theorem Multiset.mem_cons {α : Type u_1} {a : α} {b : α} {s : Multiset α} :
                    a b ::ₘ s a = b a s
                    theorem Multiset.mem_cons_of_mem {α : Type u_1} {a : α} {b : α} {s : Multiset α} (h : a s) :
                    a b ::ₘ s
                    theorem Multiset.mem_cons_self {α : Type u_1} (a : α) (s : Multiset α) :
                    a a ::ₘ s
                    theorem Multiset.forall_mem_cons {α : Type u_1} {p : αProp} {a : α} {s : Multiset α} :
                    (xa ::ₘ s, p x) p a xs, p x
                    theorem Multiset.exists_cons_of_mem {α : Type u_1} {s : Multiset α} {a : α} :
                    a s∃ (t : Multiset α), s = a ::ₘ t
                    @[simp]
                    theorem Multiset.not_mem_zero {α : Type u_1} (a : α) :
                    a0
                    theorem Multiset.eq_zero_of_forall_not_mem {α : Type u_1} {s : Multiset α} :
                    (∀ (x : α), xs)s = 0
                    theorem Multiset.eq_zero_iff_forall_not_mem {α : Type u_1} {s : Multiset α} :
                    s = 0 ∀ (a : α), as
                    theorem Multiset.exists_mem_of_ne_zero {α : Type u_1} {s : Multiset α} :
                    s 0∃ (a : α), a s
                    theorem Multiset.empty_or_exists_mem {α : Type u_1} (s : Multiset α) :
                    s = 0 ∃ (a : α), a s
                    @[simp]
                    theorem Multiset.zero_ne_cons {α : Type u_1} {a : α} {m : Multiset α} :
                    0 a ::ₘ m
                    @[simp]
                    theorem Multiset.cons_ne_zero {α : Type u_1} {a : α} {m : Multiset α} :
                    a ::ₘ m 0
                    theorem Multiset.cons_eq_cons {α : Type u_1} {a : α} {b : α} {as : Multiset α} {bs : Multiset α} :
                    a ::ₘ as = b ::ₘ bs a = b as = bs a b ∃ (cs : Multiset α), as = b ::ₘ cs bs = a ::ₘ cs

                    Singleton #

                    Equations
                    • Multiset.instSingletonMultiset = { singleton := fun (a : α) => a ::ₘ 0 }
                    @[simp]
                    theorem Multiset.cons_zero {α : Type u_1} (a : α) :
                    a ::ₘ 0 = {a}
                    @[simp]
                    theorem Multiset.coe_singleton {α : Type u_1} (a : α) :
                    [a] = {a}
                    @[simp]
                    theorem Multiset.mem_singleton {α : Type u_1} {a : α} {b : α} :
                    b {a} b = a
                    theorem Multiset.mem_singleton_self {α : Type u_1} (a : α) :
                    a {a}
                    @[simp]
                    theorem Multiset.singleton_inj {α : Type u_1} {a : α} {b : α} :
                    {a} = {b} a = b
                    @[simp]
                    theorem Multiset.coe_eq_singleton {α : Type u_1} {l : List α} {a : α} :
                    l = {a} l = [a]
                    @[simp]
                    theorem Multiset.singleton_eq_cons_iff {α : Type u_1} {a : α} {b : α} (m : Multiset α) :
                    {a} = b ::ₘ m a = b m = 0
                    theorem Multiset.pair_comm {α : Type u_1} (x : α) (y : α) :
                    {x, y} = {y, x}

                    Multiset.Subset #

                    def Multiset.Subset {α : Type u_1} (s : Multiset α) (t : Multiset α) :

                    s ⊆ t is the lift of the list subset relation. It means that any element with nonzero multiplicity in s has nonzero multiplicity in t, but it does not imply that the multiplicity of a in s is less or equal than in t; see s ≤ t for this relation.

                    Equations
                    Instances For
                      Equations
                      • Multiset.instHasSubsetMultiset = { Subset := Multiset.Subset }
                      Equations
                      instance Multiset.instIsNonstrictStrictOrder {α : Type u_1} :
                      IsNonstrictStrictOrder (Multiset α) (fun (x x_1 : Multiset α) => x x_1) fun (x x_1 : Multiset α) => x x_1
                      Equations
                      • =
                      @[simp]
                      theorem Multiset.coe_subset {α : Type u_1} {l₁ : List α} {l₂ : List α} :
                      l₁ l₂ l₁ l₂
                      @[simp]
                      theorem Multiset.Subset.refl {α : Type u_1} (s : Multiset α) :
                      s s
                      theorem Multiset.Subset.trans {α : Type u_1} {s : Multiset α} {t : Multiset α} {u : Multiset α} :
                      s tt us u
                      theorem Multiset.subset_iff {α : Type u_1} {s : Multiset α} {t : Multiset α} :
                      s t ∀ ⦃x : α⦄, x sx t
                      theorem Multiset.mem_of_subset {α : Type u_1} {s : Multiset α} {t : Multiset α} {a : α} (h : s t) :
                      a sa t
                      @[simp]
                      theorem Multiset.zero_subset {α : Type u_1} (s : Multiset α) :
                      0 s
                      theorem Multiset.subset_cons {α : Type u_1} (s : Multiset α) (a : α) :
                      s a ::ₘ s
                      theorem Multiset.ssubset_cons {α : Type u_1} {s : Multiset α} {a : α} (ha : as) :
                      s a ::ₘ s
                      @[simp]
                      theorem Multiset.cons_subset {α : Type u_1} {a : α} {s : Multiset α} {t : Multiset α} :
                      a ::ₘ s t a t s t
                      theorem Multiset.cons_subset_cons {α : Type u_1} {a : α} {s : Multiset α} {t : Multiset α} :
                      s ta ::ₘ s a ::ₘ t
                      theorem Multiset.eq_zero_of_subset_zero {α : Type u_1} {s : Multiset α} (h : s 0) :
                      s = 0
                      @[simp]
                      theorem Multiset.subset_zero {α : Type u_1} {s : Multiset α} :
                      s 0 s = 0
                      @[simp]
                      theorem Multiset.zero_ssubset {α : Type u_1} {s : Multiset α} :
                      0 s s 0
                      @[simp]
                      theorem Multiset.singleton_subset {α : Type u_1} {s : Multiset α} {a : α} :
                      {a} s a s
                      theorem Multiset.induction_on' {α : Type u_1} {p : Multiset αProp} (S : Multiset α) (h₁ : p 0) (h₂ : ∀ {a : α} {s : Multiset α}, a Ss Sp sp (insert a s)) :
                      p S

                      Multiset.toList #

                      noncomputable def Multiset.toList {α : Type u_1} (s : Multiset α) :
                      List α

                      Produces a list of the elements in the multiset using choice.

                      Equations
                      Instances For
                        @[simp]
                        theorem Multiset.coe_toList {α : Type u_1} (s : Multiset α) :
                        @[simp]
                        theorem Multiset.toList_eq_nil {α : Type u_1} {s : Multiset α} :
                        @[simp]
                        @[simp]
                        theorem Multiset.toList_zero {α : Type u_1} :
                        @[simp]
                        theorem Multiset.mem_toList {α : Type u_1} {a : α} {s : Multiset α} :
                        @[simp]
                        theorem Multiset.toList_eq_singleton_iff {α : Type u_1} {a : α} {m : Multiset α} :
                        Multiset.toList m = [a] m = {a}
                        @[simp]
                        theorem Multiset.toList_singleton {α : Type u_1} (a : α) :

                        Partial order on Multisets #

                        def Multiset.Le {α : Type u_1} (s : Multiset α) (t : Multiset α) :

                        s ≤ t means that s is a sublist of t (up to permutation). Equivalently, s ≤ t means that count a s ≤ count a t for all a.

                        Equations
                        Instances For
                          Equations
                          instance Multiset.decidableLE {α : Type u_1} [DecidableEq α] :
                          DecidableRel fun (x x_1 : Multiset α) => x x_1
                          Equations
                          theorem Multiset.subset_of_le {α : Type u_1} {s : Multiset α} {t : Multiset α} :
                          s ts t
                          theorem Multiset.Le.subset {α : Type u_1} {s : Multiset α} {t : Multiset α} :
                          s ts t

                          Alias of Multiset.subset_of_le.

                          theorem Multiset.mem_of_le {α : Type u_1} {s : Multiset α} {t : Multiset α} {a : α} (h : s t) :
                          a sa t
                          theorem Multiset.not_mem_mono {α : Type u_1} {s : Multiset α} {t : Multiset α} {a : α} (h : s t) :
                          atas
                          @[simp]
                          theorem Multiset.coe_le {α : Type u_1} {l₁ : List α} {l₂ : List α} :
                          l₁ l₂ List.Subperm l₁ l₂
                          theorem Multiset.leInductionOn {α : Type u_1} {C : Multiset αMultiset αProp} {s : Multiset α} {t : Multiset α} (h : s t) (H : ∀ {l₁ l₂ : List α}, List.Sublist l₁ l₂C l₁ l₂) :
                          C s t
                          theorem Multiset.zero_le {α : Type u_1} (s : Multiset α) :
                          0 s
                          Equations
                          • Multiset.instOrderBotMultisetToLEToPreorderInstPartialOrderMultiset = OrderBot.mk
                          @[simp]
                          theorem Multiset.bot_eq_zero {α : Type u_1} :
                          = 0

                          This is a rfl and simp version of bot_eq_zero.

                          theorem Multiset.le_zero {α : Type u_1} {s : Multiset α} :
                          s 0 s = 0
                          theorem Multiset.lt_cons_self {α : Type u_1} (s : Multiset α) (a : α) :
                          s < a ::ₘ s
                          theorem Multiset.le_cons_self {α : Type u_1} (s : Multiset α) (a : α) :
                          s a ::ₘ s
                          theorem Multiset.cons_le_cons_iff {α : Type u_1} {s : Multiset α} {t : Multiset α} (a : α) :
                          a ::ₘ s a ::ₘ t s t
                          theorem Multiset.cons_le_cons {α : Type u_1} {s : Multiset α} {t : Multiset α} (a : α) :
                          s ta ::ₘ s a ::ₘ t
                          @[simp]
                          theorem Multiset.cons_lt_cons_iff {α : Type u_1} {s : Multiset α} {t : Multiset α} {a : α} :
                          a ::ₘ s < a ::ₘ t s < t
                          theorem Multiset.cons_lt_cons {α : Type u_1} {s : Multiset α} {t : Multiset α} (a : α) (h : s < t) :
                          a ::ₘ s < a ::ₘ t
                          theorem Multiset.le_cons_of_not_mem {α : Type u_1} {s : Multiset α} {t : Multiset α} {a : α} (m : as) :
                          s a ::ₘ t s t
                          @[simp]
                          theorem Multiset.singleton_ne_zero {α : Type u_1} (a : α) :
                          {a} 0
                          @[simp]
                          theorem Multiset.singleton_le {α : Type u_1} {a : α} {s : Multiset α} :
                          {a} s a s
                          @[simp]
                          theorem Multiset.le_singleton {α : Type u_1} {s : Multiset α} {a : α} :
                          s {a} s = 0 s = {a}
                          @[simp]
                          theorem Multiset.lt_singleton {α : Type u_1} {s : Multiset α} {a : α} :
                          s < {a} s = 0
                          @[simp]
                          theorem Multiset.ssubset_singleton_iff {α : Type u_1} {s : Multiset α} {a : α} :
                          s {a} s = 0

                          Additive monoid #

                          def Multiset.add {α : Type u_1} (s₁ : Multiset α) (s₂ : Multiset α) :

                          The sum of two multisets is the lift of the list append operation. This adds the multiplicities of each element, i.e. count a (s + t) = count a s + count a t.

                          Equations
                          Instances For
                            instance Multiset.instAddMultiset {α : Type u_1} :
                            Equations
                            • Multiset.instAddMultiset = { add := Multiset.add }
                            @[simp]
                            theorem Multiset.coe_add {α : Type u_1} (s : List α) (t : List α) :
                            s + t = (s ++ t)
                            @[simp]
                            theorem Multiset.singleton_add {α : Type u_1} (a : α) (s : Multiset α) :
                            {a} + s = a ::ₘ s
                            Equations
                            • =
                            Equations
                            theorem Multiset.le_add_right {α : Type u_1} (s : Multiset α) (t : Multiset α) :
                            s s + t
                            theorem Multiset.le_add_left {α : Type u_1} (s : Multiset α) (t : Multiset α) :
                            s t + s
                            theorem Multiset.le_iff_exists_add {α : Type u_1} {s : Multiset α} {t : Multiset α} :
                            s t ∃ (u : Multiset α), t = s + u
                            Equations
                            @[simp]
                            theorem Multiset.cons_add {α : Type u_1} (a : α) (s : Multiset α) (t : Multiset α) :
                            a ::ₘ s + t = a ::ₘ (s + t)
                            @[simp]
                            theorem Multiset.add_cons {α : Type u_1} (a : α) (s : Multiset α) (t : Multiset α) :
                            s + a ::ₘ t = a ::ₘ (s + t)
                            @[simp]
                            theorem Multiset.mem_add {α : Type u_1} {a : α} {s : Multiset α} {t : Multiset α} :
                            a s + t a s a t
                            theorem Multiset.mem_of_mem_nsmul {α : Type u_1} {a : α} {s : Multiset α} {n : } (h : a n s) :
                            a s
                            @[simp]
                            theorem Multiset.mem_nsmul {α : Type u_1} {a : α} {s : Multiset α} {n : } (h0 : n 0) :
                            a n s a s
                            theorem Multiset.nsmul_cons {α : Type u_1} {s : Multiset α} (n : ) (a : α) :
                            n (a ::ₘ s) = n {a} + n s

                            Cardinality #

                            def Multiset.card {α : Type u_1} :

                            The cardinality of a multiset is the sum of the multiplicities of all its elements, or simply the length of the underlying list.

                            Equations
                            • Multiset.card = { toZeroHom := { toFun := fun (s : Multiset α) => Quot.liftOn s List.length , map_zero' := }, map_add' := }
                            Instances For
                              @[simp]
                              theorem Multiset.coe_card {α : Type u_1} (l : List α) :
                              Multiset.card l = List.length l
                              @[simp]
                              theorem Multiset.length_toList {α : Type u_1} (s : Multiset α) :
                              List.length (Multiset.toList s) = Multiset.card s
                              @[simp]
                              theorem Multiset.card_zero {α : Type u_1} :
                              Multiset.card 0 = 0
                              theorem Multiset.card_add {α : Type u_1} (s : Multiset α) (t : Multiset α) :
                              Multiset.card (s + t) = Multiset.card s + Multiset.card t
                              theorem Multiset.card_nsmul {α : Type u_1} (s : Multiset α) (n : ) :
                              Multiset.card (n s) = n * Multiset.card s
                              @[simp]
                              theorem Multiset.card_cons {α : Type u_1} (a : α) (s : Multiset α) :
                              Multiset.card (a ::ₘ s) = Multiset.card s + 1
                              @[simp]
                              theorem Multiset.card_singleton {α : Type u_1} (a : α) :
                              Multiset.card {a} = 1
                              theorem Multiset.card_pair {α : Type u_1} (a : α) (b : α) :
                              Multiset.card {a, b} = 2
                              theorem Multiset.card_eq_one {α : Type u_1} {s : Multiset α} :
                              Multiset.card s = 1 ∃ (a : α), s = {a}
                              theorem Multiset.card_le_card {α : Type u_1} {s : Multiset α} {t : Multiset α} (h : s t) :
                              Multiset.card s Multiset.card t
                              theorem Multiset.card_mono {α : Type u_1} :
                              Monotone Multiset.card
                              theorem Multiset.eq_of_le_of_card_le {α : Type u_1} {s : Multiset α} {t : Multiset α} (h : s t) :
                              Multiset.card t Multiset.card ss = t
                              theorem Multiset.card_lt_card {α : Type u_1} {s : Multiset α} {t : Multiset α} (h : s < t) :
                              Multiset.card s < Multiset.card t
                              theorem Multiset.card_strictMono {α : Type u_1} :
                              StrictMono Multiset.card
                              theorem Multiset.lt_iff_cons_le {α : Type u_1} {s : Multiset α} {t : Multiset α} :
                              s < t ∃ (a : α), a ::ₘ s t
                              @[simp]
                              theorem Multiset.card_eq_zero {α : Type u_1} {s : Multiset α} :
                              Multiset.card s = 0 s = 0
                              theorem Multiset.card_pos {α : Type u_1} {s : Multiset α} :
                              0 < Multiset.card s s 0
                              theorem Multiset.card_pos_iff_exists_mem {α : Type u_1} {s : Multiset α} :
                              0 < Multiset.card s ∃ (a : α), a s
                              theorem Multiset.card_eq_two {α : Type u_1} {s : Multiset α} :
                              Multiset.card s = 2 ∃ (x : α) (y : α), s = {x, y}
                              theorem Multiset.card_eq_three {α : Type u_1} {s : Multiset α} :
                              Multiset.card s = 3 ∃ (x : α) (y : α) (z : α), s = {x, y, z}

                              Induction principles #

                              def Multiset.strongInductionOn {α : Type u_1} {p : Multiset αSort u_3} (s : Multiset α) (ih : (s : Multiset α) → ((t : Multiset α) → t < sp t)p s) :
                              p s

                              The strong induction principle for multisets.

                              Equations
                              Instances For
                                theorem Multiset.strongInductionOn_eq {α : Type u_1} {p : Multiset αSort u_3} (s : Multiset α) (H : (s : Multiset α) → ((t : Multiset α) → t < sp t)p s) :
                                Multiset.strongInductionOn s H = H s fun (t : Multiset α) (_h : t < s) => Multiset.strongInductionOn t H
                                theorem Multiset.case_strongInductionOn {α : Type u_1} {p : Multiset αProp} (s : Multiset α) (h₀ : p 0) (h₁ : ∀ (a : α) (s : Multiset α), (ts, p t)p (a ::ₘ s)) :
                                p s
                                def Multiset.strongDownwardInduction {α : Type u_1} {p : Multiset αSort u_3} {n : } (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → Multiset.card t₂ nt₁ < t₂p t₂)Multiset.card t₁ np t₁) (s : Multiset α) :
                                Multiset.card s np s

                                Suppose that, given that p t can be defined on all supersets of s of cardinality less than n, one knows how to define p s. Then one can inductively define p s for all multisets s of cardinality less than n, starting from multisets of card n and iterating. This can be used either to define data, or to prove properties.

                                Equations
                                Instances For
                                  theorem Multiset.strongDownwardInduction_eq {α : Type u_1} {p : Multiset αSort u_3} {n : } (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → Multiset.card t₂ nt₁ < t₂p t₂)Multiset.card t₁ np t₁) (s : Multiset α) :
                                  Multiset.strongDownwardInduction H s = H s fun {t₂ : Multiset α} (ht : Multiset.card t₂ n) (_hst : s < t₂) => Multiset.strongDownwardInduction H t₂ ht
                                  def Multiset.strongDownwardInductionOn {α : Type u_1} {p : Multiset αSort u_3} {n : } (s : Multiset α) :
                                  ((t₁ : Multiset α) → ({t₂ : Multiset α} → Multiset.card t₂ nt₁ < t₂p t₂)Multiset.card t₁ np t₁)Multiset.card s np s

                                  Analogue of strongDownwardInduction with order of arguments swapped.

                                  Equations
                                  Instances For
                                    theorem Multiset.strongDownwardInductionOn_eq {α : Type u_1} {p : Multiset αSort u_3} (s : Multiset α) {n : } (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → Multiset.card t₂ nt₁ < t₂p t₂)Multiset.card t₁ np t₁) :
                                    (fun (a : Multiset.card s n) => Multiset.strongDownwardInductionOn s H a) = H s fun {t : Multiset α} (ht : Multiset.card t n) (_h : s < t) => Multiset.strongDownwardInductionOn t H ht

                                    Another way of expressing strongInductionOn: the (<) relation is well-founded.

                                    Equations
                                    • =

                                    Multiset.replicate #

                                    def Multiset.replicate {α : Type u_1} (n : ) (a : α) :

                                    replicate n a is the multiset containing only a with multiplicity n.

                                    Equations
                                    Instances For
                                      theorem Multiset.coe_replicate {α : Type u_1} (n : ) (a : α) :
                                      @[simp]
                                      theorem Multiset.replicate_zero {α : Type u_1} (a : α) :
                                      @[simp]
                                      theorem Multiset.replicate_succ {α : Type u_1} (a : α) (n : ) :
                                      theorem Multiset.replicate_add {α : Type u_1} (m : ) (n : ) (a : α) :

                                      Multiset.replicate as an AddMonoidHom.

                                      Equations
                                      Instances For
                                        theorem Multiset.replicate_one {α : Type u_1} (a : α) :
                                        @[simp]
                                        theorem Multiset.card_replicate {α : Type u_1} (n : ) (a : α) :
                                        Multiset.card (Multiset.replicate n a) = n
                                        theorem Multiset.mem_replicate {α : Type u_1} {a : α} {b : α} {n : } :
                                        theorem Multiset.eq_of_mem_replicate {α : Type u_1} {a : α} {b : α} {n : } :
                                        b Multiset.replicate n ab = a
                                        theorem Multiset.eq_replicate_card {α : Type u_1} {a : α} {s : Multiset α} :
                                        s = Multiset.replicate (Multiset.card s) a bs, b = a
                                        theorem Multiset.eq_replicate_of_mem {α : Type u_1} {a : α} {s : Multiset α} :
                                        (bs, b = a)s = Multiset.replicate (Multiset.card s) a

                                        Alias of the reverse direction of Multiset.eq_replicate_card.

                                        theorem Multiset.eq_replicate {α : Type u_1} {a : α} {n : } {s : Multiset α} :
                                        s = Multiset.replicate n a Multiset.card s = n bs, b = a
                                        @[simp]
                                        theorem Multiset.replicate_right_inj {α : Type u_1} {a : α} {b : α} {n : } (h : n 0) :
                                        theorem Multiset.replicate_subset_singleton {α : Type u_1} (n : ) (a : α) :
                                        theorem Multiset.replicate_le_coe {α : Type u_1} {a : α} {n : } {l : List α} :
                                        theorem Multiset.nsmul_replicate {α : Type u_1} {a : α} (n : ) (m : ) :
                                        theorem Multiset.nsmul_singleton {α : Type u_1} (a : α) (n : ) :
                                        theorem Multiset.le_replicate_iff {α : Type u_1} {m : Multiset α} {a : α} {n : } :
                                        m Multiset.replicate n a ∃ k ≤ n, m = Multiset.replicate k a
                                        theorem Multiset.lt_replicate_succ {α : Type u_1} {m : Multiset α} {x : α} {n : } :

                                        Erasing one copy of an element #

                                        def Multiset.erase {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) :

                                        erase s a is the multiset that subtracts 1 from the multiplicity of a.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem Multiset.coe_erase {α : Type u_1} [DecidableEq α] (l : List α) (a : α) :
                                          Multiset.erase (l) a = (List.erase l a)
                                          @[simp]
                                          theorem Multiset.erase_zero {α : Type u_1} [DecidableEq α] (a : α) :
                                          @[simp]
                                          theorem Multiset.erase_cons_head {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
                                          @[simp]
                                          theorem Multiset.erase_cons_tail {α : Type u_1} [DecidableEq α] {a : α} {b : α} (s : Multiset α) (h : b a) :
                                          @[simp]
                                          theorem Multiset.erase_singleton {α : Type u_1} [DecidableEq α] (a : α) :
                                          @[simp]
                                          theorem Multiset.erase_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                          asMultiset.erase s a = s
                                          @[simp]
                                          theorem Multiset.cons_erase {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} :
                                          a sa ::ₘ Multiset.erase s a = s
                                          theorem Multiset.erase_cons_tail_of_mem {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} {b : α} (h : a s) :
                                          theorem Multiset.le_cons_erase {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) :
                                          theorem Multiset.add_singleton_eq_iff {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :
                                          s + {a} = t a t s = Multiset.erase t a
                                          theorem Multiset.erase_add_left_pos {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α) :
                                          a sMultiset.erase (s + t) a = Multiset.erase s a + t
                                          theorem Multiset.erase_add_right_pos {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : a t) :
                                          theorem Multiset.erase_add_right_neg {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α) :
                                          asMultiset.erase (s + t) a = s + Multiset.erase t a
                                          theorem Multiset.erase_add_left_neg {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : at) :
                                          theorem Multiset.erase_le {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
                                          @[simp]
                                          theorem Multiset.erase_lt {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                          theorem Multiset.erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
                                          theorem Multiset.mem_erase_of_ne {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Multiset α} (ab : a b) :
                                          theorem Multiset.mem_of_mem_erase {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Multiset α} :
                                          a Multiset.erase s ba s
                                          theorem Multiset.erase_comm {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) (b : α) :
                                          theorem Multiset.erase_le_erase {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (a : α) (h : s t) :
                                          theorem Multiset.erase_le_iff_le_cons {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :
                                          @[simp]
                                          theorem Multiset.card_erase_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                          a sMultiset.card (Multiset.erase s a) = Nat.pred (Multiset.card s)
                                          @[simp]
                                          theorem Multiset.card_erase_add_one {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                          a sMultiset.card (Multiset.erase s a) + 1 = Multiset.card s
                                          theorem Multiset.card_erase_lt_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                          a sMultiset.card (Multiset.erase s a) < Multiset.card s
                                          theorem Multiset.card_erase_le {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                          Multiset.card (Multiset.erase s a) Multiset.card s
                                          theorem Multiset.card_erase_eq_ite {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                          Multiset.card (Multiset.erase s a) = if a s then Nat.pred (Multiset.card s) else Multiset.card s
                                          @[simp]
                                          theorem Multiset.coe_reverse {α : Type u_1} (l : List α) :
                                          (List.reverse l) = l

                                          Multiset.map #

                                          def Multiset.map {α : Type u_1} {β : Type v} (f : αβ) (s : Multiset α) :

                                          map f s is the lift of the list map operation. The multiplicity of b in map f s is the number of a ∈ s (counting multiplicity) such that f a = b.

                                          Equations
                                          Instances For
                                            theorem Multiset.map_congr {α : Type u_1} {β : Type v} {f : αβ} {g : αβ} {s : Multiset α} {t : Multiset α} :
                                            s = t(xt, f x = g x)Multiset.map f s = Multiset.map g t
                                            theorem Multiset.map_hcongr {α : Type u_1} {β : Type v} {β' : Type v} {m : Multiset α} {f : αβ} {f' : αβ'} (h : β = β') (hf : am, HEq (f a) (f' a)) :
                                            theorem Multiset.forall_mem_map_iff {α : Type u_1} {β : Type v} {f : αβ} {p : βProp} {s : Multiset α} :
                                            (yMultiset.map f s, p y) xs, p (f x)
                                            @[simp]
                                            theorem Multiset.map_coe {α : Type u_1} {β : Type v} (f : αβ) (l : List α) :
                                            Multiset.map f l = (List.map f l)
                                            @[simp]
                                            theorem Multiset.map_zero {α : Type u_1} {β : Type v} (f : αβ) :
                                            @[simp]
                                            theorem Multiset.map_cons {α : Type u_1} {β : Type v} (f : αβ) (a : α) (s : Multiset α) :
                                            theorem Multiset.map_comp_cons {α : Type u_1} {β : Type v} (f : αβ) (t : α) :
                                            @[simp]
                                            theorem Multiset.map_singleton {α : Type u_1} {β : Type v} (f : αβ) (a : α) :
                                            Multiset.map f {a} = {f a}
                                            @[simp]
                                            theorem Multiset.map_replicate {α : Type u_1} {β : Type v} (f : αβ) (k : ) (a : α) :
                                            @[simp]
                                            theorem Multiset.map_add {α : Type u_1} {β : Type v} (f : αβ) (s : Multiset α) (t : Multiset α) :
                                            instance Multiset.canLift {α : Type u_1} {β : Type v} (c : βα) (p : αProp) [CanLift α β c p] :
                                            CanLift (Multiset α) (Multiset β) (Multiset.map c) fun (s : Multiset α) => xs, p x

                                            If each element of s : Multiset α can be lifted to β, then s can be lifted to Multiset β.

                                            Equations
                                            • =
                                            def Multiset.mapAddMonoidHom {α : Type u_1} {β : Type v} (f : αβ) :

                                            Multiset.map as an AddMonoidHom.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem Multiset.coe_mapAddMonoidHom {α : Type u_1} {β : Type v} (f : αβ) :
                                              theorem Multiset.map_nsmul {α : Type u_1} {β : Type v} (f : αβ) (n : ) (s : Multiset α) :
                                              @[simp]
                                              theorem Multiset.mem_map {α : Type u_1} {β : Type v} {f : αβ} {b : β} {s : Multiset α} :
                                              b Multiset.map f s ∃ a ∈ s, f a = b
                                              @[simp]
                                              theorem Multiset.card_map {α : Type u_1} {β : Type v} (f : αβ) (s : Multiset α) :
                                              Multiset.card (Multiset.map f s) = Multiset.card s
                                              @[simp]
                                              theorem Multiset.map_eq_zero {α : Type u_1} {β : Type v} {s : Multiset α} {f : αβ} :
                                              Multiset.map f s = 0 s = 0
                                              theorem Multiset.mem_map_of_mem {α : Type u_1} {β : Type v} (f : αβ) {a : α} {s : Multiset α} (h : a s) :
                                              theorem Multiset.map_eq_singleton {α : Type u_1} {β : Type v} {f : αβ} {s : Multiset α} {b : β} :
                                              Multiset.map f s = {b} ∃ (a : α), s = {a} f a = b
                                              theorem Multiset.map_eq_cons {α : Type u_1} {β : Type v} [DecidableEq α] (f : αβ) (s : Multiset α) (t : Multiset β) (b : β) :
                                              (∃ a ∈ s, f a = b Multiset.map f (Multiset.erase s a) = t) Multiset.map f s = b ::ₘ t
                                              @[simp]
                                              theorem Multiset.mem_map_of_injective {α : Type u_1} {β : Type v} {f : αβ} (H : Function.Injective f) {a : α} {s : Multiset α} :
                                              f a Multiset.map f s a s
                                              @[simp]
                                              theorem Multiset.map_map {α : Type u_1} {β : Type v} {γ : Type u_2} (g : βγ) (f : αβ) (s : Multiset α) :
                                              theorem Multiset.map_id {α : Type u_1} (s : Multiset α) :
                                              @[simp]
                                              theorem Multiset.map_id' {α : Type u_1} (s : Multiset α) :
                                              Multiset.map (fun (x : α) => x) s = s
                                              theorem Multiset.map_const {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) :
                                              Multiset.map (Function.const α b) s = Multiset.replicate (Multiset.card s) b
                                              @[simp]
                                              theorem Multiset.map_const' {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) :
                                              Multiset.map (fun (x : α) => b) s = Multiset.replicate (Multiset.card s) b
                                              theorem Multiset.eq_of_mem_map_const {α : Type u_1} {β : Type v} {b₁ : β} {b₂ : β} {l : List α} (h : b₁ Multiset.map (Function.const α b₂) l) :
                                              b₁ = b₂
                                              @[simp]
                                              theorem Multiset.map_le_map {α : Type u_1} {β : Type v} {f : αβ} {s : Multiset α} {t : Multiset α} (h : s t) :
                                              @[simp]
                                              theorem Multiset.map_lt_map {α : Type u_1} {β : Type v} {f : αβ} {s : Multiset α} {t : Multiset α} (h : s < t) :
                                              theorem Multiset.map_mono {α : Type u_1} {β : Type v} (f : αβ) :
                                              theorem Multiset.map_strictMono {α : Type u_1} {β : Type v} (f : αβ) :
                                              @[simp]
                                              theorem Multiset.map_subset_map {α : Type u_1} {β : Type v} {f : αβ} {s : Multiset α} {t : Multiset α} (H : s t) :
                                              theorem Multiset.map_erase {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : αβ) (hf : Function.Injective f) (x : α) (s : Multiset α) :
                                              theorem Multiset.map_erase_of_mem {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : αβ) (s : Multiset α) {x : α} (h : x s) :

                                              Multiset.fold #

                                              def Multiset.foldl {α : Type u_1} {β : Type v} (f : βαβ) (H : RightCommutative f) (b : β) (s : Multiset α) :
                                              β

                                              foldl f H b s is the lift of the list operation foldl f b l, which folds f over the multiset. It is well defined when f is right-commutative, that is, f (f b a₁) a₂ = f (f b a₂) a₁.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem Multiset.foldl_zero {α : Type u_1} {β : Type v} (f : βαβ) (H : RightCommutative f) (b : β) :
                                                Multiset.foldl f H b 0 = b
                                                @[simp]
                                                theorem Multiset.foldl_cons {α : Type u_1} {β : Type v} (f : βαβ) (H : RightCommutative f) (b : β) (a : α) (s : Multiset α) :
                                                Multiset.foldl f H b (a ::ₘ s) = Multiset.foldl f H (f b a) s
                                                @[simp]
                                                theorem Multiset.foldl_add {α : Type u_1} {β : Type v} (f : βαβ) (H : RightCommutative f) (b : β) (s : Multiset α) (t : Multiset α) :
                                                Multiset.foldl f H b (s + t) = Multiset.foldl f H (Multiset.foldl f H b s) t
                                                def Multiset.foldr {α : Type u_1} {β : Type v} (f : αββ) (H : LeftCommutative f) (b : β) (s : Multiset α) :
                                                β

                                                foldr f H b s is the lift of the list operation foldr f b l, which folds f over the multiset. It is well defined when f is left-commutative, that is, f a₁ (f a₂ b) = f a₂ (f a₁ b).

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem Multiset.foldr_zero {α : Type u_1} {β : Type v} (f : αββ) (H : LeftCommutative f) (b : β) :
                                                  Multiset.foldr f H b 0 = b
                                                  @[simp]
                                                  theorem Multiset.foldr_cons {α : Type u_1} {β : Type v} (f : αββ) (H : LeftCommutative f) (b : β) (a : α) (s : Multiset α) :
                                                  Multiset.foldr f H b (a ::ₘ s) = f a (Multiset.foldr f H b s)
                                                  @[simp]
                                                  theorem Multiset.foldr_singleton {α : Type u_1} {β : Type v} (f : αββ) (H : LeftCommutative f) (b : β) (a : α) :
                                                  Multiset.foldr f H b {a} = f a b
                                                  @[simp]
                                                  theorem Multiset.foldr_add {α : Type u_1} {β : Type v} (f : αββ) (H : LeftCommutative f) (b : β) (s : Multiset α) (t : Multiset α) :
                                                  Multiset.foldr f H b (s + t) = Multiset.foldr f H (Multiset.foldr f H b t) s
                                                  @[simp]
                                                  theorem Multiset.coe_foldr {α : Type u_1} {β : Type v} (f : αββ) (H : LeftCommutative f) (b : β) (l : List α) :
                                                  Multiset.foldr f H b l = List.foldr f b l
                                                  @[simp]
                                                  theorem Multiset.coe_foldl {α : Type u_1} {β : Type v} (f : βαβ) (H : RightCommutative f) (b : β) (l : List α) :
                                                  Multiset.foldl f H b l = List.foldl f b l
                                                  theorem Multiset.coe_foldr_swap {α : Type u_1} {β : Type v} (f : αββ) (H : LeftCommutative f) (b : β) (l : List α) :
                                                  Multiset.foldr f H b l = List.foldl (fun (x : β) (y : α) => f y x) b l
                                                  theorem Multiset.foldr_swap {α : Type u_1} {β : Type v} (f : αββ) (H : LeftCommutative f) (b : β) (s : Multiset α) :
                                                  Multiset.foldr f H b s = Multiset.foldl (fun (x : β) (y : α) => f y x) b s
                                                  theorem Multiset.foldl_swap {α : Type u_1} {β : Type v} (f : βαβ) (H : RightCommutative f) (b : β) (s : Multiset α) :
                                                  Multiset.foldl f H b s = Multiset.foldr (fun (x : α) (y : β) => f y x) b s
                                                  theorem Multiset.foldr_induction' {α : Type u_1} {β : Type v} (f : αββ) (H : LeftCommutative f) (x : β) (q : αProp) (p : βProp) (s : Multiset α) (hpqf : ∀ (a : α) (b : β), q ap bp (f a b)) (px : p x) (q_s : as, q a) :
                                                  p (Multiset.foldr f H x s)
                                                  theorem Multiset.foldr_induction {α : Type u_1} (f : ααα) (H : LeftCommutative f) (x : α) (p : αProp) (s : Multiset α) (p_f : ∀ (a b : α), p ap bp (f a b)) (px : p x) (p_s : as, p a) :
                                                  p (Multiset.foldr f H x s)
                                                  theorem Multiset.foldl_induction' {α : Type u_1} {β : Type v} (f : βαβ) (H : RightCommutative f) (x : β) (q : αProp) (p : βProp) (s : Multiset α) (hpqf : ∀ (a : α) (b : β), q ap bp (f b a)) (px : p x) (q_s : as, q a) :
                                                  p (Multiset.foldl f H x s)
                                                  theorem Multiset.foldl_induction {α : Type u_1} (f : ααα) (H : RightCommutative f) (x : α) (p : αProp) (s : Multiset α) (p_f : ∀ (a b : α), p ap bp (f b a)) (px : p x) (p_s : as, p a) :
                                                  p (Multiset.foldl f H x s)

                                                  Map for partial functions #

                                                  def Multiset.pmap {α : Type u_1} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (s : Multiset α) :
                                                  (as, p a)Multiset β

                                                  Lift of the list pmap operation. Map a partial function f over a multiset s whose elements are all in the domain of f.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem Multiset.coe_pmap {α : Type u_1} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (l : List α) (H : al, p a) :
                                                    Multiset.pmap f (l) H = (List.pmap f l H)
                                                    @[simp]
                                                    theorem Multiset.pmap_zero {α : Type u_1} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (h : a0, p a) :
                                                    @[simp]
                                                    theorem Multiset.pmap_cons {α : Type u_1} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (a : α) (m : Multiset α) (h : ba ::ₘ m, p b) :
                                                    Multiset.pmap f (a ::ₘ m) h = f a ::ₘ Multiset.pmap f m
                                                    def Multiset.attach {α : Type u_1} (s : Multiset α) :
                                                    Multiset { x : α // x s }

                                                    "Attach" a proof that a ∈ s to each element a in s to produce a multiset on {x // x ∈ s}.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem Multiset.coe_attach {α : Type u_1} (l : List α) :
                                                      theorem Multiset.sizeOf_lt_sizeOf_of_mem {α : Type u_1} [SizeOf α] {x : α} {s : Multiset α} (hx : x s) :
                                                      theorem Multiset.pmap_eq_map {α : Type u_1} {β : Type v} (p : αProp) (f : αβ) (s : Multiset α) (H : as, p a) :
                                                      Multiset.pmap (fun (a : α) (x : p a) => f a) s H = Multiset.map f s
                                                      theorem Multiset.pmap_congr {α : Type u_1} {β : Type v} {p : αProp} {q : αProp} {f : (a : α) → p aβ} {g : (a : α) → q aβ} (s : Multiset α) {H₁ : as, p a} {H₂ : as, q a} :
                                                      (as, ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂)Multiset.pmap f s H₁ = Multiset.pmap g s H₂
                                                      theorem Multiset.map_pmap {α : Type u_1} {β : Type v} {γ : Type u_2} {p : αProp} (g : βγ) (f : (a : α) → p aβ) (s : Multiset α) (H : as, p a) :
                                                      Multiset.map g (Multiset.pmap f s H) = Multiset.pmap (fun (a : α) (h : p a) => g (f a h)) s H
                                                      theorem Multiset.pmap_eq_map_attach {α : Type u_1} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (s : Multiset α) (H : as, p a) :
                                                      Multiset.pmap f s H = Multiset.map (fun (x : { x : α // x s }) => f x ) (Multiset.attach s)
                                                      theorem Multiset.attach_map_val' {α : Type u_1} {β : Type v} (s : Multiset α) (f : αβ) :
                                                      Multiset.map (fun (i : { x : α // x s }) => f i) (Multiset.attach s) = Multiset.map f s
                                                      @[simp]
                                                      theorem Multiset.attach_map_val {α : Type u_1} (s : Multiset α) :
                                                      Multiset.map Subtype.val (Multiset.attach s) = s
                                                      @[simp]
                                                      theorem Multiset.mem_attach {α : Type u_1} (s : Multiset α) (x : { x : α // x s }) :
                                                      @[simp]
                                                      theorem Multiset.mem_pmap {α : Type u_1} {β : Type v} {p : αProp} {f : (a : α) → p aβ} {s : Multiset α} {H : as, p a} {b : β} :
                                                      b Multiset.pmap f s H ∃ (a : α) (h : a s), f a = b
                                                      @[simp]
                                                      theorem Multiset.card_pmap {α : Type u_1} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (s : Multiset α) (H : as, p a) :
                                                      Multiset.card (Multiset.pmap f s H) = Multiset.card s
                                                      @[simp]
                                                      theorem Multiset.card_attach {α : Type u_1} {m : Multiset α} :
                                                      Multiset.card (Multiset.attach m) = Multiset.card m
                                                      @[simp]
                                                      theorem Multiset.attach_zero {α : Type u_1} :
                                                      theorem Multiset.attach_cons {α : Type u_1} (a : α) (m : Multiset α) :
                                                      Multiset.attach (a ::ₘ m) = { val := a, property := } ::ₘ Multiset.map (fun (p : { x : α // x m }) => { val := p, property := }) (Multiset.attach m)
                                                      def Multiset.decidableForallMultiset {α : Type u_1} {m : Multiset α} {p : αProp} [hp : (a : α) → Decidable (p a)] :
                                                      Decidable (am, p a)

                                                      If p is a decidable predicate, so is the predicate that all elements of a multiset satisfy p.

                                                      Equations
                                                      Instances For
                                                        instance Multiset.decidableDforallMultiset {α : Type u_1} {m : Multiset α} {p : (a : α) → a mProp} [_hp : (a : α) → (h : a m) → Decidable (p a h)] :
                                                        Decidable (∀ (a : α) (h : a m), p a h)
                                                        Equations
                                                        instance Multiset.decidableEqPiMultiset {α : Type u_1} {m : Multiset α} {β : αType u_3} [h : (a : α) → DecidableEq (β a)] :
                                                        DecidableEq ((a : α) → a mβ a)

                                                        decidable equality for functions whose domain is bounded by multisets

                                                        Equations
                                                        def Multiset.decidableExistsMultiset {α : Type u_1} {m : Multiset α} {p : αProp} [DecidablePred p] :
                                                        Decidable (∃ x ∈ m, p x)

                                                        If p is a decidable predicate, so is the existence of an element in a multiset satisfying p.

                                                        Equations
                                                        Instances For
                                                          instance Multiset.decidableDexistsMultiset {α : Type u_1} {m : Multiset α} {p : (a : α) → a mProp} [_hp : (a : α) → (h : a m) → Decidable (p a h)] :
                                                          Decidable (∃ (a : α) (h : a m), p a h)
                                                          Equations

                                                          Subtraction #

                                                          def Multiset.sub {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :

                                                          s - t is the multiset such that count a (s - t) = count a s - count a t for all a (note that it is truncated subtraction, so it is 0 if count a t ≥ count a s).

                                                          Equations
                                                          Instances For
                                                            instance Multiset.instSubMultiset {α : Type u_1} [DecidableEq α] :
                                                            Equations
                                                            • Multiset.instSubMultiset = { sub := Multiset.sub }
                                                            @[simp]
                                                            theorem Multiset.coe_sub {α : Type u_1} [DecidableEq α] (s : List α) (t : List α) :
                                                            s - t = (List.diff s t)
                                                            theorem Multiset.sub_zero {α : Type u_1} [DecidableEq α] (s : Multiset α) :
                                                            s - 0 = s

                                                            This is a special case of tsub_zero, which should be used instead of this. This is needed to prove OrderedSub (Multiset α).

                                                            @[simp]
                                                            theorem Multiset.sub_cons {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :
                                                            s - a ::ₘ t = Multiset.erase s a - t
                                                            theorem Multiset.sub_le_iff_le_add {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} :
                                                            s - t u s u + t

                                                            This is a special case of tsub_le_iff_right, which should be used instead of this. This is needed to prove OrderedSub (Multiset α).

                                                            theorem Multiset.cons_sub_of_le {α : Type u_1} [DecidableEq α] (a : α) {s : Multiset α} {t : Multiset α} (h : t s) :
                                                            a ::ₘ s - t = a ::ₘ (s - t)
                                                            theorem Multiset.sub_eq_fold_erase {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                            s - t = Multiset.foldl Multiset.erase s t
                                                            @[simp]
                                                            theorem Multiset.card_sub {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (h : t s) :
                                                            Multiset.card (s - t) = Multiset.card s - Multiset.card t

                                                            Union #

                                                            def Multiset.union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :

                                                            s ∪ t is the lattice join operation with respect to the multiset . The multiplicity of a in s ∪ t is the maximum of the multiplicities in s and t.

                                                            Equations
                                                            Instances For
                                                              Equations
                                                              • Multiset.instUnionMultiset = { union := Multiset.union }
                                                              theorem Multiset.union_def {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                              s t = s - t + t
                                                              theorem Multiset.le_union_left {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                              s s t
                                                              theorem Multiset.le_union_right {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                              t s t
                                                              theorem Multiset.eq_union_left {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
                                                              t ss t = s
                                                              theorem Multiset.union_le_union_right {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (h : s t) (u : Multiset α) :
                                                              s u t u
                                                              theorem Multiset.union_le {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} (h₁ : s u) (h₂ : t u) :
                                                              s t u
                                                              @[simp]
                                                              theorem Multiset.mem_union {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :
                                                              a s t a s a t
                                                              @[simp]
                                                              theorem Multiset.map_union {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] {f : αβ} (finj : Function.Injective f) {s : Multiset α} {t : Multiset α} :
                                                              @[simp]
                                                              theorem Multiset.zero_union {α : Type u_1} [DecidableEq α] {s : Multiset α} :
                                                              0 s = s
                                                              @[simp]
                                                              theorem Multiset.union_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} :
                                                              s 0 = s

                                                              Intersection #

                                                              def Multiset.inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :

                                                              s ∩ t is the lattice meet operation with respect to the multiset . The multiplicity of a in s ∩ t is the minimum of the multiplicities in s and t.

                                                              Equations
                                                              Instances For
                                                                Equations
                                                                • Multiset.instInterMultiset = { inter := Multiset.inter }
                                                                @[simp]
                                                                theorem Multiset.inter_zero {α : Type u_1} [DecidableEq α] (s : Multiset α) :
                                                                s 0 = 0
                                                                @[simp]
                                                                theorem Multiset.zero_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) :
                                                                0 s = 0
                                                                @[simp]
                                                                theorem Multiset.cons_inter_of_pos {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} :
                                                                a t(a ::ₘ s) t = a ::ₘ s Multiset.erase t a
                                                                @[simp]
                                                                theorem Multiset.cons_inter_of_neg {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} :
                                                                at(a ::ₘ s) t = s t
                                                                theorem Multiset.inter_le_left {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s t s
                                                                theorem Multiset.inter_le_right {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s t t
                                                                theorem Multiset.le_inter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} (h₁ : s t) (h₂ : s u) :
                                                                s t u
                                                                @[simp]
                                                                theorem Multiset.mem_inter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :
                                                                a s t a s a t
                                                                Equations
                                                                @[simp]
                                                                theorem Multiset.sup_eq_union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s t = s t
                                                                @[simp]
                                                                theorem Multiset.inf_eq_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s t = s t
                                                                @[simp]
                                                                theorem Multiset.le_inter_iff {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} :
                                                                s t u s t s u
                                                                @[simp]
                                                                theorem Multiset.union_le_iff {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} :
                                                                s t u s u t u
                                                                theorem Multiset.union_comm {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s t = t s
                                                                theorem Multiset.inter_comm {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s t = t s
                                                                theorem Multiset.eq_union_right {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (h : s t) :
                                                                s t = t
                                                                theorem Multiset.union_le_union_left {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (h : s t) (u : Multiset α) :
                                                                u s u t
                                                                theorem Multiset.union_le_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s t s + t
                                                                theorem Multiset.union_add_distrib {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) (u : Multiset α) :
                                                                s t + u = s + u (t + u)
                                                                theorem Multiset.add_union_distrib {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) (u : Multiset α) :
                                                                s + (t u) = s + t (s + u)
                                                                theorem Multiset.cons_union_distrib {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :
                                                                a ::ₘ (s t) = a ::ₘ s a ::ₘ t
                                                                theorem Multiset.inter_add_distrib {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) (u : Multiset α) :
                                                                s t + u = (s + u) (t + u)
                                                                theorem Multiset.add_inter_distrib {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) (u : Multiset α) :
                                                                s + t u = (s + t) (s + u)
                                                                theorem Multiset.cons_inter_distrib {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :
                                                                a ::ₘ s t = (a ::ₘ s) (a ::ₘ t)
                                                                theorem Multiset.union_add_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s t + s t = s + t
                                                                theorem Multiset.sub_add_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s - t + s t = s
                                                                theorem Multiset.sub_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                s - s t = s - t

                                                                Multiset.filter #

                                                                def Multiset.filter {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) :

                                                                Filter p s returns the elements in s (with the same multiplicities) which satisfy p, and removes the rest.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Multiset.filter_coe {α : Type u_1} (p : αProp) [DecidablePred p] (l : List α) :
                                                                  Multiset.filter p l = (List.filter (fun (b : α) => decide (p b)) l)
                                                                  @[simp]
                                                                  theorem Multiset.filter_zero {α : Type u_1} (p : αProp) [DecidablePred p] :
                                                                  theorem Multiset.filter_congr {α : Type u_1} {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] {s : Multiset α} :
                                                                  (xs, p x q x)Multiset.filter p s = Multiset.filter q s
                                                                  @[simp]
                                                                  theorem Multiset.filter_add {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) (t : Multiset α) :
                                                                  @[simp]
                                                                  theorem Multiset.filter_le {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) :
                                                                  @[simp]
                                                                  theorem Multiset.filter_subset {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) :
                                                                  theorem Multiset.filter_le_filter {α : Type u_1} (p : αProp) [DecidablePred p] {s : Multiset α} {t : Multiset α} (h : s t) :
                                                                  theorem Multiset.monotone_filter_right {α : Type u_1} (s : Multiset α) ⦃p : αProp ⦃q : αProp [DecidablePred p] [DecidablePred q] (h : ∀ (b : α), p bq b) :
                                                                  @[simp]
                                                                  theorem Multiset.filter_cons_of_pos {α : Type u_1} {p : αProp} [DecidablePred p] {a : α} (s : Multiset α) :
                                                                  @[simp]
                                                                  theorem Multiset.filter_cons_of_neg {α : Type u_1} {p : αProp} [DecidablePred p] {a : α} (s : Multiset α) :
                                                                  @[simp]
                                                                  theorem Multiset.mem_filter {α : Type u_1} {p : αProp} [DecidablePred p] {a : α} {s : Multiset α} :
                                                                  a Multiset.filter p s a s p a
                                                                  theorem Multiset.of_mem_filter {α : Type u_1} {p : αProp} [DecidablePred p] {a : α} {s : Multiset α} (h : a Multiset.filter p s) :
                                                                  p a
                                                                  theorem Multiset.mem_of_mem_filter {α : Type u_1} {p : αProp} [DecidablePred p] {a : α} {s : Multiset α} (h : a Multiset.filter p s) :
                                                                  a s
                                                                  theorem Multiset.mem_filter_of_mem {α : Type u_1} {p : αProp} [DecidablePred p] {a : α} {l : Multiset α} (m : a l) (h : p a) :
                                                                  theorem Multiset.filter_eq_self {α : Type u_1} {p : αProp} [DecidablePred p] {s : Multiset α} :
                                                                  Multiset.filter p s = s as, p a
                                                                  theorem Multiset.filter_eq_nil {α : Type u_1} {p : αProp} [DecidablePred p] {s : Multiset α} :
                                                                  Multiset.filter p s = 0 as, ¬p a
                                                                  theorem Multiset.le_filter {α : Type u_1} {p : αProp} [DecidablePred p] {s : Multiset α} {t : Multiset α} :
                                                                  s Multiset.filter p t s t as, p a
                                                                  theorem Multiset.filter_cons {α : Type u_1} {p : αProp} [DecidablePred p] {a : α} (s : Multiset α) :
                                                                  Multiset.filter p (a ::ₘ s) = (if p a then {a} else 0) + Multiset.filter p s
                                                                  theorem Multiset.filter_singleton {α : Type u_1} {a : α} (p : αProp) [DecidablePred p] :
                                                                  Multiset.filter p {a} = if p a then {a} else
                                                                  theorem Multiset.filter_nsmul {α : Type u_1} {p : αProp} [DecidablePred p] (s : Multiset α) (n : ) :
                                                                  @[simp]
                                                                  theorem Multiset.filter_sub {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                  @[simp]
                                                                  theorem Multiset.filter_union {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                  @[simp]
                                                                  theorem Multiset.filter_inter {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] (s : Multiset α) (t : Multiset α) :
                                                                  @[simp]
                                                                  theorem Multiset.filter_filter {α : Type u_1} (p : αProp) [DecidablePred p] (q : αProp) [DecidablePred q] (s : Multiset α) :
                                                                  Multiset.filter p (Multiset.filter q s) = Multiset.filter (fun (a : α) => p a q a) s
                                                                  theorem Multiset.filter_comm {α : Type u_1} (p : αProp) [DecidablePred p] (q : αProp) [DecidablePred q] (s : Multiset α) :
                                                                  theorem Multiset.filter_add_filter {α : Type u_1} (p : αProp) [DecidablePred p] (q : αProp) [DecidablePred q] (s : Multiset α) :
                                                                  Multiset.filter p s + Multiset.filter q s = Multiset.filter (fun (a : α) => p a q a) s + Multiset.filter (fun (a : α) => p a q a) s
                                                                  theorem Multiset.filter_add_not {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) :
                                                                  Multiset.filter p s + Multiset.filter (fun (a : α) => ¬p a) s = s
                                                                  theorem Multiset.map_filter {α : Type u_1} {β : Type v} (p : αProp) [DecidablePred p] (f : βα) (s : Multiset β) :
                                                                  theorem Multiset.map_filter' {α : Type u_1} {β : Type v} (p : αProp) [DecidablePred p] {f : αβ} (hf : Function.Injective f) (s : Multiset α) [DecidablePred fun (b : β) => ∃ (a : α), p a f a = b] :
                                                                  Multiset.map f (Multiset.filter p s) = Multiset.filter (fun (b : β) => ∃ (a : α), p a f a = b) (Multiset.map f s)
                                                                  theorem Multiset.card_filter_le_iff {α : Type u_1} (s : Multiset α) (P : αProp) [DecidablePred P] (n : ) :
                                                                  Multiset.card (Multiset.filter P s) n s's, n < Multiset.card s'∃ a ∈ s', ¬P a

                                                                  Simultaneously filter and map elements of a multiset #

                                                                  def Multiset.filterMap {α : Type u_1} {β : Type v} (f : αOption β) (s : Multiset α) :

                                                                  filterMap f s is a combination filter/map operation on s. The function f : α → Option β is applied to each element of s; if f a is some b then b is added to the result, otherwise a is removed from the resulting multiset.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem Multiset.filterMap_coe {α : Type u_1} {β : Type v} (f : αOption β) (l : List α) :
                                                                    @[simp]
                                                                    theorem Multiset.filterMap_zero {α : Type u_1} {β : Type v} (f : αOption β) :
                                                                    @[simp]
                                                                    theorem Multiset.filterMap_cons_none {α : Type u_1} {β : Type v} {f : αOption β} (a : α) (s : Multiset α) (h : f a = none) :
                                                                    @[simp]
                                                                    theorem Multiset.filterMap_cons_some {α : Type u_1} {β : Type v} (f : αOption β) (a : α) (s : Multiset α) {b : β} (h : f a = some b) :
                                                                    theorem Multiset.filterMap_eq_map {α : Type u_1} {β : Type v} (f : αβ) :
                                                                    theorem Multiset.filterMap_filterMap {α : Type u_1} {β : Type v} {γ : Type u_2} (f : αOption β) (g : βOption γ) (s : Multiset α) :
                                                                    theorem Multiset.map_filterMap {α : Type u_1} {β : Type v} {γ : Type u_2} (f : αOption β) (g : βγ) (s : Multiset α) :
                                                                    Multiset.map g (Multiset.filterMap f s) = Multiset.filterMap (fun (x : α) => Option.map g (f x)) s
                                                                    theorem Multiset.filterMap_map {α : Type u_1} {β : Type v} {γ : Type u_2} (f : αβ) (g : βOption γ) (s : Multiset α) :
                                                                    theorem Multiset.filter_filterMap {α : Type u_1} {β : Type v} (f : αOption β) (p : βProp) [DecidablePred p] (s : Multiset α) :
                                                                    Multiset.filter p (Multiset.filterMap f s) = Multiset.filterMap (fun (x : α) => Option.filter (fun (b : β) => decide (p b)) (f x)) s
                                                                    theorem Multiset.filterMap_filter {α : Type u_1} {β : Type v} (p : αProp) [DecidablePred p] (f : αOption β) (s : Multiset α) :
                                                                    Multiset.filterMap f (Multiset.filter p s) = Multiset.filterMap (fun (x : α) => if p x then f x else none) s
                                                                    @[simp]
                                                                    theorem Multiset.filterMap_some {α : Type u_1} (s : Multiset α) :
                                                                    @[simp]
                                                                    theorem Multiset.mem_filterMap {α : Type u_1} {β : Type v} (f : αOption β) (s : Multiset α) {b : β} :
                                                                    b Multiset.filterMap f s ∃ a ∈ s, f a = some b
                                                                    theorem Multiset.map_filterMap_of_inv {α : Type u_1} {β : Type v} (f : αOption β) (g : βα) (H : ∀ (x : α), Option.map g (f x) = some x) (s : Multiset α) :
                                                                    theorem Multiset.filterMap_le_filterMap {α : Type u_1} {β : Type v} (f : αOption β) {s : Multiset α} {t : Multiset α} (h : s t) :

                                                                    countP #

                                                                    def Multiset.countP {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) :

                                                                    countP p s counts the number of elements of s (with multiplicity) that satisfy p.

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem Multiset.coe_countP {α : Type u_1} (p : αProp) [DecidablePred p] (l : List α) :
                                                                      Multiset.countP p l = List.countP (fun (b : α) => decide (p b)) l
                                                                      @[simp]
                                                                      theorem Multiset.countP_zero {α : Type u_1} (p : αProp) [DecidablePred p] :
                                                                      @[simp]
                                                                      theorem Multiset.countP_cons_of_pos {α : Type u_1} {p : αProp} [DecidablePred p] {a : α} (s : Multiset α) :
                                                                      p aMultiset.countP p (a ::ₘ s) = Multiset.countP p s + 1
                                                                      @[simp]
                                                                      theorem Multiset.countP_cons_of_neg {α : Type u_1} {p : αProp} [DecidablePred p] {a : α} (s : Multiset α) :
                                                                      theorem Multiset.countP_cons {α : Type u_1} (p : αProp) [DecidablePred p] (b : α) (s : Multiset α) :
                                                                      Multiset.countP p (b ::ₘ s) = Multiset.countP p s + if p b then 1 else 0
                                                                      theorem Multiset.countP_eq_card_filter {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) :
                                                                      Multiset.countP p s = Multiset.card (Multiset.filter p s)
                                                                      theorem Multiset.countP_le_card {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) :
                                                                      Multiset.countP p s Multiset.card s
                                                                      @[simp]
                                                                      theorem Multiset.countP_add {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) (t : Multiset α) :
                                                                      @[simp]
                                                                      theorem Multiset.countP_nsmul {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) (n : ) :
                                                                      theorem Multiset.card_eq_countP_add_countP {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) :
                                                                      Multiset.card s = Multiset.countP p s + Multiset.countP (fun (x : α) => ¬p x) s
                                                                      def Multiset.countPAddMonoidHom {α : Type u_1} (p : αProp) [DecidablePred p] :

                                                                      countP p, the number of elements of a multiset satisfying p, promoted to an AddMonoidHom.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem Multiset.countP_sub {α : Type u_1} (p : αProp) [DecidablePred p] [DecidableEq α] {s : Multiset α} {t : Multiset α} (h : t s) :
                                                                        theorem Multiset.countP_le_of_le {α : Type u_1} (p : αProp) [DecidablePred p] {s : Multiset α} {t : Multiset α} (h : s t) :
                                                                        @[simp]
                                                                        theorem Multiset.countP_filter {α : Type u_1} (p : αProp) [DecidablePred p] (q : αProp) [DecidablePred q] (s : Multiset α) :
                                                                        Multiset.countP p (Multiset.filter q s) = Multiset.countP (fun (a : α) => p a q a) s
                                                                        theorem Multiset.countP_eq_countP_filter_add {α : Type u_1} (s : Multiset α) (p : αProp) (q : αProp) [DecidablePred p] [DecidablePred q] :
                                                                        @[simp]
                                                                        theorem Multiset.countP_True {α : Type u_1} {s : Multiset α} :
                                                                        Multiset.countP (fun (x : α) => True) s = Multiset.card s
                                                                        @[simp]
                                                                        theorem Multiset.countP_False {α : Type u_1} {s : Multiset α} :
                                                                        Multiset.countP (fun (x : α) => False) s = 0
                                                                        theorem Multiset.countP_map {α : Type u_1} {β : Type v} (f : αβ) (s : Multiset α) (p : βProp) [DecidablePred p] :
                                                                        Multiset.countP p (Multiset.map f s) = Multiset.card (Multiset.filter (fun (a : α) => p (f a)) s)
                                                                        theorem Multiset.countP_attach {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) :
                                                                        Multiset.countP (fun (a : { a : α // a s }) => p a) (Multiset.attach s) = Multiset.countP p s
                                                                        theorem Multiset.filter_attach {α : Type u_1} (s : Multiset α) (p : αProp) [DecidablePred p] :
                                                                        Multiset.filter (fun (a : { a : α // a s }) => p a) (Multiset.attach s) = Multiset.map (Subtype.map id ) (Multiset.attach (Multiset.filter p s))
                                                                        theorem Multiset.countP_pos {α : Type u_1} {p : αProp} [DecidablePred p] {s : Multiset α} :
                                                                        0 < Multiset.countP p s ∃ a ∈ s, p a
                                                                        theorem Multiset.countP_eq_zero {α : Type u_1} {p : αProp} [DecidablePred p] {s : Multiset α} :
                                                                        Multiset.countP p s = 0 as, ¬p a
                                                                        theorem Multiset.countP_eq_card {α : Type u_1} {p : αProp} [DecidablePred p] {s : Multiset α} :
                                                                        Multiset.countP p s = Multiset.card s as, p a
                                                                        theorem Multiset.countP_pos_of_mem {α : Type u_1} {p : αProp} [DecidablePred p] {s : Multiset α} {a : α} (h : a s) (pa : p a) :
                                                                        theorem Multiset.countP_congr {α : Type u_1} {s : Multiset α} {s' : Multiset α} (hs : s = s') {p : αProp} {p' : αProp} [DecidablePred p] [DecidablePred p'] (hp : xs, p x = p' x) :

                                                                        Multiplicity of an element #

                                                                        def Multiset.count {α : Type u_1} [DecidableEq α] (a : α) :
                                                                        Multiset α

                                                                        count a s is the multiplicity of a in s.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem Multiset.coe_count {α : Type u_1} [DecidableEq α] (a : α) (l : List α) :
                                                                          @[simp]
                                                                          theorem Multiset.count_zero {α : Type u_1} [DecidableEq α] (a : α) :
                                                                          @[simp]
                                                                          theorem Multiset.count_cons_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
                                                                          @[simp]
                                                                          theorem Multiset.count_cons_of_ne {α : Type u_1} [DecidableEq α] {a : α} {b : α} (h : a b) (s : Multiset α) :
                                                                          theorem Multiset.count_le_card {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
                                                                          Multiset.count a s Multiset.card s
                                                                          theorem Multiset.count_le_of_le {α : Type u_1} [DecidableEq α] (a : α) {s : Multiset α} {t : Multiset α} :
                                                                          theorem Multiset.count_le_count_cons {α : Type u_1} [DecidableEq α] (a : α) (b : α) (s : Multiset α) :
                                                                          theorem Multiset.count_cons {α : Type u_1} [DecidableEq α] (a : α) (b : α) (s : Multiset α) :
                                                                          Multiset.count a (b ::ₘ s) = Multiset.count a s + if a = b then 1 else 0
                                                                          theorem Multiset.count_singleton_self {α : Type u_1} [DecidableEq α] (a : α) :
                                                                          theorem Multiset.count_singleton {α : Type u_1} [DecidableEq α] (a : α) (b : α) :
                                                                          Multiset.count a {b} = if a = b then 1 else 0
                                                                          @[simp]
                                                                          theorem Multiset.count_add {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :
                                                                          def Multiset.countAddMonoidHom {α : Type u_1} [DecidableEq α] (a : α) :

                                                                          count a, the multiplicity of a in a multiset, promoted to an AddMonoidHom.

                                                                          Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem Multiset.count_nsmul {α : Type u_1} [DecidableEq α] (a : α) (n : ) (s : Multiset α) :
                                                                            @[simp]
                                                                            theorem Multiset.count_attach {α : Type u_1} [DecidableEq α] {s : Multiset α} (a : { x : α // x s }) :
                                                                            theorem Multiset.count_pos {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                                                            theorem Multiset.one_le_count_iff_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                                                            @[simp]
                                                                            theorem Multiset.count_eq_zero_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : as) :
                                                                            theorem Multiset.count_ne_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} :
                                                                            @[simp]
                                                                            theorem Multiset.count_eq_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} :
                                                                            Multiset.count a s = 0 as
                                                                            theorem Multiset.count_eq_card {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
                                                                            Multiset.count a s = Multiset.card s xs, a = x
                                                                            @[simp]
                                                                            theorem Multiset.count_replicate_self {α : Type u_1} [DecidableEq α] (a : α) (n : ) :
                                                                            theorem Multiset.count_replicate {α : Type u_1} [DecidableEq α] (a : α) (b : α) (n : ) :
                                                                            Multiset.count a (Multiset.replicate n b) = if a = b then n else 0
                                                                            @[simp]
                                                                            theorem Multiset.count_erase_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
                                                                            @[simp]
                                                                            theorem Multiset.count_erase_of_ne {α : Type u_1} [DecidableEq α] {a : α} {b : α} (ab : a b) (s : Multiset α) :
                                                                            @[simp]
                                                                            theorem Multiset.count_sub {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :
                                                                            @[simp]
                                                                            theorem Multiset.count_union {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :
                                                                            @[simp]
                                                                            theorem Multiset.count_inter {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) (t : Multiset α) :
                                                                            @[simp]
                                                                            theorem Multiset.count_filter_of_pos {α : Type u_1} [DecidableEq α] {p : αProp} [DecidablePred p] {a : α} {s : Multiset α} (h : p a) :
                                                                            @[simp]
                                                                            theorem Multiset.count_filter_of_neg {α : Type u_1} [DecidableEq α] {p : αProp} [DecidablePred p] {a : α} {s : Multiset α} (h : ¬p a) :
                                                                            theorem Multiset.count_filter {α : Type u_1} [DecidableEq α] {p : αProp} [DecidablePred p] {a : α} {s : Multiset α} :
                                                                            Multiset.count a (Multiset.filter p s) = if p a then Multiset.count a s else 0
                                                                            theorem Multiset.ext {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
                                                                            s = t ∀ (a : α), Multiset.count a s = Multiset.count a t
                                                                            theorem Multiset.ext' {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
                                                                            (∀ (a : α), Multiset.count a s = Multiset.count a t)s = t
                                                                            @[simp]
                                                                            theorem Multiset.coe_inter {α : Type u_1} [DecidableEq α] (s : List α) (t : List α) :
                                                                            s t = (List.bagInter s t)
                                                                            theorem Multiset.le_iff_count {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
                                                                            s t ∀ (a : α), Multiset.count a s Multiset.count a t
                                                                            Equations
                                                                            theorem Multiset.count_map {α : Type u_3} {β : Type u_4} (f : αβ) (s : Multiset α) [DecidableEq β] (b : β) :
                                                                            Multiset.count b (Multiset.map f s) = Multiset.card (Multiset.filter (fun (a : α) => b = f a) s)
                                                                            theorem Multiset.count_map_eq_count {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : αβ) (s : Multiset α) (hf : Set.InjOn f {x : α | x s}) (x : α) (H : x s) :

                                                                            Multiset.map f preserves count if f is injective on the set of elements contained in the multiset

                                                                            theorem Multiset.count_map_eq_count' {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : αβ) (s : Multiset α) (hf : Function.Injective f) (x : α) :

                                                                            Multiset.map f preserves count if f is injective

                                                                            theorem Multiset.filter_eq' {α : Type u_1} [DecidableEq α] (s : Multiset α) (b : α) :
                                                                            Multiset.filter (fun (x : α) => x = b) s = Multiset.replicate (Multiset.count b s) b
                                                                            theorem Multiset.filter_eq {α : Type u_1} [DecidableEq α] (s : Multiset α) (b : α) :
                                                                            @[simp]
                                                                            theorem Multiset.replicate_inter {α : Type u_1} [DecidableEq α] (n : ) (x : α) (s : Multiset α) :
                                                                            @[simp]
                                                                            theorem Multiset.inter_replicate {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ) (x : α) :
                                                                            theorem Multiset.erase_attach_map_val {α : Type u_1} [DecidableEq α] (s : Multiset α) (x : { x : α // x s }) :
                                                                            theorem Multiset.erase_attach_map {α : Type u_1} {β : Type v} [DecidableEq α] (s : Multiset α) (f : αβ) (x : { x : α // x s }) :
                                                                            Multiset.map (fun (j : { x : α // x s }) => f j) (Multiset.erase (Multiset.attach s) x) = Multiset.map f (Multiset.erase s x)
                                                                            theorem Multiset.addHom_ext {α : Type u_1} {β : Type v} [AddZeroClass β] ⦃f : Multiset α →+ β ⦃g : Multiset α →+ β (h : ∀ (x : α), f {x} = g {x}) :
                                                                            f = g
                                                                            @[simp]
                                                                            theorem Multiset.map_le_map_iff {α : Type u_1} {β : Type v} {f : αβ} (hf : Function.Injective f) {s : Multiset α} {t : Multiset α} :
                                                                            @[simp]
                                                                            theorem Multiset.mapEmbedding_apply {α : Type u_1} {β : Type v} (f : α β) (s : Multiset α) :
                                                                            def Multiset.mapEmbedding {α : Type u_1} {β : Type v} (f : α β) :

                                                                            Associate to an embedding f from α to β the order embedding that maps a multiset to its image under f.

                                                                            Equations
                                                                            Instances For
                                                                              theorem Multiset.count_eq_card_filter_eq {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) :
                                                                              Multiset.count a s = Multiset.card (Multiset.filter (fun (x : α) => a = x) s)
                                                                              @[simp]
                                                                              theorem Multiset.map_count_True_eq_filter_card {α : Type u_1} (s : Multiset α) (p : αProp) [DecidablePred p] :

                                                                              Mapping a multiset through a predicate and counting the Trues yields the cardinality of the set filtered by the predicate. Note that this uses the notion of a multiset of Props - due to the decidability requirements of count, the decidability instance on the LHS is different from the RHS. In particular, the decidability instance on the left leaks Classical.decEq. See here for more discussion.

                                                                              Lift a relation to Multisets #

                                                                              theorem Multiset.rel_iff {α : Type u_1} {β : Type v} (r : αβProp) :
                                                                              ∀ (a : Multiset α) (a_1 : Multiset β), Multiset.Rel r a a_1 a = 0 a_1 = 0 ∃ (a_2 : α) (b : β) (as : Multiset α) (bs : Multiset β), r a_2 b Multiset.Rel r as bs a = a_2 ::ₘ as a_1 = b ::ₘ bs
                                                                              inductive Multiset.Rel {α : Type u_1} {β : Type v} (r : αβProp) :
                                                                              Multiset αMultiset βProp

                                                                              Rel r s t -- lift the relation r between two elements to a relation between s and t, s.t. there is a one-to-one mapping between elements in s and t following r.

                                                                              Instances For
                                                                                theorem Multiset.rel_flip {α : Type u_1} {β : Type v} {r : αβProp} {s : Multiset β} {t : Multiset α} :
                                                                                theorem Multiset.rel_refl_of_refl_on {α : Type u_1} {m : Multiset α} {r : ααProp} :
                                                                                (xm, r x x)Multiset.Rel r m m
                                                                                theorem Multiset.rel_eq_refl {α : Type u_1} {s : Multiset α} :
                                                                                Multiset.Rel (fun (x x_1 : α) => x = x_1) s s
                                                                                theorem Multiset.rel_eq {α : Type u_1} {s : Multiset α} {t : Multiset α} :
                                                                                Multiset.Rel (fun (x x_1 : α) => x = x_1) s t s = t
                                                                                theorem Multiset.Rel.mono {α : Type u_1} {β : Type v} {r : αβProp} {p : αβProp} {s : Multiset α} {t : Multiset β} (hst : Multiset.Rel r s t) (h : as, bt, r a bp a b) :
                                                                                theorem Multiset.Rel.add {α : Type u_1} {β : Type v} {r : αβProp} {s : Multiset α} {t : Multiset β} {u : Multiset α} {v : Multiset β} (hst : Multiset.Rel r s t) (huv : Multiset.Rel r u v) :
                                                                                Multiset.Rel r (s + u) (t + v)
                                                                                theorem Multiset.rel_flip_eq {α : Type u_1} {s : Multiset α} {t : Multiset α} :
                                                                                Multiset.Rel (fun (a b : α) => b = a) s t s = t