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_2} [AddZeroClass β] :
AddZeroClass (Π₀ (x : α), β)

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

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

    A DFinsupp version of Finsupp.toMultiset.

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

        A DFinsupp version of Multiset.toFinsupp.

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

            Multiset.toDFinsupp as an AddEquiv.

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