Option of a type #
This file develops the basic theory of option types.
If α
is a type, then Option α
can be understood as the type with one more element than α
.
Option α
has terms some a
, where a : α
, and none
, which is the added element.
This is useful in multiple ways:
- It is the prototype of addition of terms to a type. See for example
WithBot α
which usesnone
as an element smaller than all others. - It can be used to define failsafe partial functions, which return
some the_result_we_expect
if we can findthe_result_we_expect
, andnone
if there is no meaningful result. This forces any subsequent use of the partial function to explicitly deal with the exceptions that make it returnnone
. Option
is a monad. We love monads.
Part
is an alternative to Option
that can be seen as the type of True
/False
values
along with a term a : α
if the value is True
.
@[simp]
theorem
Option.mem_map_of_injective
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(H : Function.Injective f)
{a : α}
{o : Option α}
:
theorem
Option.forall_mem_map
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{o : Option α}
{p : β → Prop}
:
theorem
Option.Mem.leftUnique
{α : Type u_1}
:
Relator.LeftUnique fun (x1 : α) (x2 : Option α) => x1 ∈ x2
theorem
Option.map_injective
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(Hf : Function.Injective f)
:
Option.map f
is injective if f
is injective.
@[simp]
@[simp]
Option.map
as a function between functions is injective.
@[simp]
@[deprecated Option.some_orElse (since := "2025-04-10")]
Alias of Option.some_orElse
.
@[simp]
@[deprecated Option.not_isSome (since := "2025-04-10")]
Alias of Option.not_isSome
.
@[deprecated Option.not_comp_isSome (since := "2025-04-10")]
Alias of Option.not_comp_isSome
.
@[deprecated Option.not_isNone (since := "2025-04-10")]
Alias of Option.not_isNone
.
@[deprecated Option.not_comp_isNone (since := "2025-04-10")]
Alias of Option.not_comp_isNone
.
@[deprecated Option.eq_none_iff_forall_some_ne (since := "2025-03-19")]
Alias of Option.eq_none_iff_forall_some_ne
.
@[simp]
theorem
Option.elim'_update
{α : Type u_5}
{β : Type u_6}
[DecidableEq α]
(f : β)
(g : α → β)
(a : α)
(x : β)
: