Documentation

Mathlib.Data.Multiset.Fintype

Multiset coercion to type #

This module defines a CoeSort instance for multisets and gives it a Fintype instance. It also defines Multiset.toEnumFinset, which is another way to enumerate the elements of a multiset. These coercions and definitions make it easier to sum over multisets using existing Finset theory.

Main definitions #

Tags #

multiset enumeration

def Multiset.ToType {α : Type u_1} [DecidableEq α] (m : Multiset α) :
Type u_1

Auxiliary definition for the CoeSort instance. This prevents the CoeOut m α instance from inadvertently applying to other sigma types.

Equations
Instances For
    instance instCoeSortMultisetType {α : Type u_1} [DecidableEq α] :

    Create a type that has the same number of elements as the multiset. Terms of this type are triples ⟨x, ⟨i, h⟩⟩ where x : α, i : ℕ, and h : i < m.count x. This way repeated elements of a multiset appear multiple times from different values of i.

    Equations
    • instCoeSortMultisetType = { coe := Multiset.ToType }
    @[reducible, match_pattern]
    def Multiset.mkToType {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : α) (i : Fin (Multiset.count x m)) :
    m.ToType

    Constructor for terms of the coercion of m to a type. This helps Lean pick up the correct instances.

    Equations
    • m.mkToType x i = x, i
    Instances For
      instance instCoeSortMultisetType.instCoeOutToType {α : Type u_1} [DecidableEq α] {m : Multiset α} :
      CoeOut m.ToType α

      As a convenience, there is a coercion from m : Type* to α by projecting onto the first component.

      Equations
      • instCoeSortMultisetType.instCoeOutToType = { coe := fun (x : m.ToType) => x.fst }
      theorem Multiset.coe_mk {α : Type u_1} [DecidableEq α] {m : Multiset α} {x : α} {i : Fin (Multiset.count x m)} :
      (m.mkToType x i).fst = x
      @[simp]
      theorem Multiset.coe_mem {α : Type u_1} [DecidableEq α] {m : Multiset α} {x : m.ToType} :
      x.fst m
      @[simp]
      theorem Multiset.forall_coe {α : Type u_1} [DecidableEq α] {m : Multiset α} (p : m.ToTypeProp) :
      (∀ (x : m.ToType), p x) ∀ (x : α) (i : Fin (Multiset.count x m)), p x, i
      @[simp]
      theorem Multiset.exists_coe {α : Type u_1} [DecidableEq α] {m : Multiset α} (p : m.ToTypeProp) :
      (∃ (x : m.ToType), p x) ∃ (x : α) (i : Fin (Multiset.count x m)), p x, i
      instance instFintypeElemProdNatSetOfLtSndCountFst {α : Type u_1} [DecidableEq α] {m : Multiset α} :
      Fintype {p : α × | p.2 < Multiset.count p.1 m}
      Equations
      def Multiset.toEnumFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) :

      Construct a finset whose elements enumerate the elements of the multiset m. The component is used to differentiate between equal elements: if x appears n times then (x, 0), ..., and (x, n-1) appear in the Finset.

      Equations
      Instances For
        @[simp]
        theorem Multiset.mem_toEnumFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) (p : α × ) :
        p m.toEnumFinset p.2 < Multiset.count p.1 m
        theorem Multiset.mem_of_mem_toEnumFinset {α : Type u_1} [DecidableEq α] {m : Multiset α} {p : α × } (h : p m.toEnumFinset) :
        p.1 m
        @[simp]
        theorem Multiset.toEnumFinset_filter_eq {α : Type u_1} [DecidableEq α] (m : Multiset α) (a : α) :
        Finset.filter (fun (x : α × ) => x.1 = a) m.toEnumFinset = {a} ×ˢ Finset.range (Multiset.count a m)
        @[simp]
        theorem Multiset.map_toEnumFinset_fst {α : Type u_1} [DecidableEq α] (m : Multiset α) :
        Multiset.map Prod.fst m.toEnumFinset.val = m
        @[simp]
        theorem Multiset.image_toEnumFinset_fst {α : Type u_1} [DecidableEq α] (m : Multiset α) :
        Finset.image Prod.fst m.toEnumFinset = m.toFinset
        @[simp]
        theorem Multiset.map_fst_le_of_subset_toEnumFinset {α : Type u_1} [DecidableEq α] {m : Multiset α} {s : Finset (α × )} (hsm : s m.toEnumFinset) :
        Multiset.map Prod.fst s.val m
        theorem Multiset.toEnumFinset_mono {α : Type u_1} [DecidableEq α] {m₁ : Multiset α} {m₂ : Multiset α} (h : m₁ m₂) :
        m₁.toEnumFinset m₂.toEnumFinset
        @[simp]
        theorem Multiset.toEnumFinset_subset_iff {α : Type u_1} [DecidableEq α] {m₁ : Multiset α} {m₂ : Multiset α} :
        m₁.toEnumFinset m₂.toEnumFinset m₁ m₂
        @[simp]
        theorem Multiset.coeEmbedding_apply {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : m.ToType) :
        m.coeEmbedding x = (x.fst, x.snd)
        def Multiset.coeEmbedding {α : Type u_1} [DecidableEq α] (m : Multiset α) :
        m.ToType α ×

        The embedding from a multiset into α × ℕ where the second coordinate enumerates repeats. If you are looking for the function m → α, that would be plain (↑).

        Equations
        • m.coeEmbedding = { toFun := fun (x : m.ToType) => (x.fst, x.snd), inj' := }
        Instances For
          @[simp]
          theorem Multiset.coeEquiv_apply_coe {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : m.ToType) :
          (m.coeEquiv x) = m.coeEmbedding x
          @[simp]
          theorem Multiset.coeEquiv_symm_apply_snd_val {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : { x : α × // x m.toEnumFinset }) :
          (m.coeEquiv.symm x).snd = (↑x).2
          @[simp]
          theorem Multiset.coeEquiv_symm_apply_fst {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : { x : α × // x m.toEnumFinset }) :
          (m.coeEquiv.symm x).fst = (↑x).1
          def Multiset.coeEquiv {α : Type u_1} [DecidableEq α] (m : Multiset α) :
          m.ToType { x : α × // x m.toEnumFinset }

          Another way to coerce a Multiset to a type is to go through m.toEnumFinset and coerce that Finset to a type.

          Equations
          • m.coeEquiv = { toFun := fun (x : m.ToType) => m.coeEmbedding x, , invFun := fun (x : { x : α × // x m.toEnumFinset }) => (↑x).1, (↑x).2, , left_inv := , right_inv := }
          Instances For
            @[simp]
            theorem Multiset.toEmbedding_coeEquiv_trans {α : Type u_1} [DecidableEq α] (m : Multiset α) :
            m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun (x : α × ) => x m.toEnumFinset) = m.coeEmbedding
            @[irreducible]
            instance Multiset.fintypeCoe {α : Type u_1} [DecidableEq α] {m : Multiset α} :
            Fintype m.ToType
            Equations
            theorem Multiset.map_univ_coeEmbedding {α : Type u_1} [DecidableEq α] (m : Multiset α) :
            Finset.map m.coeEmbedding Finset.univ = m.toEnumFinset
            @[simp]
            theorem Multiset.map_univ_coe {α : Type u_1} [DecidableEq α] (m : Multiset α) :
            Multiset.map (fun (x : m.ToType) => x.fst) Finset.univ.val = m
            @[simp]
            theorem Multiset.map_univ {α : Type u_1} [DecidableEq α] {β : Type u_2} (m : Multiset α) (f : αβ) :
            Multiset.map (fun (x : m.ToType) => f x.fst) Finset.univ.val = Multiset.map f m
            @[simp]
            theorem Multiset.card_toEnumFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) :
            m.toEnumFinset.card = Multiset.card m
            @[simp]
            theorem Multiset.card_coe {α : Type u_1} [DecidableEq α] (m : Multiset α) :
            Fintype.card m.ToType = Multiset.card m
            theorem Multiset.sum_eq_sum_coe {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (m : Multiset α) :
            m.sum = x : m.ToType, x.fst
            theorem Multiset.prod_eq_prod_coe {α : Type u_1} [DecidableEq α] [CommMonoid α] (m : Multiset α) :
            m.prod = x : m.ToType, x.fst
            theorem Multiset.sum_eq_sum_toEnumFinset {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (m : Multiset α) :
            m.sum = xm.toEnumFinset, x.1
            theorem Multiset.prod_eq_prod_toEnumFinset {α : Type u_1} [DecidableEq α] [CommMonoid α] (m : Multiset α) :
            m.prod = xm.toEnumFinset, x.1
            theorem Multiset.sum_toEnumFinset {α : Type u_1} [DecidableEq α] {β : Type u_2} [AddCommMonoid β] (m : Multiset α) (f : αβ) :
            xm.toEnumFinset, f x.1 x.2 = x : m.ToType, f x.fst x.snd
            theorem Multiset.prod_toEnumFinset {α : Type u_1} [DecidableEq α] {β : Type u_2} [CommMonoid β] (m : Multiset α) (f : αβ) :
            xm.toEnumFinset, f x.1 x.2 = x : m.ToType, f x.fst x.snd