Documentation

Mathlib.Data.Finsupp.Multiset

Equivalence between Multiset and -valued finitely supported functions #

This defines Finsupp.toMultiset the equivalence between α →₀ ℕ and Multiset α, along with Multiset.toFinsupp the reverse equivalence and Finsupp.orderIsoMultiset (the equivalence promoted to an order isomorphism).

def Finsupp.toMultiset {α : Type u_1} :

Given f : α →₀ ℕ, f.toMultiset is the multiset with multiplicities given by the values of f on the elements of α. We define this function as an AddMonoidHom.

Under the additional assumption of [DecidableEq α], this is available as Multiset.toFinsupp : Multiset α ≃+ (α →₀ ℕ); the two declarations are separate as this assumption is only needed for one direction.

Equations
  • Finsupp.toMultiset = { toFun := fun (f : α →₀ ) => f.sum fun (a : α) (n : ) => n {a}, map_zero' := , map_add' := }
Instances For
    theorem Finsupp.toMultiset_zero {α : Type u_1} :
    Finsupp.toMultiset 0 = 0
    theorem Finsupp.toMultiset_add {α : Type u_1} (m : α →₀ ) (n : α →₀ ) :
    Finsupp.toMultiset (m + n) = Finsupp.toMultiset m + Finsupp.toMultiset n
    theorem Finsupp.toMultiset_apply {α : Type u_1} (f : α →₀ ) :
    Finsupp.toMultiset f = f.sum fun (a : α) (n : ) => n {a}
    @[simp]
    theorem Finsupp.toMultiset_single {α : Type u_1} (a : α) (n : ) :
    Finsupp.toMultiset (Finsupp.single a n) = n {a}
    theorem Finsupp.toMultiset_sum {α : Type u_1} {ι : Type u_3} {f : ια →₀ } (s : Finset ι) :
    Finsupp.toMultiset (is, f i) = is, Finsupp.toMultiset (f i)
    theorem Finsupp.toMultiset_sum_single {ι : Type u_3} (s : Finset ι) (n : ) :
    Finsupp.toMultiset (is, Finsupp.single i n) = n s.val
    @[simp]
    theorem Finsupp.card_toMultiset {α : Type u_1} (f : α →₀ ) :
    Multiset.card (Finsupp.toMultiset f) = f.sum fun (x : α) => id
    theorem Finsupp.toMultiset_map {α : Type u_1} {β : Type u_2} (f : α →₀ ) (g : αβ) :
    Multiset.map g (Finsupp.toMultiset f) = Finsupp.toMultiset (Finsupp.mapDomain g f)
    @[simp]
    theorem Finsupp.sum_toMultiset {α : Type u_1} [AddCommMonoid α] (f : α →₀ ) :
    (Finsupp.toMultiset f).sum = f.sum fun (a : α) (n : ) => n a
    @[simp]
    theorem Finsupp.prod_toMultiset {α : Type u_1} [CommMonoid α] (f : α →₀ ) :
    (Finsupp.toMultiset f).prod = f.prod fun (a : α) (n : ) => a ^ n
    @[simp]
    theorem Finsupp.toFinset_toMultiset {α : Type u_1} [DecidableEq α] (f : α →₀ ) :
    (Finsupp.toMultiset f).toFinset = f.support
    @[simp]
    theorem Finsupp.count_toMultiset {α : Type u_1} [DecidableEq α] (f : α →₀ ) (a : α) :
    Multiset.count a (Finsupp.toMultiset f) = f a
    theorem Finsupp.toMultiset_sup {α : Type u_1} [DecidableEq α] (f : α →₀ ) (g : α →₀ ) :
    Finsupp.toMultiset (f g) = Finsupp.toMultiset f Finsupp.toMultiset g
    theorem Finsupp.toMultiset_inf {α : Type u_1} [DecidableEq α] (f : α →₀ ) (g : α →₀ ) :
    Finsupp.toMultiset (f g) = Finsupp.toMultiset f Finsupp.toMultiset g
    @[simp]
    theorem Finsupp.mem_toMultiset {α : Type u_1} (f : α →₀ ) (i : α) :
    i Finsupp.toMultiset f i f.support
    @[simp]
    theorem Multiset.toFinsupp_symm_apply {α : Type u_1} [DecidableEq α] (f : α →₀ ) :
    Multiset.toFinsupp.symm f = Finsupp.toMultiset f

    Given a multiset s, s.toFinsupp returns the finitely supported function on given by the multiplicities of the elements of s.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Multiset.toFinsupp_support {α : Type u_1} [DecidableEq α] (s : Multiset α) :
      (Multiset.toFinsupp s).support = s.toFinset
      @[simp]
      theorem Multiset.toFinsupp_apply {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) :
      (Multiset.toFinsupp s) a = Multiset.count a s
      theorem Multiset.toFinsupp_zero {α : Type u_1} [DecidableEq α] :
      Multiset.toFinsupp 0 = 0
      theorem Multiset.toFinsupp_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
      Multiset.toFinsupp (s + t) = Multiset.toFinsupp s + Multiset.toFinsupp t
      @[simp]
      theorem Multiset.toFinsupp_singleton {α : Type u_1} [DecidableEq α] (a : α) :
      Multiset.toFinsupp {a} = Finsupp.single a 1
      @[simp]
      theorem Multiset.toFinsupp_toMultiset {α : Type u_1} [DecidableEq α] (s : Multiset α) :
      Finsupp.toMultiset (Multiset.toFinsupp s) = s
      theorem Multiset.toFinsupp_eq_iff {α : Type u_1} [DecidableEq α] {s : Multiset α} {f : α →₀ } :
      Multiset.toFinsupp s = f s = Finsupp.toMultiset f
      theorem Multiset.toFinsupp_union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
      Multiset.toFinsupp (s t) = Multiset.toFinsupp s Multiset.toFinsupp t
      theorem Multiset.toFinsupp_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
      Multiset.toFinsupp (s t) = Multiset.toFinsupp s Multiset.toFinsupp t
      @[simp]
      theorem Multiset.toFinsupp_sum_eq {α : Type u_1} [DecidableEq α] (s : Multiset α) :
      ((Multiset.toFinsupp s).sum fun (x : α) => id) = Multiset.card s
      @[simp]
      theorem Finsupp.toMultiset_toFinsupp {α : Type u_1} [DecidableEq α] (f : α →₀ ) :
      Multiset.toFinsupp (Finsupp.toMultiset f) = f
      theorem Finsupp.toMultiset_eq_iff {α : Type u_1} [DecidableEq α] {f : α →₀ } {s : Multiset α} :
      Finsupp.toMultiset f = s f = Multiset.toFinsupp s

      As an order isomorphism #

      Finsupp.toMultiset as an order isomorphism.

      Equations
      • Finsupp.orderIsoMultiset = { toEquiv := Multiset.toFinsupp.symm.toEquiv, map_rel_iff' := }
      Instances For
        @[simp]
        theorem Finsupp.coe_orderIsoMultiset {ι : Type u_3} [DecidableEq ι] :
        Finsupp.orderIsoMultiset = Finsupp.toMultiset
        @[simp]
        theorem Finsupp.coe_orderIsoMultiset_symm {ι : Type u_3} [DecidableEq ι] :
        Finsupp.orderIsoMultiset.symm = Multiset.toFinsupp
        theorem Finsupp.toMultiset_strictMono {ι : Type u_3} :
        StrictMono Finsupp.toMultiset
        theorem Finsupp.sum_id_lt_of_lt {ι : Type u_3} (m : ι →₀ ) (n : ι →₀ ) (h : m < n) :
        (m.sum fun (x : ι) => id) < n.sum fun (x : ι) => id
        theorem Finsupp.lt_wf (ι : Type u_3) :

        The order on ι →₀ ℕ is well-founded.

        Equations
        theorem Multiset.toFinsupp_strictMono {ι : Type u_3} [DecidableEq ι] :
        StrictMono Multiset.toFinsupp
        def Sym.equivNatSum (α : Type u_1) [DecidableEq α] (n : ) :
        Sym α n { P : α →₀ // (P.sum fun (x : α) => id) = n }

        The nth symmetric power of a type α is naturally equivalent to the subtype of finitely-supported maps α →₀ ℕ with total mass n.

        See also Sym.equivNatSumOfFintype when α is finite.

        Equations
        Instances For
          @[simp]
          theorem Sym.coe_equivNatSum_apply_apply (α : Type u_1) [DecidableEq α] (n : ) (s : Sym α n) (a : α) :
          ((Sym.equivNatSum α n) s) a = Multiset.count a s
          @[simp]
          theorem Sym.coe_equivNatSum_symm_apply (α : Type u_1) [DecidableEq α] (n : ) (P : { P : α →₀ // (P.sum fun (x : α) => id) = n }) :
          ((Sym.equivNatSum α n).symm P) = Finsupp.toMultiset P
          noncomputable def Sym.equivNatSumOfFintype (α : Type u_1) [DecidableEq α] (n : ) [Fintype α] :
          Sym α n { P : α // i : α, P i = n }

          The nth symmetric power of a finite type α is naturally equivalent to the subtype of maps α → ℕ with total mass n.

          See also Sym.equivNatSum when α is not necessarily finite.

          Equations
          Instances For
            @[simp]
            theorem Sym.coe_equivNatSumOfFintype_apply_apply (α : Type u_1) [DecidableEq α] (n : ) [Fintype α] (s : Sym α n) (a : α) :
            @[simp]
            theorem Sym.coe_equivNatSumOfFintype_symm_apply (α : Type u_1) [DecidableEq α] (n : ) [Fintype α] (P : { P : α // i : α, P i = n }) :
            ((Sym.equivNatSumOfFintype α n).symm P) = a : α, P a {a}