@[simp]
@[simp]
theorem
Option.map_eq_bind
{α : Type u_1}
:
∀ {α_1 : Type u_2} {f : α → α_1} {x : Option α}, Option.map f x = x.bind (some ∘ f)
theorem
Option.map_congr
{α : Type u_1}
:
∀ {α_1 : Type u_2} {f g : α → α_1} {x : Option α}, (∀ (a : α), a ∈ x → f a = g a) → Option.map f x = Option.map g x
@[simp]
@[simp]
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
theorem
Option.comp_map
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
(h : β → γ)
(g : α → β)
(x : Option α)
:
Option.map (h ∘ g) x = Option.map h (Option.map g x)
@[simp]
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)
theorem
Option.mem_map_of_mem
{α : Type u_1}
{β : Type u_2}
{a : α}
{x : Option α}
(g : α → β)
(h : a ∈ x)
:
g a ∈ Option.map g x
theorem
Option.bind_map_comm
{α : Type u_1}
{β : Type u_2}
{x : Option (Option α)}
{f : α → β}
:
x.bind (Option.map f) = (Option.map (Option.map f) x).bind id
theorem
Option.join_map_eq_map_join
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x : Option (Option α)}
:
(Option.map (Option.map f) x).join = Option.map f x.join
theorem
Option.join_join
{α : Type u_1}
{x : Option (Option (Option α))}
:
x.join.join = (Option.map Option.join x).join
@[simp]
theorem
Option.some_orElse
{α : Type u_1}
(a : α)
(x : Option α)
:
(HOrElse.hOrElse (some a) fun (x_1 : Unit) => x) = some a
@[simp]
theorem
Option.none_orElse
{α : Type u_1}
(x : Option α)
:
(HOrElse.hOrElse none fun (x_1 : Unit) => x) = x
@[simp]
theorem
Option.orElse_none
{α : Type u_1}
(x : Option α)
:
(HOrElse.hOrElse x fun (x : Unit) => none) = x
theorem
Option.map_orElse
{α : Type u_1}
:
∀ {α_1 : Type u_2} {f : α → α_1} {x y : Option α},
Option.map f (HOrElse.hOrElse x fun (x : Unit) => y) = HOrElse.hOrElse (Option.map f x) fun (x : Unit) => Option.map f y
@[simp]
theorem
Option.guard_eq_some :
∀ {α : Type u_1} {p : α → Prop} {a b : α} [inst : DecidablePred p], Option.guard p a = some b ↔ a = b ∧ p a
theorem
Option.liftOrGet_eq_or_eq
{α : Type u_1}
{f : α → α → α}
(h : ∀ (a b : α), f a b = a ∨ f a b = b)
(o₁ : Option α)
(o₂ : Option α)
:
Option.liftOrGet f o₁ o₂ = o₁ ∨ Option.liftOrGet f o₁ o₂ = o₂
@[simp]
theorem
Option.liftOrGet_none_left
{α : Type u_1}
{f : α → α → α}
{b : Option α}
:
Option.liftOrGet f none b = b
@[simp]
theorem
Option.liftOrGet_none_right
{α : Type u_1}
{f : α → α → α}
{a : Option α}
:
Option.liftOrGet f a none = a
@[simp]
theorem
Option.liftOrGet_some_some
{α : Type u_1}
{f : α → α → α}
{a : α}
{b : α}
:
Option.liftOrGet f (some a) (some b) = some (f a b)
@[simp]
@[simp]
theorem
Option.getD_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α)
(o : Option α)
:
(Option.map f o).getD (f x) = f (o.getD x)
An arbitrary some a
with a : α
if α
is nonempty, and otherwise none
.
Equations
- Option.choice α = if h : Nonempty α then some (Classical.choice h) else none
Instances For
theorem
Option.choice_isSome_iff_nonempty
{α : Type u_1}
:
(Option.choice α).isSome = true ↔ Nonempty α