mathlib documentation

data.option.basic

theorem option.coe_def {α : Type u_1} :

theorem option.some_ne_none {α : Type u_1} (x : α) :

@[simp]
theorem option.get_mem {α : Type u_1} {o : option α} (h : (o.is_some)) :

theorem option.get_of_mem {α : Type u_1} {a : α} {o : option α} (h : (o.is_some)) :
a ooption.get h = a

@[simp]
theorem option.not_mem_none {α : Type u_1} (a : α) :

@[simp]
theorem option.some_get {α : Type u_1} {x : option α} (h : (x.is_some)) :

@[simp]
theorem option.get_some {α : Type u_1} (x : α) (h : ((some x).is_some)) :

@[simp]
theorem option.get_or_else_some {α : Type u_1} (x y : α) :

@[simp]
theorem option.get_or_else_coe {α : Type u_1} (x y : α) :

theorem option.get_or_else_of_ne_none {α : Type u_1} {x : option α} (hx : x none) (y : α) :

theorem option.mem_unique {α : Type u_1} {o : option α} {a b : α} (ha : a o) (hb : b o) :
a = b

theorem option.map_injective {α : Type u_1} {β : Type u_2} {f : α → β} (Hf : function.injective f) :

option.map f is injective if f is injective.

@[ext]
theorem option.ext {α : Type u_1} {o₁ o₂ : option α} :
(∀ (a : α), a o₁ a o₂)o₁ = o₂

theorem option.eq_none_iff_forall_not_mem {α : Type u_1} {o : option α} :
o = none ∀ (a : α), a o

@[simp]
theorem option.none_bind {α β : Type u_1} (f : α → option β) :

@[simp]
theorem option.some_bind {α β : Type u_1} (a : α) (f : α → option β) :
some a >>= f = f a

@[simp]
theorem option.none_bind' {α : Type u_1} {β : Type u_2} (f : α → option β) :

@[simp]
theorem option.some_bind' {α : Type u_1} {β : Type u_2} (a : α) (f : α → option β) :
(some a).bind f = f a

@[simp]
theorem option.bind_some {α : Type u_1} (x : option α) :
x >>= some = x

@[simp]
theorem option.bind_eq_some {α β : Type u_1} {x : option α} {f : α → option β} {b : β} :
x >>= f = some b ∃ (a : α), x = some a f a = some b

@[simp]
theorem option.bind_eq_some' {α : Type u_1} {β : Type u_2} {x : option α} {f : α → option β} {b : β} :
x.bind f = some b ∃ (a : α), x = some a f a = some b

@[simp]
theorem option.bind_eq_none' {α : Type u_1} {β : Type u_2} {o : option α} {f : α → option β} :
o.bind f = none ∀ (b : β) (a : α), a ob f a

@[simp]
theorem option.bind_eq_none {α β : Type u_1} {o : option α} {f : α → option β} :
o >>= f = none ∀ (b : β) (a : α), a ob f a

theorem option.bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → option γ} (a : option α) (b : option β) :
a.bind (λ (x : α), b.bind (f x)) = b.bind (λ (y : β), a.bind (λ (x : α), f x y))

theorem option.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : option α) (f : α → option β) (g : β → option γ) :
(x.bind f).bind g = x.bind (λ (y : α), (f y).bind g)

theorem option.join_eq_some {α : Type u_1} {x : option (option α)} {a : α} :
x.join = some a x = some (some a)

theorem option.join_ne_none {α : Type u_1} {x : option (option α)} :
x.join none ∃ (z : α), x = some (some z)

theorem option.join_ne_none' {α : Type u_1} {x : option (option α)} :
¬x.join = none ∃ (z : α), x = some (some z)

theorem option.bind_id_eq_join {α : Type u_1} {x : option (option α)} :
x >>= id = x.join

theorem option.join_eq_join {α : Type u_1} :

theorem option.bind_eq_bind {α β : Type u_1} {f : α → option β} {x : option α} :
x >>= f = x.bind f

@[simp]
theorem option.map_eq_map {α β : Type u_1} {f : α → β} :

theorem option.map_none {α β : Type u_1} {f : α → β} :

theorem option.map_some {α β : Type u_1} {a : α} {f : α → β} :
f <$> some a = some (f a)

@[simp]
theorem option.map_none' {α : Type u_1} {β : Type u_2} {f : α → β} :

@[simp]
theorem option.map_some' {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} :
option.map f (some a) = some (f a)

theorem option.map_eq_some {α β : Type u_1} {x : option α} {f : α → β} {b : β} :
f <$> x = some b ∃ (a : α), x = some a f a = b

