Option.map_injective
theorem Option.map_injective :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.Injective (Option.map f)
The theorem `Option.map_injective` states that for any types `α` and `β` and any function `f` from `α` to `β`, if `f` is injective (meaning that equal outputs imply equal inputs), then the function `Option.map f`, which applies `f` to the value inside an `Option` if it exists, is also injective. This ensures that mapping an injective function over option types preserves the injectivity property.
More concisely: If `f : α → β` is an injective function, then `Option.map f : Option α → Option β` is also an injective function.
|
Option.map_injective'
theorem Option.map_injective' : ∀ {α : Type u_1} {β : Type u_2}, Function.Injective Option.map
The theorem `Option.map_injective'` asserts that the `Option.map` function in Lean, which applies a given function to the value contained within an `Option` if it exists, is injective. This means that if two functions `f` and `g` map an `Option` of type `α` to the same `Option` of type `β` under `Option.map`, then `f` and `g` must be the same function. In other words, `Option.map` is a function between functions that has the property that equal outputs imply equal inputs.
More concisely: If two functions map an `Option` to the same `Option` under `Option.map` in Lean, then those functions are equal.
|
Option.some_injective
theorem Option.some_injective : ∀ (α : Type u_5), Function.Injective some
The theorem `Option.some_injective` states that for any type `α`, the `some` function, which wraps an element of `α` into the `Option` type, is injective. In other words, if `some a = some b` for any two elements `a` and `b` of type `α`, then it must be the case that `a = b`.
More concisely: For any type `α`, the function `some : α → Option α` is injective, i.e., `some a = some b` implies `a = b`.
|