Documentation

Mathlib.Data.Multiset.Bind

Bind operation for multisets #

This file defines a few basic operations on Multiset, notably the monadic bind.

Main declarations #

Join #

def Multiset.join {α : Type u_1} :

join S, where S is a multiset of multisets, is the lift of the list join operation, that is, the union of all the sets. join {{1, 2}, {1, 2}, {0, 1}} = {0, 1, 1, 1, 2, 2}

Equations
    Instances For
      theorem Multiset.coe_join {α : Type u_1} (L : List (List α)) :
      (↑(List.map ofList L)).join = L.flatten
      @[simp]
      theorem Multiset.join_zero {α : Type u_1} :
      join 0 = 0
      @[simp]
      theorem Multiset.join_cons {α : Type u_1} (s : Multiset α) (S : Multiset (Multiset α)) :
      (s ::ₘ S).join = s + S.join
      @[simp]
      theorem Multiset.join_add {α : Type u_1} (S T : Multiset (Multiset α)) :
      (S + T).join = S.join + T.join
      @[simp]
      theorem Multiset.singleton_join {α : Type u_1} (a : Multiset α) :
      {a}.join = a
      @[simp]
      theorem Multiset.mem_join {α : Type u_1} {a : α} {S : Multiset (Multiset α)} :
      a S.join sS, a s
      @[simp]
      theorem Multiset.card_join {α : Type u_1} (S : Multiset (Multiset α)) :
      @[simp]
      theorem Multiset.map_join {α : Type u_1} {β : Type v} (f : αβ) (S : Multiset (Multiset α)) :
      map f S.join = (map (map f) S).join
      @[simp]
      theorem Multiset.prod_join {α : Type u_1} [CommMonoid α] {S : Multiset (Multiset α)} :
      @[simp]
      theorem Multiset.sum_join {α : Type u_1} [AddCommMonoid α] {S : Multiset (Multiset α)} :
      theorem Multiset.rel_join {α : Type u_1} {β : Type v} {r : αβProp} {s : Multiset (Multiset α)} {t : Multiset (Multiset β)} (h : Rel (Rel r) s t) :
      Rel r s.join t.join

      Bind #

      def Multiset.bind {α : Type u_1} {β : Type v} (s : Multiset α) (f : αMultiset β) :

      s.bind f is the monad bind operation, defined as (s.map f).join. It is the union of f a as a ranges over s.

      Equations
        Instances For
          @[simp]
          theorem Multiset.coe_bind {α : Type u_1} {β : Type v} (l : List α) (f : αList β) :
          ((↑l).bind fun (a : α) => (f a)) = (List.flatMap f l)
          @[simp]
          theorem Multiset.zero_bind {α : Type u_1} {β : Type v} (f : αMultiset β) :
          bind 0 f = 0
          @[simp]
          theorem Multiset.cons_bind {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (f : αMultiset β) :
          (a ::ₘ s).bind f = f a + s.bind f
          @[simp]
          theorem Multiset.singleton_bind {α : Type u_1} {β : Type v} (a : α) (f : αMultiset β) :
          {a}.bind f = f a
          @[simp]
          theorem Multiset.add_bind {α : Type u_1} {β : Type v} (s t : Multiset α) (f : αMultiset β) :
          (s + t).bind f = s.bind f + t.bind f
          @[simp]
          theorem Multiset.bind_zero {α : Type u_1} {β : Type v} (s : Multiset α) :
          (s.bind fun (x : α) => 0) = 0
          @[simp]
          theorem Multiset.bind_add {α : Type u_1} {β : Type v} (s : Multiset α) (f g : αMultiset β) :
          (s.bind fun (a : α) => f a + g a) = s.bind f + s.bind g
          @[simp]
          theorem Multiset.bind_cons {α : Type u_1} {β : Type v} (s : Multiset α) (f : αβ) (g : αMultiset β) :
          (s.bind fun (a : α) => f a ::ₘ g a) = map f s + s.bind g
          @[simp]
          theorem Multiset.bind_singleton {α : Type u_1} {β : Type v} (s : Multiset α) (f : αβ) :
          (s.bind fun (x : α) => {f x}) = map f s
          @[simp]
          theorem Multiset.mem_bind {α : Type u_1} {β : Type v} {b : β} {s : Multiset α} {f : αMultiset β} :
          b s.bind f as, b f a
          @[simp]
          theorem Multiset.card_bind {α : Type u_1} {β : Type v} (s : Multiset α) (f : αMultiset β) :
          (s.bind f).card = (map (card f) s).sum
          theorem Multiset.bind_congr {α : Type u_1} {β : Type v} {f g : αMultiset β} {m : Multiset α} :
          (∀ am, f a = g a)m.bind f = m.bind g
          theorem Multiset.bind_hcongr {α : Type u_1} {β β' : Type v} {m : Multiset α} {f : αMultiset β} {f' : αMultiset β'} (h : β = β') (hf : am, f a f' a) :
          m.bind f m.bind f'
          theorem Multiset.map_bind {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : αMultiset β) (f : βγ) :
          map f (m.bind n) = m.bind fun (a : α) => map f (n a)
          theorem Multiset.bind_map {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : βMultiset γ) (f : αβ) :
          (map f m).bind n = m.bind fun (a : α) => n (f a)
          theorem Multiset.bind_assoc {α : Type u_1} {β : Type v} {γ : Type u_2} {s : Multiset α} {f : αMultiset β} {g : βMultiset γ} :
          (s.bind f).bind g = s.bind fun (a : α) => (f a).bind g
          theorem Multiset.bind_bind {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : Multiset β) {f : αβMultiset γ} :
          (m.bind fun (a : α) => n.bind fun (b : β) => f a b) = n.bind fun (b : β) => m.bind fun (a : α) => f a b
          theorem Multiset.bind_map_comm {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : Multiset β) {f : αβγ} :
          (m.bind fun (a : α) => map (fun (b : β) => f a b) n) = n.bind fun (b : β) => map (fun (a : α) => f a b) m
          @[simp]
          theorem Multiset.prod_bind {α : Type u_1} {β : Type v} [CommMonoid β] (s : Multiset α) (t : αMultiset β) :
          (s.bind t).prod = (map (fun (a : α) => (t a).prod) s).prod
          @[simp]
          theorem Multiset.sum_bind {α : Type u_1} {β : Type v} [AddCommMonoid β] (s : Multiset α) (t : αMultiset β) :
          (s.bind t).sum = (map (fun (a : α) => (t a).sum) s).sum
          theorem Multiset.rel_bind {α : Type u_1} {β : Type v} {γ : Type u_2} {δ : Type u_3} {r : αβProp} {p : γδProp} {s : Multiset α} {t : Multiset β} {f : αMultiset γ} {g : βMultiset δ} (h : Relator.LiftFun r (Rel p) f g) (hst : Rel r s t) :
          Rel p (s.bind f) (t.bind g)
          theorem Multiset.count_sum {α : Type u_1} {β : Type v} [DecidableEq α] {m : Multiset β} {f : βMultiset α} {a : α} :
          count a (map f m).sum = (map (fun (b : β) => count a (f b)) m).sum
          theorem Multiset.count_bind {α : Type u_1} {β : Type v} [DecidableEq α] {m : Multiset β} {f : βMultiset α} {a : α} :
          count a (m.bind f) = (map (fun (b : β) => count a (f b)) m).sum
          theorem Multiset.le_bind {α : Type u_4} {β : Type u_5} {f : αMultiset β} (S : Multiset α) {x : α} (hx : x S) :
          f x S.bind f
          @[simp]
          theorem Multiset.attach_bind_coe {α : Type u_1} {β : Type v} (s : Multiset α) (f : αMultiset β) :
          (s.attach.bind fun (i : { x : α // x s }) => f i) = s.bind f
          @[simp]
          theorem Multiset.nodup_bind {α : Type u_1} {β : Type v} {s : Multiset α} {f : αMultiset β} :
          (s.bind f).Nodup (∀ as, (f a).Nodup) Pairwise (Function.onFun Disjoint f) s
          @[simp]
          theorem Multiset.dedup_bind_dedup {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (s : Multiset α) (f : αMultiset β) :
          (s.dedup.bind f).dedup = (s.bind f).dedup
          theorem Multiset.fold_bind {α : Type u_1} (op : ααα) [hc : Std.Commutative op] [ha : Std.Associative op] {ι : Type u_4} (s : Multiset ι) (t : ιMultiset α) (b : ια) (b₀ : α) :
          fold op (fold op b₀ (map b s)) (s.bind t) = fold op b₀ (map (fun (i : ι) => fold op (b i) (t i)) s)

          Product of two multisets #

          def Multiset.product {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β) :
          Multiset (α × β)

          The multiplicity of (a, b) in s ×ˢ t is the product of the multiplicity of a in s and b in t.

          Equations
            Instances For
              instance Multiset.instSProd {α : Type u_1} {β : Type v} :
              SProd (Multiset α) (Multiset β) (Multiset (α × β))
              Equations
                @[simp]
                theorem Multiset.coe_product {α : Type u_1} {β : Type v} (l₁ : List α) (l₂ : List β) :
                l₁ ×ˢ l₂ = ↑(l₁ ×ˢ l₂)
                @[simp]
                theorem Multiset.zero_product {α : Type u_1} {β : Type v} (t : Multiset β) :
                0 ×ˢ t = 0
                @[simp]
                theorem Multiset.cons_product {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (t : Multiset β) :
                (a ::ₘ s) ×ˢ t = map (Prod.mk a) t + s ×ˢ t
                @[simp]
                theorem Multiset.product_zero {α : Type u_1} {β : Type v} (s : Multiset α) :
                s ×ˢ 0 = 0
                @[simp]
                theorem Multiset.product_cons {α : Type u_1} {β : Type v} (b : β) (s : Multiset α) (t : Multiset β) :
                s ×ˢ (b ::ₘ t) = map (fun (a : α) => (a, b)) s + s ×ˢ t
                @[simp]
                theorem Multiset.product_singleton {α : Type u_1} {β : Type v} (a : α) (b : β) :
                @[simp]
                theorem Multiset.add_product {α : Type u_1} {β : Type v} (s t : Multiset α) (u : Multiset β) :
                (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
                @[simp]
                theorem Multiset.product_add {α : Type u_1} {β : Type v} (s : Multiset α) (t u : Multiset β) :
                s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
                @[simp]
                theorem Multiset.card_product {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β) :
                (s ×ˢ t).card = s.card * t.card
                @[simp]
                theorem Multiset.mem_product {α : Type u_1} {β : Type v} {s : Multiset α} {t : Multiset β} {p : α × β} :
                p s.product t p.1 s p.2 t
                theorem Multiset.Nodup.product {α : Type u_1} {β : Type v} {s : Multiset α} {t : Multiset β} :
                s.Nodupt.Nodup(s ×ˢ t).Nodup

                Disjoint sum of multisets #

                def Multiset.sigma {α : Type u_1} {σ : αType u_4} (s : Multiset α) (t : (a : α) → Multiset (σ a)) :
                Multiset ((a : α) × σ a)

                Multiset.sigma s t is the dependent version of Multiset.product. It is the sum of (a, b) as a ranges over s and b ranges over t a.

                Equations
                  Instances For
                    @[simp]
                    theorem Multiset.coe_sigma {α : Type u_1} {σ : αType u_4} (l₁ : List α) (l₂ : (a : α) → List (σ a)) :
                    ((↑l₁).sigma fun (a : α) => (l₂ a)) = (l₁.sigma l₂)
                    @[simp]
                    theorem Multiset.zero_sigma {α : Type u_1} {σ : αType u_4} (t : (a : α) → Multiset (σ a)) :
                    @[simp]
                    theorem Multiset.cons_sigma {α : Type u_1} {σ : αType u_4} (a : α) (s : Multiset α) (t : (a : α) → Multiset (σ a)) :
                    (a ::ₘ s).sigma t = map (Sigma.mk a) (t a) + s.sigma t
                    @[simp]
                    theorem Multiset.sigma_singleton {α : Type u_1} {β : Type v} (a : α) (b : αβ) :
                    ({a}.sigma fun (a : α) => {b a}) = {a, b a}
                    @[simp]
                    theorem Multiset.add_sigma {α : Type u_1} {σ : αType u_4} (s t : Multiset α) (u : (a : α) → Multiset (σ a)) :
                    (s + t).sigma u = s.sigma u + t.sigma u
                    @[simp]
                    theorem Multiset.sigma_add {α : Type u_1} {σ : αType u_4} (s : Multiset α) (t u : (a : α) → Multiset (σ a)) :
                    (s.sigma fun (a : α) => t a + u a) = s.sigma t + s.sigma u
                    @[simp]
                    theorem Multiset.card_sigma {α : Type u_1} {σ : αType u_4} (s : Multiset α) (t : (a : α) → Multiset (σ a)) :
                    (s.sigma t).card = (map (fun (a : α) => (t a).card) s).sum
                    @[simp]
                    theorem Multiset.mem_sigma {α : Type u_1} {σ : αType u_4} {s : Multiset α} {t : (a : α) → Multiset (σ a)} {p : (a : α) × σ a} :
                    p s.sigma t p.fst s p.snd t p.fst
                    theorem Multiset.Nodup.sigma {α : Type u_1} {s : Multiset α} {σ : αType u_5} {t : (a : α) → Multiset (σ a)} :
                    s.Nodup(∀ (a : α), (t a).Nodup)(s.sigma t).Nodup