@[simp]
theorem option.map_eq_some' {α : Type u_1} {β : Type u_2} {x : option α} {f : α → β} {b : β} :
option.map f x = some b ∃ (a : α), x = some a f a = b

theorem option.map_eq_none {α β : Type u_1} {x : option α} {f : α → β} :
f <$> x = none x = none

@[simp]
theorem option.map_eq_none' {α : Type u_1} {β : Type u_2} {x : option α} {f : α → β} :

theorem option.map_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {x : option α} (h : ∀ (a : α), a xf a = g a) :

@[simp]
theorem option.map_id' {α : Type u_1} :

@[simp]
theorem option.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (x : option α) :

theorem option.comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (x : option α) :

@[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 : option α} (g : α → β) (h : a x) :
g a option.map g x

theorem option.bind_map_comm {α β : Type u_1} {x : option (option α)} {f : α → β} :

theorem option.join_map_eq_map_join {α : Type u_1} {β : Type u_2} {f : α → β} {x : option (option α)} :

theorem option.join_join {α : Type u_1} {x : option (option (option α))} :

theorem option.mem_of_mem_join {α : Type u_1} {a : α} {x : option (option α)} (h : a x.join) :
some a x

@[simp]
theorem option.pbind_eq_bind {α : Type u_1} {β : Type u_2} (f : α → option β) (x : option α) :
x.pbind (λ (a : α) (_x : a x), f a) = x.bind f

theorem option.map_bind {α β γ : Type u_1} (f : β → γ) (x : option α) (g : α → option β) :
option.map f (x >>= g) = x >>= λ (a : α), option.map f (g a)

theorem option.map_bind' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (x : option α) (g : α → option β) :
option.map f (x.bind g) = x.bind (λ (a : α), option.map f (g a))

theorem option.map_pbind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (x : option α) (g : Π (a : α), a xoption β) :
option.map f (x.pbind g) = x.pbind (λ (a : α) (H : a x), option.map f (g a H))

theorem option.pbind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (x : option α) (g : Π (b : β), b option.map f xoption γ) :
(option.map f x).pbind g = x.pbind (λ (a : α) (h : a x), g (f a) _)

@[simp]
theorem option.pmap_none {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) {H : ∀ (a : α), a nonep a} :

@[simp]
theorem option.pmap_some {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) {x : α} (h : p x) :
option.pmap f (some x) = λ (_x : ∀ (a : α), a some xp a), some (f x h)

theorem option.mem_pmem {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (x : option α) {a : α} (h : ∀ (a : α), a xp a) (ha : a x) :
f a _ option.pmap f x h

theorem option.pmap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} (f : Π (a : α), p a → β) (g : γ → α) (x : option γ) (H : ∀ (a : α), a option.map g xp a) :
option.pmap f (option.map g x) H = option.pmap (λ (a : γ) (h : p (g a)), f (g a) h) x _

theorem option.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} (g : β → γ) (f : Π (a : α), p a → β) (x : option α) (H : ∀ (a : α), a xp a) :
option.map g (option.pmap f x H) = option.pmap (λ (a : α) (h : p a), g (f a h)) x H

@[simp]
theorem option.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : α → β) (x : option α) (H : ∀ (a : α), a xp a) :
option.pmap (λ (a : α) (_x : p a), f a) x H = option.map f x

