Option.map_map
theorem Option.map_map :
∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : β → γ) (g : α → β) (x : Option α),
Option.map h (Option.map g x) = Option.map (h ∘ g) x
The theorem `Option.map_map` states that for any types `α`, `β`, and `γ`, and for any functions `h : β → γ` and `g : α → β`, and for any optional value `x` of type `Option α`, mapping function `h` over the result of mapping function `g` over `x` is equivalent to mapping the composition function `h ∘ g` over `x`. In other words, the process of mapping over optional values is associative with respect to function composition. This is a formal statement of the property of functor composition in the context of the `Option` functor.
More concisely: For any types `α`, `β`, and `γ`, and functions `g : α → β` and `h : β → γ`, the optional value `Option.map (h ∘ g) x` is equal to `Option.map h (Option.map g x)`, where `x` is an optional value of type `Option α`.
|
Option.not_mem_none
theorem Option.not_mem_none : ∀ {α : Type u_1} (a : α), a ∉ none
This theorem states that for all types `α` and any element `a` of type `α`, `a` is not in the `none` option. In other words, no matter what type and element you choose, it cannot be a member of an option that is `none`, as `none` represents the absence of a value in the `Option` type in Lean.
More concisely: For all types `α` and elements `a` of type `α`, `a` is not contained in an option of type `option α` that is equal to `none`.
|
Option.isSome_iff_exists
theorem Option.isSome_iff_exists : ∀ {α : Type u_1} {x : Option α}, x.isSome = true ↔ ∃ a, x = some a
This theorem `Option.isSome_iff_exists` states that for all types `α` and all options `x` of type `α`, the function `Option.isSome` applied to `x` equals `true` if and only if there exists some `a` such that `x` equals `some a`. In other words, an option `x` contains some value if and only if there exists a value such that `x` is the option of that value.
More concisely: For any type `α` and option `x` of type `option α`, `Option.isSome x` holds if and only if there exists an `a` such that `x = some a`.
|
Option.map_comp_map
theorem Option.map_comp_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ),
Option.map g ∘ Option.map f = Option.map (g ∘ f)
The theorem `Option.map_comp_map` asserts that for all types `α`, `β`, and `γ`, and for all functions `f` from `α` to `β` and `g` from `β` to `γ`, composing map operations on `Option` types is equivalent to mapping the composition of the two functions. In other words, mapping `g` over the result of mapping `f` over an `Option` type is the same as mapping the composition of `g` and `f` over the `Option` type. This theorem embodies the principle of function composition preservation under the `Option.map` operation.
More concisely: For all types `α`, `β`, and `γ`, and functions `f : α → β` and `g : β → γ`, `Option.map (g) (Option.map f (some x)) = Option.map (g ∘ f) (some x)`.
|
Option.mem_unique
theorem Option.mem_unique : ∀ {α : Type u_1} {o : Option α} {a b : α}, a ∈ o → b ∈ o → a = b
This theorem, `Option.mem_unique`, states that for any type `α`, any instance of `Option α` denoted by `o`, and any two instances of `α` denoted by `a` and `b`, if both `a` and `b` are members of `o`, then `a` must be equal to `b`. In other words, it guarantees that an Option type in Lean 4 can't contain more than one distinct value, reinforcing the concept of an Option as a container that either holds one value or none.
More concisely: Given an Option type `o` of any type `α`, if `a` and `b` are two elements in `o`, then `a = b`.
|
Option.eq_none_iff_forall_not_mem
theorem Option.eq_none_iff_forall_not_mem : ∀ {α : Type u_1} {o : Option α}, o = none ↔ ∀ (a : α), a ∉ o
This theorem states that for any type `α` and any option `o` of type `Option α`, `o` is equal to `none` if and only if for every element `a` of type `α`, `a` is not an element of `o`. In other words, an option is `none` if it does not contain any elements of the type it is supposed to hold.
More concisely: For any type `α` and `Option α` value `o`, `o` is equal to `none` if and only if `o` has no elements of type `α`.
|
Option.not_isSome_iff_eq_none
theorem Option.not_isSome_iff_eq_none : ∀ {α : Type u_1} {o : Option α}, ¬o.isSome = true ↔ o = none
This theorem states that for any type `α` and an instance `o` of `Option α`, the boolean function `Option.isSome o` not being true is logically equivalent to `o` being `none`. In other words, if `o` is not an instance of `some val` (i.e., `Option.isSome o` does not return `true`), then it must be `none`.
More concisely: For any type `α` and `Option α` value `o`, `Option.isSome o = false` if and only if `o` is `none`.
|
Option.map_eq_bind
theorem Option.map_eq_bind :
∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {x : Option α}, Option.map f x = x.bind (some ∘ f)
This theorem states that for any types `α` and `α_1`, any function `f` from `α` to `α_1`, and any `Option α`, applying a function `f` over the `Option α` using `Option.map` is equivalent to binding the `Option α` to the function `some ∘ f` using `Option.bind`. In other words, when we have an optional value, we can either map a function over it, or we can bind it to a function that makes an optional value out of the result, and these two operations will always produce the same result.
More concisely: For any types `α` and `α_1`, functions `f : α → α_1` and optional values `x : Option α`, `Option.map f x = Option.bind (some ∘ f) x`.
|
Option.ne_none_iff_isSome
theorem Option.ne_none_iff_isSome : ∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ o.isSome = true
This theorem, named `Option.ne_none_iff_isSome`, states that for any type `α` and an option `o` of type `α`, the option `o` is not `none` if and only if the function `Option.isSome` applied to `o` equals `true`. In other words, an optional value is not `none` exactly when it is `some` value.
More concisely: For any type `α` and option `o` of type `Option α`, `o ≠ none` if and only if `Option.isSome o` holds.
|
Option.eq_some_of_isSome
theorem Option.eq_some_of_isSome : ∀ {α : Type u_1} {o : Option α} (h : o.isSome = true), o = some (o.get h)
This theorem states that for all types `α` and for any option `o` of type `α`, if the function `Option.isSome` returns `true` when applied to `o`, then `o` must be equal to `some` applied to `Option.get o h`. In other words, if an option `o` is not `none`, it must be `some a` for some `a` and we can retrieve `a` using `Option.get`. This theorem asserts that `Option.isSome` and `Option.get` are consistent with each other.
More concisely: If `Option.isSome o` holds for an option `o` of type `α`, then `o = some (Option.get o)`.
|
Option.ne_none_iff_exists'
theorem Option.ne_none_iff_exists' : ∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ ∃ x, o = some x
This theorem, `Option.ne_none_iff_exists'`, states that for any type `α` and option `o` of this type, `o` is not `none` if and only if there exists some `x` such that `o` equals `some x`. In other words, an option is not `none` precisely when there exists a value that the option can be.
More concisely: For any type `α` and option `o` of type `option α`, the option `o` is not `none` if and only if there exists an `x` such that `o = some x`.
|
Option.ne_none_iff_exists
theorem Option.ne_none_iff_exists : ∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ ∃ x, some x = o
This theorem states that for any type `α` and any option `o` of that type, `o` is not `none` if and only if there exists an element `x` such that `some x` is equal to `o`. In other words, an option is not `none` precisely when it is `some x` for some value `x`.
More concisely: For any type `α`, an option `o` of type `option α` is non-empty (not `none`) if and only if it is the `some` value of some element `x` of type `α`.
|
Option.ext
theorem Option.ext : ∀ {α : Type u_1} {o₁ o₂ : Option α}, (∀ (a : α), a ∈ o₁ ↔ a ∈ o₂) → o₁ = o₂
This theorem, `Option.ext`, states that for any type `α`, and any two Option types `o₁` and `o₂` of type `α`, if we have that for every element `a` of type `α`, `a` is in `o₁` if and only if `a` is in `o₂`, then `o₁` and `o₂` must be equal. Essentially, it's saying that two Option types are equal if they contain the same elements.
More concisely: If two Option types `o₁` and `o₂` of type `α` have the same elements, then `o₁` is equal to `o₂`.
|
Option.exists
theorem Option.exists : ∀ {α : Type u_1} {p : Option α → Prop}, (∃ x, p x) ↔ p none ∨ ∃ x, p (some x)
This theorem, `Option.exists`, is a statement about options in Lean 4. It states that for all types `α` and all propositions `p` of type `Option α → Prop`, there exists an `x` such that `p x` holds if and only if either `p none` holds or there exists an `x` such that `p (some x)` holds. Essentially, it expresses that an existential quantifier over an option type can be decomposed into the disjunction of the proposition applied to `none` and the existence of an element of the underlying type that satisfies the proposition when wrapped with `some`.
More concisely: For any type `α` and proposition `p` over `Option α`, `Option.exists x, p x ↔ p none ∨ ∃x, p (some x)` holds. (In other words, an option `x` satisfies proposition `p` if and only if `p` holds for the `none` option or there exists an element `x` in the underlying type making `p (some x)` true.)
|
Option.some_get
theorem Option.some_get : ∀ {α : Type u_1} {x : Option α} (h : x.isSome = true), some (x.get h) = x
The theorem `Option.some_get` states that for any type `α` and any option value `x` of type `Option α`, if we can confirm that `x` is not `none` (i.e., `Option.isSome x = true`), then when we extract the value from `x` using the `Option.get` function and wrap it back into an `Option` using `some`, we get back the original option `x`.
More concisely: For any type `α` and `Option α` value `x`, if `Option.isSome x` holds, then `Option.get (Option.some x) = x`.
|
Option.some_ne_none
theorem Option.some_ne_none : ∀ {α : Type u_1} (x : α), some x ≠ none
This theorem, `Option.some_ne_none`, asserts that for any type `α` and any value `x` of type `α`, the option `some x` is not equal to `none`. In other words, an option wrapping a specific value is always distinct from an option that contains no value, irrespective of the type and the value that is wrapped.
More concisely: For all types `α` and values `x` of type `α`, `Option.some x ≠ Option.none`.
|
Option.forall
theorem Option.forall :
∀ {α : Type u_1} {p : Option α → Prop}, (∀ (x : Option α), p x) ↔ p none ∧ ∀ (x : α), p (some x)
This theorem states that for any type `α` and a property `p` that applies to `Option α`, the property `p` holds for all elements of `Option α` if and only if `p` holds for `none` and `p` holds for all elements `x` of `α` when wrapped in `some`. In other words, in terms of optional values, if a property is true for all possible optional values, it must be true both for the value `none` and for any value `x` wrapped in `some`.
More concisely: For any property `p` on `Option α`, `p` holds for all `Option α` if and only if `p(none)` and `∀x ∈ α, p(some x)` hold.
|