Documentation

Mathlib.Data.DFinsupp.Multiset

Equivalence between Multiset and ℕ-valued finitely supported functions #

This defines DFinsupp.toMultiset the equivalence between Π₀ a : α, ℕ and Multiset α, along with Multiset.toDFinsupp the reverse equivalence.

source
instance DFinsupp.addZeroClass' {α : Type u_1} {β : Type u_3} [AddZeroClass β] :
AddZeroClass (Π₀ (x : α), β)

Non-dependent special case of DFinsupp.addZeroClass to help typeclass search.

source
def DFinsupp.toMultiset {α : Type u_1} [DecidableEq α] :
(Π₀ (x : α), ℕ) →+ Multiset α

A DFinsupp version of Finsupp.toMultiset.

Instances For
    source
    @[simp]
    theorem DFinsupp.toMultiset_single {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) :
    ↑DFinsupp.toMultiset (DFinsupp.single a n) = Multiset.replicate n a
    source
    def Multiset.toDFinsupp {α : Type u_1} [DecidableEq α] :
    Multiset α →+ Π₀ (x : α), ℕ

    A DFinsupp version of Multiset.toFinsupp.

    Instances For
      source
      @[simp]
      theorem Multiset.toDFinsupp_apply {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) :
      ↑(↑Multiset.toDFinsupp s) a = Multiset.count a s
      source
      @[simp]
      theorem Multiset.toDFinsupp_support {α : Type u_1} [DecidableEq α] (s : Multiset α) :
      DFinsupp.support (↑Multiset.toDFinsupp s) = Multiset.toFinset s
      source
      @[simp]
      theorem Multiset.toDFinsupp_replicate {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) :
      ↑Multiset.toDFinsupp (Multiset.replicate n a) = DFinsupp.single a n
      source
      @[simp]
      theorem Multiset.toDFinsupp_singleton {α : Type u_1} [DecidableEq α] (a : α) :
      ↑Multiset.toDFinsupp {a} = DFinsupp.single a 1
      source
      @[simp]
      theorem Multiset.equivDFinsupp_symm_apply {α : Type u_1} [DecidableEq α] (a : Π₀ (x : α), ℕ) :
      ↑(AddEquiv.symm Multiset.equivDFinsupp) a = ↑DFinsupp.toMultiset a
      source
      @[simp]
      theorem Multiset.equivDFinsupp_apply {α : Type u_1} [DecidableEq α] (a : Multiset α) :
      ↑Multiset.equivDFinsupp a = ↑Multiset.toDFinsupp a
      source
      def Multiset.equivDFinsupp {α : Type u_1} [DecidableEq α] :
      Multiset α ≃+ Π₀ (x : α), ℕ

      Multiset.toDFinsupp as an AddEquiv.

      Instances For
        source
        @[simp]
        theorem Multiset.toDFinsupp_toMultiset {α : Type u_1} [DecidableEq α] (s : Multiset α) :
        ↑DFinsupp.toMultiset (↑Multiset.toDFinsupp s) = s
        source
        theorem Multiset.toDFinsupp_injective {α : Type u_1} [DecidableEq α] :
        Function.Injective ↑Multiset.toDFinsupp
        source
        @[simp]
        theorem Multiset.toDFinsupp_inj {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
        ↑Multiset.toDFinsupp s = ↑Multiset.toDFinsupp t ↔ s = t
        source
        @[simp]
        theorem Multiset.toDFinsupp_le_toDFinsupp {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
        ↑Multiset.toDFinsupp s ≤ ↑Multiset.toDFinsupp t ↔ s ≤ t
        source
        @[simp]
        theorem Multiset.toDFinsupp_lt_toDFinsupp {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
        ↑Multiset.toDFinsupp s < ↑Multiset.toDFinsupp t ↔ s < t
        source
        @[simp]
        theorem Multiset.toDFinsupp_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
        ↑Multiset.toDFinsupp (s ∩ t) = ↑Multiset.toDFinsupp s ⊓ ↑Multiset.toDFinsupp t
        source
        @[simp]
        theorem Multiset.toDFinsupp_union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
        ↑Multiset.toDFinsupp (s ∪ t) = ↑Multiset.toDFinsupp s ⊔ ↑Multiset.toDFinsupp t
        source
        @[simp]
        theorem DFinsupp.toMultiset_toDFinsupp {α : Type u_1} [DecidableEq α] (f : Π₀ (x : α), ℕ) :
        ↑Multiset.toDFinsupp (↑DFinsupp.toMultiset f) = f
        source
        theorem DFinsupp.toMultiset_injective {α : Type u_1} [DecidableEq α] :
        Function.Injective ↑DFinsupp.toMultiset
        source
        @[simp]
        theorem DFinsupp.toMultiset_inj {α : Type u_1} [DecidableEq α] {f : Π₀ (_a : α), ℕ} {g : Π₀ (_a : α), ℕ} :
        ↑DFinsupp.toMultiset f = ↑DFinsupp.toMultiset g ↔ f = g
        source
        @[simp]
        theorem DFinsupp.toMultiset_le_toMultiset {α : Type u_1} [DecidableEq α] {f : Π₀ (_a : α), ℕ} {g : Π₀ (_a : α), ℕ} :
        ↑DFinsupp.toMultiset f ≤ ↑DFinsupp.toMultiset g ↔ f ≤ g
        source
        @[simp]
        theorem DFinsupp.toMultiset_lt_toMultiset {α : Type u_1} [DecidableEq α] {f : Π₀ (_a : α), ℕ} {g : Π₀ (_a : α), ℕ} :
        ↑DFinsupp.toMultiset f < ↑DFinsupp.toMultiset g ↔ f < g
        source
        @[simp]
        theorem DFinsupp.toMultiset_inf {α : Type u_1} [DecidableEq α] (f : Π₀ (_a : α), ℕ) (g : Π₀ (_a : α), ℕ) :
        ↑DFinsupp.toMultiset (f ⊓ g) = ↑DFinsupp.toMultiset f ∩ ↑DFinsupp.toMultiset g
        source
        @[simp]
        theorem DFinsupp.toMultiset_sup {α : Type u_1} [DecidableEq α] (f : Π₀ (_a : α), ℕ) (g : Π₀ (_a : α), ℕ) :
        ↑DFinsupp.toMultiset (f ⊔ g) = ↑DFinsupp.toMultiset f ∪ ↑DFinsupp.toMultiset g