Multiset.bind_map
theorem Multiset.bind_map :
∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : β → Multiset γ) (f : α → β),
(Multiset.map f m).bind n = m.bind fun a => n (f a)
The `Multiset.bind_map` theorem states that for all types `α`, `β`, and `γ`, and for all multisets `m` of type `α`, functions `n` from `β` to multiset `γ`, and functions `f` from `α` to `β`, the operation of binding the multiset obtained by mapping `f` over `m` with `n` is the same as the operation of binding `m` with the function that first applies `f` to its argument and then applies `n`. In mathematical terms, this theorem asserts the equality of `(map f m).bind n` and `m.bind (λ a => n (f a))`, underscoring the interchangeability of the map and bind operations on multisets.
More concisely: For all types `α`, `β`, and `γ`, and for all multisets `m` of type `α`, functions `n : β -> multiset γ`, and functions `f : α -> β`, `(map f m).bind n` equals `m.bind (λ a => n (f a))`.
|
Mathlib.Data.Multiset.Bind._auxLemma.5
theorem Mathlib.Data.Multiset.Bind._auxLemma.5 :
∀ {α : Type u} {β : Type v} {l₁ : List α} {f : α → List β},
(l₁.bind f).Nodup = ((∀ x ∈ l₁, (f x).Nodup) ∧ List.Pairwise (fun a b => (f a).Disjoint (f b)) l₁)
This theorem states that for any types `α` and `β`, any element `b` of type `β`, any multiset `s` of type `α`, and any function `f` from `α` to a multiset of `β`, the condition of `b` being in the multiset obtained by binding `s` with `f` is equivalent to there existing an element `a` in `s` such that `b` is in the multiset generated by applying `f` on `a`. In other words, `b` is in the bound multiset if and only if `b` is in the image of some element of `s` under `f`.
More concisely: For any types `α` and `β`, any multiset `s` of `α`, any function `f` from `α` to multisets of `β`, and any `b` in `β`, `b` is in the multiset obtained by binding `s` with `f` if and only if there exists an `a` in `s` such that `b` is in the multiset generated by applying `f` on `a`.
|
Multiset.cons_bind
theorem Multiset.cons_bind :
∀ {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (f : α → Multiset β), (a ::ₘ s).bind f = f a + s.bind f := by
sorry
The theorem `Multiset.cons_bind` states that for any types `α` and `β`, any element `a` of type `α`, any multiset `s` of type `α`, and any function `f` from `α` to `Multiset β`, binding the function `f` to the multiset formed by consing `a` onto `s` (denoted `(a ::ₘ s)`) is equivalent to the union of the multiset resulting from applying `f` to `a` and the multiset resulting from binding `f` to `s`. In other words, we can distribute the bind operation over the addition (union) of multisets.
More concisely: For any types `α` and `β`, any element `a` of type `α`, any multiset `s` of type `α`, and any function `f` from `α` to `Multiset β`, `(f a) ⊎ (f '' s) = (f) '' (a ::ₘ s)`.
|
Multiset.join_cons
theorem Multiset.join_cons :
∀ {α : Type u_1} (s : Multiset α) (S : Multiset (Multiset α)), (s ::ₘ S).join = s + S.join
The theorem `Multiset.join_cons` states that for any type `α`, any multiset `s` of type `α`, and any multiset `S` of multisets of type `α`, the join operation on a multiset obtained by appending `s` to the front of `S` is equivalent to the multiset obtained by adding `s` to the multiset resulting from the join operation on `S`. In other words, the join operation distributes over the '+', or append, operation on multisets.
More concisely: For any type `α`, the join of a multiset `s` with the multiset obtained by joining a multiset `S` of multisets of type `α` is equal to the multiset obtained by first joining the multisets in `S` and then appending `s`.
|
Multiset.add_bind
theorem Multiset.add_bind :
∀ {α : Type u_1} {β : Type v} (s t : Multiset α) (f : α → Multiset β), (s + t).bind f = s.bind f + t.bind f := by
sorry
This theorem, `Multiset.add_bind`, states that for all types `α` and `β`, and for all multisets `s` and `t` of type `α`, and a function `f` from `α` to `Multiset β`, the bind operation on the sum of `s` and `t` with `f` is equivalent to the sum of the bind operation on `s` with `f` and the bind operation on `t` with `f`. In other words, it states that the bind operation distributes over the addition operation for multisets. This is similar to the distributive law in algebra where multiplication distributes over addition.
More concisely: For all types `α` and `β`, and for all multisets `s` and `t` of type `α` and function `f` from `α` to `Multiset β`, `(s ++ t).bind (f) = s.bind (f) ++ t.bind (f)`.
|
Multiset.map_bind
theorem Multiset.map_bind :
∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : α → Multiset β) (f : β → γ),
Multiset.map f (m.bind n) = m.bind fun a => Multiset.map f (n a)
The theorem `Multiset.map_bind` asserts that for all types `α`, `β`, and `γ`, and for all multisets `m` of type `α`, functions `n` from `α` to `Multiset β`, and functions `f` from `β` to `γ`, mapping function `f` over the binding of `m` with `n` is equivalent to binding `m` with the function that maps `f` over `n a`. In essence, this theorem encodes a form of the interchange law for multisets, demonstrating that the manner in which we bind and map over multisets can be rearranged without changing the outcome.
More concisely: For all types `α`, `β`, and `γ`, and for all multisets `m` of type `α`, functions `n : α → Multiset β`, and functions `f : β → γ`, the application of `f` over the binding of `m` with `n` is equivalent to binding `m` with the function that maps `f` over `n`.
|
Multiset.singleton_bind
theorem Multiset.singleton_bind : ∀ {α : Type u_1} {β : Type v} (a : α) (f : α → Multiset β), {a}.bind f = f a := by
sorry
This theorem, `Multiset.singleton_bind`, states that for any type `α` and `β`, any element `a` of type `α`, and any function `f` from `α` to `Multiset β`, the `bind` operation on a `Multiset` containing singleton element `a` with the function `f`, is equal to the result of applying function `f` on `a`. Essentially, it means that binding over a multiset with only one element is the same as directly applying the function to that element.
More concisely: For any type `α` and `β`, given a `Multiset` `ms` of type `α` with a single element `a`, `bind (ms) f = f a`.
|
Multiset.coe_bind
theorem Multiset.coe_bind :
∀ {α : Type u_1} {β : Type v} (l : List α) (f : α → List β), ((↑l).bind fun a => ↑(f a)) = ↑(l.bind f)
This theorem, `Multiset.coe_bind`, establishes the equivalence between the `bind` operations of multisets and lists. Specifically, for any list `l` of elements of some type `α` and any function `f` mapping elements of `α` to list of elements of some type `β`, the `bind` operation on the multiset equivalent of `l` with the function that applies `f` and then converts to a multiset, is equivalent to the list obtained by applying the `bind` operation on `l` with `f`. This `bind` operation applies `f` to each element of the list/multiset and then joins all the results together.
More concisely: For any list `l` and function `f`, the multiset `bind` operation of `f` over the multiset representation of `l` is equivalent to the list obtained by applying the list `bind` operation of `f` to `l`.
|
Multiset.bind_singleton
theorem Multiset.bind_singleton :
∀ {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β), (s.bind fun x => {f x}) = Multiset.map f s
This theorem states that for any multiset `s` of type `α` and any function `f` from `α` to `β`, applying the `bind` operation on `s` with a function that produces a singleton set from the application of `f` to each element of `s` is equivalent to directly applying the `map` operation with `f` on `s`. In other words, the multiset obtained by binding `s` with the singleton-producing function is identical to the multiset obtained by mapping `f` over `s`.
More concisely: For any multiset `s` of type `α` and function `f` from `α` to `β`, the multiset obtained by binding `s` with a function that maps each element to a singleton set is equivalent to the multiset obtained by applying `f` to each element of `s` and then taking the multiset of the resulting images.
|
Multiset.bind_zero
theorem Multiset.bind_zero : ∀ {α : Type u_1} {β : Type v} (s : Multiset α), (s.bind fun x => 0) = 0
The theorem `Multiset.bind_zero` states that for any multiset `s` of elements from some type `α`, if we bind `s` with a function that sends every element of `s` to the zero multiset, the result is the zero multiset. This is equivalent to saying that mapping every element of a multiset to an empty multiset and then flattening results in an empty multiset.
More concisely: For any multiset `s` over type `α`, the flattened result of binding each element of `s` to the zero multiset is the zero multiset.
|
Multiset.card_bind
theorem Multiset.card_bind :
∀ {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β),
Multiset.card (s.bind f) = (Multiset.map (⇑Multiset.card ∘ f) s).sum
The theorem `Multiset.card_bind` states that for any type `α` and `β`, any multiset `s` of type `α`, and any function `f` that maps an element of type `α` to a multiset of type `β`, the cardinality of the multiset obtained by binding `s` with `f` is equal to the sum of the multisets obtained by mapping the function that applies the cardinality function to `f` over `s`. This can be seen as calculating the total number of elements after a transformation `f` is applied to each element in a multiset.
More concisely: For any multiset `s` of type `α` and function `f` from `α` to multisets of `β`, the cardinality of the multiset obtained by binding `s` with `f` is equal to the sum of the cardinalities of the images of elements in `s` under `f`.
|