theorem option.pmap_bind {α β γ : Type u_1} {x : option α} {g : α → option β} {p : β → Prop} {f : Π (b : β), p b → γ} (H : ∀ (a : β), a x >>= gp a) (H' : ∀ (a : α) (b : β), b g ab x >>= g) :
option.pmap f (x >>= g) H = x >>= λ (a : α), option.pmap f (g a) _

theorem option.bind_pmap {α : Type u_1} {β γ : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (x : option α) (g : β → option γ) (H : ∀ (a : α), a xp a) :
option.pmap f x H >>= g = x.pbind (λ (a : α) (h : a x), g (f a _))

theorem option.pbind_eq_none {α : Type u_1} {β : Type u_2} {x : option α} {f : Π (a : α), a xoption β} (h' : ∀ (a : α) (H : a x), f a H = nonex = none) :

theorem option.pbind_eq_some {α : Type u_1} {β : Type u_2} {x : option α} {f : Π (a : α), a xoption β} {y : β} :
x.pbind f = some y ∃ (z : α) (H : z x), f z H = some y

@[simp]
theorem option.pmap_eq_none_iff {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : Π (a : α), p a → β} {x : option α} {h : ∀ (a : α), a xp a} :

@[simp]
theorem option.pmap_eq_some_iff {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : Π (a : α), p a → β} {x : option α} {hf : ∀ (a : α), a xp a} {y : β} :
option.pmap f x hf = some y ∃ (a : α) (H : x = some a), f a _ = y

@[simp]
theorem option.join_pmap_eq_pmap_join {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : Π (a : α), p a → β} {x : option (option α)} (H : ∀ (a : option α), a x∀ (a_1 : α), a_1 ap a_1) :

@[simp]
theorem option.seq_some {α β : Type u_1} {a : α} {f : α → β} :
some f <*> some a = some (f a)

@[simp]
theorem option.some_orelse' {α : Type u_1} (a : α) (x : option α) :
(some a).orelse x = some a

@[simp]
theorem option.some_orelse {α : Type u_1} (a : α) (x : option α) :
(some a <|> x) = some a

@[simp]
theorem option.none_orelse' {α : Type u_1} (x : option α) :

@[simp]
theorem option.none_orelse {α : Type u_1} (x : option α) :
(none <|> x) = x

@[simp]
theorem option.orelse_none' {α : Type u_1} (x : option α) :

@[simp]
theorem option.orelse_none {α : Type u_1} (x : option α) :
(x <|> none) = x

@[simp]
theorem option.is_some_none {α : Type u_1} :

@[simp]
theorem option.is_some_some {α : Type u_1} {a : α} :

theorem option.is_some_iff_exists {α : Type u_1} {x : option α} :
(x.is_some) ∃ (a : α), x = some a

@[simp]
theorem option.is_none_none {α : Type u_1} :

@[simp]
theorem option.is_none_some {α : Type u_1} {a : α} :

@[simp]
theorem option.not_is_some {α : Type u_1} {a : option α} :

theorem option.eq_some_iff_get_eq {α : Type u_1} {o : option α} {a : α} :
o = some a ∃ (h : (o.is_some)), option.get h = a

theorem option.not_is_some_iff_eq_none {α : Type u_1} {o : option α} :

theorem option.ne_none_iff_is_some {α : Type u_1} {o : option α} :

theorem option.ne_none_iff_exists {α : Type u_1} {o : option α} :
o none ∃ (x : α), some x = o

theorem option.ne_none_iff_exists' {α : Type u_1} {o : option α} :
o none ∃ (x : α), o = some x

theorem option.bex_ne_none {α : Type u_1} {p : option α → Prop} :
(∃ (x : option α) (H : x none), p x) ∃ (x : α), p (some x)

theorem option.ball_ne_none {α : Type u_1} {p : option α → Prop} :
(∀ (x : option α), x nonep x) ∀ (x : α), p (some x)

theorem option.iget_mem {α : Type u_1} [inhabited α] {o : option α} :
(o.is_some) → o.iget o

theorem option.iget_of_mem {α : Type u_1} [inhabited α] {a : α} {o : option α} :
a oo.iget = a

@[simp]
theorem option.guard_eq_some {α : Type u_1} {p : α → Prop} [decidable_pred p] {a b : α} :
option.guard p a = some b a = b p a

@[simp]
theorem option.guard_eq_some' {p : Prop} [decidable p] (u : unit) :
guard p = some u p

theorem option.lift_or_get_choice {α : Type u_1} {f : α → α → α} (h : ∀ (a b : α), f a b = a f a b = b) (o₁ o₂ : option α) :
option.lift_or_get f o₁ o₂ = o₁ option.lift_or_get f o₁ o₂ = o₂

@[simp]
theorem option.lift_or_get_none_left {α : Type u_1} {f : α → α → α} {b : option α} :

@[simp]
theorem option.lift_or_get_none_right {α : Type u_1} {f : α → α → α} {a : option α} :

@[simp]
theorem option.lift_or_get_some_some {α : Type u_1} {f : α → α → α} {a b : α} :
option.lift_or_get f (some a) (some b) = (f a b)

def option.cases_on' {α : Type u_1} {β : Type u_2} :
option αβ → (α → β) → β

given an element of a : option α, a default element b : β and a function α → β, apply this function to a if it comes from α, and return b otherwise.

Equations
@[simp]
theorem option.cases_on'_none {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) :

@[simp]
theorem option.cases_on'_some {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) (a : α) :
(some a).cases_on' x f = f a

@[simp]
theorem option.cases_on'_coe {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) (a : α) :
a.cases_on' x f = f a

@[simp]
theorem option.cases_on'_none_coe {α : Type u_1} {β : Type u_2} (f : option α → β) (o : option α) :
o.cases_on' (f none) (f coe) = f o