List.map_eq_bind
theorem List.map_eq_bind :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α), List.map f l = l.bind fun x => [f x]
This theorem states that for any two types `α` and `β`, and any function `f` from `α` to `β`, the operation of mapping `f` over a list `l` of elements of type `α` is equivalent to the operation of binding the list `l` with a function that applies `f` to each element, and wraps each result in a singleton list. In other words, `List.map f l` produces the same result as `List.bind l fun x => [f x]` for any list `l` and function `f`.
More concisely: For any types `α` and `β` and function `f` from `α` to `β`, `List.map f` on a list `l` of type `α` is equivalent to `List.bind l (fun x => [x := f x])`.
|
List.bind_singleton
theorem List.bind_singleton : ∀ {α : Type u} {β : Type v} (f : α → List β) (x : α), [x].bind f = f x
The theorem `List.bind_singleton` states that for any types `α` and `β`, for any function `f` from type `α` to a list of type `β`, and for any element `x` of type `α`, the bind operation of the list monad on the singleton list containing `x` with function `f` is equal to the result of the function `f` applied to `x`. In other words, if we apply the function `f` to each element of the singleton list `[x]` to get a list of lists, and then concatenate them all together, the result will be the same as just applying `f` to `x`.
More concisely: For all types `α` and `β`, and for every function `f : α → list β`, the application of the bind operation `>>=` to the singleton list `[x]` with `f` equals the application of `f` to `x`, i.e., `[x] >>= f = f x`.
|