Documentation

Mathlib.Data.Multiset.Defs

Multisets #

Multisets are finite sets with duplicates allowed. They are implemented here as the quotient of lists by permutation. This gives them computational content.

This file contains the definition of Multiset and the basic predicates. Most operations have been split off into their own files. The goal is that we can define Finset with only importing Multiset.Defs.

Main definitions #

Notation (defined later) #

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.instCoeList {α : Type u_1} :
          Coe (List α) (Multiset α)
          Equations
            @[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 (x1 x2 : List α) => x1 x2) l = l
            @[simp]
            theorem Multiset.quot_mk_to_coe'' {α : Type u_1} (l : List α) :
            Quot.mk (⇑(List.isSetoid α)) l = l
            @[simp]
            theorem Multiset.lift_coe {α : Type u_3} {β : Type u_4} (x : List α) (f : List αβ) (h : ∀ (a b : List α), a bf a = f b) :
            Quotient.lift f h x = f x
            @[simp]
            theorem Multiset.coe_eq_coe {α : Type u_1} {l₁ l₂ : List α} :
            l₁ = l₂ l₁.Perm l₂
            instance Multiset.instDecidableEquivListOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
            Decidable (l₁ l₂)
            Equations
              instance Multiset.instDecidableRListOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
              Decidable ((List.isSetoid α) l₁ l₂)
              Equations
                Equations
                  def Multiset.Mem {α : Type u_1} (s : Multiset α) (a : α) :

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

                  Equations
                    Instances For
                      instance Multiset.instMembership {α : Type u_1} :
                      Equations
                        @[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

                          Multiset.Subset #

                          def Multiset.Subset {α : Type u_1} (s 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
                              instance Multiset.instHasSubset {α : Type u_1} :
                              Equations
                                Equations
                                  instance Multiset.instIsNonstrictStrictOrder {α : Type u_1} :
                                  IsNonstrictStrictOrder (Multiset α) (fun (x1 x2 : Multiset α) => x1 x2) fun (x1 x2 : Multiset α) => x1 x2
                                  @[simp]
                                  theorem Multiset.coe_subset {α : Type u_1} {l₁ 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 t u : Multiset α} :
                                  s tt us u
                                  theorem Multiset.subset_iff {α : Type u_1} {s t : Multiset α} :
                                  s t ∀ ⦃x : α⦄, x sx t
                                  theorem Multiset.mem_of_subset {α : Type u_1} {s t : Multiset α} {a : α} (h : s t) :
                                  a sa t

                                  Partial order on Multisets #

                                  def Multiset.Le {α : Type u_1} (s 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
                                        Equations
                                          theorem Multiset.subset_of_le {α : Type u_1} {s t : Multiset α} :
                                          s ts t
                                          theorem Multiset.Le.subset {α : Type u_1} {s t : Multiset α} :
                                          s ts t

                                          Alias of Multiset.subset_of_le.

                                          theorem Multiset.mem_of_le {α : Type u_1} {s t : Multiset α} {a : α} (h : s t) :
                                          a sa t
                                          theorem Multiset.notMem_mono {α : Type u_1} {s t : Multiset α} {a : α} (h : s t) :
                                          ¬a t¬a s
                                          @[deprecated Multiset.notMem_mono (since := "2025-05-23")]
                                          theorem Multiset.not_mem_mono {α : Type u_1} {s t : Multiset α} {a : α} (h : s t) :
                                          ¬a t¬a s

                                          Alias of Multiset.notMem_mono.

                                          @[simp]
                                          theorem Multiset.coe_le {α : Type u_1} {l₁ l₂ : List α} :
                                          l₁ l₂ l₁.Subperm l₂
                                          theorem Multiset.leInductionOn {α : Type u_1} {C : Multiset αMultiset αProp} {s t : Multiset α} (h : s t) (H : ∀ {l₁ l₂ : List α}, l₁.Sublist l₂C l₁ l₂) :
                                          C s t

                                          Cardinality #

                                          def Multiset.card {α : Type u_1} :
                                          Multiset α

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

                                          Equations
                                            Instances For
                                              @[simp]
                                              theorem Multiset.coe_card {α : Type u_1} (l : List α) :
                                              (↑l).card = l.length
                                              theorem Multiset.card_le_card {α : Type u_1} {s t : Multiset α} (h : s t) :
                                              theorem Multiset.eq_of_le_of_card_le {α : Type u_1} {s t : Multiset α} (h : s t) :
                                              t.card s.cards = t
                                              theorem Multiset.card_lt_card {α : Type u_1} {s t : Multiset α} (h : s < t) :
                                              s.card < t.card

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

                                              @[simp]
                                              theorem Multiset.coe_reverse {α : Type u_1} (l : List α) :
                                              l.reverse = l

                                              Map for partial functions #

                                              def Multiset.pmap {α : Type u_1} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (s : Multiset α) :
                                              (∀ (a : α), a sp 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 : ∀ (a : α), a lp a) :
                                                  pmap f (↑l) H = (List.pmap f l H)
                                                  theorem Multiset.pmap_congr {α : Type u_1} {β : Type v} {p q : αProp} {f : (a : α) → p aβ} {g : (a : α) → q aβ} (s : Multiset α) {H₁ : ∀ (a : α), a sp a} {H₂ : ∀ (a : α), a sq a} :
                                                  (∀ (a : α), a s∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂)pmap f s H₁ = pmap g s H₂
                                                  @[simp]
                                                  theorem Multiset.mem_pmap {α : Type u_1} {β : Type v} {p : αProp} {f : (a : α) → p aβ} {s : Multiset α} {H : ∀ (a : α), a sp a} {b : β} :
                                                  b 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 : ∀ (a : α), a sp a) :
                                                  (pmap f s H).card = s.card
                                                  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 α) :
                                                      (↑l).attach = l.attach
                                                      @[simp]
                                                      theorem Multiset.mem_attach {α : Type u_1} (s : Multiset α) (x : { x : α // x s }) :
                                                      @[simp]
                                                      theorem Multiset.card_attach {α : Type u_1} {m : Multiset α} :
                                                      def Multiset.decidableForallMultiset {α : Type u_1} {m : Multiset α} {p : αProp} [(a : α) → Decidable (p a)] :
                                                      Decidable (∀ (a : α), a mp 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} [(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 : α), 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
                                                                    def Multiset.Pairwise {α : Type u_1} (r : ααProp) (m : Multiset α) :

                                                                    Pairwise r m states that there exists a list of the elements s.t. r holds pairwise on this list.

                                                                    Equations
                                                                      Instances For
                                                                        theorem Multiset.pairwise_coe_iff {α : Type u_1} {r : ααProp} {l : List α} :
                                                                        Pairwise r l (l' : List α), l.Perm l' List.Pairwise r l'
                                                                        theorem Multiset.pairwise_coe_iff_pairwise {α : Type u_1} {r : ααProp} (hr : Symmetric r) {l : List α} :
                                                                        def Multiset.Nodup {α : Type u_1} (s : Multiset α) :

                                                                        Nodup s means that s has no duplicates, i.e. the multiplicity of any element is at most 1.

                                                                        Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem Multiset.coe_nodup {α : Type u_1} {l : List α} :
                                                                            (↑l).Nodup l.Nodup
                                                                            theorem Multiset.Nodup.ext {α : Type u_1} {s t : Multiset α} :
                                                                            s.Nodupt.Nodup → (s = t ∀ (a : α), a s a t)
                                                                            theorem Multiset.le_iff_subset {α : Type u_1} {s t : Multiset α} :
                                                                            s.Nodup → (s t s t)
                                                                            theorem Multiset.nodup_of_le {α : Type u_1} {s t : Multiset α} (h : s t) :
                                                                            t.Nodups.Nodup
                                                                            instance Multiset.nodupDecidable {α : Type u_1} [DecidableEq α] (s : Multiset α) :
                                                                            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.

                                                                              This has to be defined before the definition of Finset, otherwise its automatically generated SizeOf instance will be wrong.

                                                                              Equations
                                                                                Instances For
                                                                                  instance Multiset.instSizeOf {α : Type u_1} [SizeOf α] :
                                                                                  Equations