Documentation

Mathlib.Data.Multiset.Basic

Basic results on multisets #

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 α) :
      s.toList = s
      @[simp]
      theorem Multiset.toList_eq_nil {α : Type u_1} {s : Multiset α} :
      s.toList = [] s = 0
      theorem Multiset.empty_toList {α : Type u_1} {s : Multiset α} :
      @[simp]
      theorem Multiset.toList_zero {α : Type u_1} :
      @[simp]
      theorem Multiset.mem_toList {α : Type u_1} {a : α} {s : Multiset α} :
      a s.toList a s
      @[simp]
      theorem Multiset.toList_eq_singleton_iff {α : Type u_1} {a : α} {m : Multiset α} :
      m.toList = [a] m = {a}
      @[simp]
      theorem Multiset.toList_singleton {α : Type u_1} (a : α) :
      @[simp]
      theorem Multiset.length_toList {α : Type u_1} (s : Multiset α) :

      Induction principles #

      @[irreducible]
      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) :
          s.strongInductionOn H = H s fun (t : Multiset α) (_h : t < s) => t.strongInductionOn H
          theorem Multiset.case_strongInductionOn {α : Type u_1} {p : Multiset αProp} (s : Multiset α) (h₀ : p 0) (h₁ : ∀ (a : α) (s : Multiset α), (∀ (t : Multiset α), t sp t)p (a ::ₘ s)) :
          p s
          @[irreducible]
          def Multiset.strongDownwardInduction {α : Type u_1} {p : Multiset αSort u_3} {n : } (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card nt₁ < t₂p t₂)t₁.card np t₁) (s : Multiset α) :
          s.card 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 α} → t₂.card nt₁ < t₂p t₂)t₁.card np t₁) (s : Multiset α) :
              strongDownwardInduction H s = H s fun {t₂ : Multiset α} (ht : t₂.card n) (_hst : s < t₂) => strongDownwardInduction H t₂ ht
              def Multiset.strongDownwardInductionOn {α : Type u_1} {p : Multiset αSort u_3} {n : } (s : Multiset α) :
              ((t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card nt₁ < t₂p t₂)t₁.card np t₁)s.card 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 α} → t₂.card nt₁ < t₂p t₂)t₁.card np t₁) :
                  (fun (a : s.card n) => s.strongDownwardInductionOn H a) = H s fun {t : Multiset α} (ht : t.card n) (_h : s < t) => t.strongDownwardInductionOn H ht
                  def Multiset.chooseX {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (_hp : ∃! a : α, a l p a) :
                  { a : α // a l p a }

                  Given a proof hp that there exists a unique a ∈ l such that p a, chooseX p l hp returns that a together with proofs of a ∈ l and p a.

                  Equations
                    Instances For
                      def Multiset.choose {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a l p a) :
                      α

                      Given a proof hp that there exists a unique a ∈ l such that p a, choose p l hp returns that a.

                      Equations
                        Instances For
                          theorem Multiset.choose_spec {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a l p a) :
                          choose p l hp l p (choose p l hp)
                          theorem Multiset.choose_mem {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a l p a) :
                          choose p l hp l
                          theorem Multiset.choose_property {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a l p a) :
                          p (choose p l hp)

                          The equivalence between lists and multisets of a subsingleton type.

                          Equations
                            Instances For
                              @[deprecated "Deprecated without replacement." (since := "2025-02-07")]
                              theorem Multiset.sizeOf_lt_sizeOf_of_mem {α : Type u_1} [SizeOf α] {x : α} {s : Multiset α} (hx : x s) :