# Documentation

Std.Data.Option.Lemmas

theorem Option.mem_iff {α : Type u_1} {a : α} {b : } :
a b b = some a
theorem Option.some_ne_none {α : Type u_1} (x : α) :
some x none
theorem Option.forall {α : Type u_1} {p : Prop} :
((x : ) → p x) p none ((x : α) → p (some x))
theorem Option.exists {α : Type u_1} {p : Prop} :
(x, p x) p none x, p (some x)
theorem Option.get_mem {α : Type u_1} {o : } (h : ) :
o
theorem Option.get_of_mem {α : Type u_1} {a : α} {o : } (h : ) :
a o = a
theorem Option.not_mem_none {α : Type u_1} (a : α) :
¬a none
@[simp]
theorem Option.some_get {α : Type u_1} {x : } (h : ) :
some () = x
@[simp]
theorem Option.get_some {α : Type u_1} (x : α) (h : ) :
Option.get (some x) h = x
theorem Option.getD_of_ne_none {α : Type u_1} {x : } (hx : x none) (y : α) :
some () = x
theorem Option.mem_unique {α : Type u_1} {o : } {a : α} {b : α} (ha : a o) (hb : b o) :
a = b
theorem Option.ext {α : Type u_1} {o₁ : } {o₂ : } :
(∀ (a : α), a o₁ a o₂) → o₁ = o₂
theorem Option.eq_none_iff_forall_not_mem :
∀ {α : Type u_1} {o : }, o = none ∀ (a : α), ¬a o
@[simp]
theorem Option.isSome_none {α : Type u_1} :
@[simp]
theorem Option.isSome_some :
∀ {α : Type u_1} {a : α},
theorem Option.isSome_iff_exists :
∀ {α : Type u_1} {x : }, a, x = some a
@[simp]
theorem Option.isNone_none {α : Type u_1} :
@[simp]
theorem Option.isNone_some :
∀ {α : Type u_1} {a : α},
@[simp]
theorem Option.not_isSome :
∀ {α : Type u_1} {a : },
theorem Option.eq_some_iff_get_eq :
∀ {α : Type u_1} {o : } {a : α}, o = some a h, = a
theorem Option.eq_some_of_isSome {α : Type u_1} {o : } (h : ) :
o = some ()
theorem Option.not_isSome_iff_eq_none :
∀ {α : Type u_1} {o : }, o = none
theorem Option.ne_none_iff_isSome :
∀ {α : Type u_1} {o : }, o none
theorem Option.ne_none_iff_exists :
∀ {α : Type u_1} {o : }, o none x, some x = o
theorem Option.ne_none_iff_exists' :
∀ {α : Type u_1} {o : }, o none x, o = some x
theorem Option.bex_ne_none {α : Type u_1} {p : Prop} :
(x x_1, p x) x, p (some x)
theorem Option.ball_ne_none {α : Type u_1} {p : Prop} :
((x : ) → x nonep x) (x : α) → p (some x)
@[simp]
theorem Option.bind_some {α : Type u_1} (x : ) :
Option.bind x some = x
@[simp]
theorem Option.bind_eq_some :
∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {x : Option α_1} {f : α_1}, = some b a, x = some a f a = some b
@[simp]
theorem Option.bind_eq_none {α : Type u_1} {β : Type u_2} {o : } {f : α} :
= none ∀ (b : β) (a : α), a o¬b f a
theorem Option.bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} (a : ) (b : ) :
(Option.bind a fun x => Option.bind b (f x)) = Option.bind b fun y => Option.bind a fun x => f x y
theorem Option.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : ) (f : α) (g : β) :
Option.bind () g = Option.bind x fun y => Option.bind (f y) g
theorem Option.join_eq_some :
∀ {α : Type u_1} {a : α} {x : Option ()}, = some a x = some (some a)
theorem Option.join_ne_none :
∀ {α : Type u_1} {x : Option ()}, none z, x = some (some z)
theorem Option.join_ne_none' :
∀ {α : Type u_1} {x : Option ()}, ¬ = none z, x = some (some z)
theorem Option.join_eq_none :
∀ {α : Type u_1} {o : Option ()}, = none o = none o = some none
theorem Option.bind_id_eq_join {α : Type u_1} {x : Option ()} :
@[simp]
theorem Option.map_eq_map :
∀ {α α_1 : Type u_1} {f : αα_1},
theorem Option.map_none :
∀ {α α_1 : Type u_1} {f : αα_1}, f <$> none = none theorem Option.map_some : ∀ {α α_1 : Type u_1} {f : αα_1} {a : α}, f <$> some a = some (f a)
@[simp]
theorem Option.map_eq_some' :
∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {x : Option α_1} {f : α_1α}, = some b a, x = some a f a = b
theorem Option.map_eq_some :
∀ {α α_1 : Type u_1} {f : αα_1} {x : } {b : α_1}, f <$> x = some b a, x = some a f a = b @[simp] theorem Option.map_eq_none' : ∀ {α : Type u_1} {x : } {α_1 : Type u_2} {f : αα_1}, = none x = none theorem Option.map_eq_none : ∀ {α α_1 : Type u_1} {f : αα_1} {x : }, f <$> x = none x = none
theorem Option.map_eq_bind {α : Type u_1} :
∀ {α : Type u_2} {f : αα} {x : }, = Option.bind x (some f)
theorem Option.map_congr {α : Type u_1} :
∀ {α : Type u_2} {f g : αα} {x : }, (∀ (a : α), a xf a = g a) → =
@[simp]
theorem Option.map_id' {α : Type u_1} :
= id
@[simp]
theorem Option.map_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : βγ) (g : αβ) (x : ) :
Option.map h () = Option.map (h g) x
theorem Option.comp_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (h : βγ) (g : αβ) (x : ) :
Option.map (h g) x = Option.map h ()
@[simp]
theorem Option.map_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : βγ) :
theorem Option.mem_map_of_mem {α : Type u_1} {β : Type u_2} {a : α} {x : } (g : αβ) (h : a x) :
g a
theorem Option.bind_map_comm {α : Type u_1} {β : Type u_2} {x : Option ()} {f : αβ} :
theorem Option.join_map_eq_map_join {α : Type u_1} {β : Type u_2} {f : αβ} {x : Option ()} :
theorem Option.join_join {α : Type u_1} {x : Option (Option ())} :
= Option.join (Option.map Option.join x)
theorem Option.mem_of_mem_join {α : Type u_1} {a : α} {x : Option ()} (h : a ) :
some a x
@[simp]
theorem Option.some_orElse {α : Type u_1} (a : α) (x : ) :
(HOrElse.hOrElse (some a) fun x => x) = some a
@[simp]
theorem Option.none_orElse {α : Type u_1} (x : ) :
(HOrElse.hOrElse none fun x => x) = x
@[simp]
theorem Option.orElse_none {α : Type u_1} (x : ) :
(HOrElse.hOrElse x fun x => none) = x
@[simp]
theorem Option.guard_eq_some :
∀ {α : Type u_1} {p : αProp} {a b : α} [inst : ], = 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₁ : ) (o₂ : ) :
Option.liftOrGet f o₁ o₂ = o₁ Option.liftOrGet f o₁ o₂ = o₂
@[simp]
theorem Option.liftOrGet_none_left {α : Type u_1} {f : ααα} {b : } :
Option.liftOrGet f none b = b
@[simp]
theorem Option.liftOrGet_none_right {α : Type u_1} {f : ααα} {a : } :
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)
theorem Option.elim_none {β : Sort u_1} {α : Type u_2} (x : β) (f : αβ) :
Option.elim none x f = x
theorem Option.elim_some {β : Sort u_1} {α : Type u_2} (x : β) (f : αβ) (a : α) :
Option.elim (some a) x f = f a
@[simp]
theorem Option.getD_map {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) (o : ) :
Option.getD () (f x) = f ()
noncomputable def Option.choice (α : Type u_1) :

An arbitrary some a with a : α if α is nonempty, and otherwise none.

Equations
• = if h : then else none
theorem Option.choice_eq {α : Type u_1} [inst : ] (a : α) :
@[simp]
theorem Option.to_list_some {α : Type u_1} (a : α) :
= [a]
@[simp]
theorem Option.to_list_none (α : Type u_1) :