Option.map_id
theorem Option.map_id : ∀ {α : Type u_1}, Option.map id = id
The theorem `Option.map_id` states that for any type `α`, mapping the identity function over an `Option` value results in the same `Option` value. In other words, if we have an `Option α` (which is either `some a` for some `a` of type `α`, or `none`), and we apply the `Option.map` function to it with the identity function as the argument, we get the original `Option α` back. This is essentially stating that the `Option.map` function is compatible with the identity function.
More concisely: For any type `α`, the application of `Option.map` with the identity function to an `Option α` leaves it unchanged.
|
Option.getD_some
theorem Option.getD_some : ∀ {α : Type u_1} {a b : α}, (some a).getD b = a
This theorem states that for any type `α` and any two elements `a` and `b` of type `α`, when the `getD` function is applied to the `Option` type `some a` and a default option `b`, it always returns `a`. This is because the `getD` function is defined such that it returns the value encapsulated in the `some` type if it exists, ignoring the default option.
More concisely: For all types `α` and elements `a, b` of type `α`, `getD (some a) b = a`.
|
Option.map_some'
theorem Option.map_some' : ∀ {α : Type u_1} {β : Type u_2} (a : α) (f : α → β), Option.map f (some a) = some (f a) := by
sorry
The theorem `Option.map_some'` states that for all types `α` and `β`, for any element `a` of type `α`, and any function `f` from `α` to `β`, if you map the function `f` over the `Option` containing `a` (`some a`), then the result is the `Option` containing the result of applying `f` to `a` (`some (f a)`). In other words, the function `f` is applied directly to the value wrapped in the `Option` type.
More concisely: For all types `α` and `β`, and functions `f` from `α` to `β`, `Option.map some f a = some (f a)`.
|