mathlib documentation

data.option.basic

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

some x ≠ none

@[simp]

theorem option.get_mem {α : Type u_1} {o : option α} (h : ↥(o.is_some)) :

option.get h ∈ o

theorem option.get_of_mem {α : Type u_1} {a : α} {o : option α} (h : ↥(o.is_some)) (a_1 : a ∈ o) :

option.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)) :

some (option.get h) = x

@[simp]

theorem option.get_some {α : Type u_1} (x : α) (h : ↥((some x).is_some)) :

option.get h = x

@[simp]

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

(some x).get_or_else y = x

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

some (x.get_or_else y) = x

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

a = b

theorem option.some_injective (α : Type u_1) :

function.injective some

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

function.injective (option.map f)

option.map f is injective if f is injective.

@[ext]

theorem option.ext {α : Type u_1} {o₁ o₂ : option α} (a : ∀ (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 β) :

none >>= f = none

@[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 β) :

none.bind f = none

@[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 α) :

@[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 ∈ o → b ∉ f a

@[simp]

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

o >>= f = none ↔ ∀ (b : β) (a : α), a ∈ o → b ∉ 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)

@[simp]

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

f <$> none = none

@[simp]

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 : α → β} :

option.map f none = none

@[simp]

theorem option.map_some' {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} :

option.map f (some a) = some (f a)

@[simp]

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

@[simp]

theorem option.map_id' {α : Type u_1} :

option.map id = id

@[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 α) :

none.orelse x = x

@[simp]

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

(none <|> x) = x

@[simp]

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

x.orelse none = x

@[simp]

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

(x <|> none) = x

@[simp]

theorem option.is_some_none {α : Type u_1} :

none.is_some = ff

@[simp]

theorem option.is_some_some {α : Type u_1} {a : α} :

(some a).is_some = tt

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} :

none.is_none = tt

@[simp]

theorem option.is_none_some {α : Type u_1} {a : α} :

(some a).is_none = ff

@[simp]

theorem option.not_is_some {α : Type u_1} {a : option α} :

a.is_some = ff ↔ a.is_none = tt

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 α} :

¬↥(o.is_some) ↔ o = none

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

o ≠ none ↔ ↥(o.is_some)

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 ≠ none → p x) ↔ ∀ (x : α), p (some x)

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

theorem option.iget_of_mem {α : Type u_1} [inhabited α] {a : α} {o : option α} (a_1 : a ∈ o) :

o.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 α} :

option.lift_or_get f none b = b

@[simp]

theorem option.lift_or_get_none_right {α : Type u_1} {f : α → α → α} {a : option α} :

option.lift_or_get f a none = a

@[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} (a : option α) (a_1 : β) (a_2 : α → β) :

β

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

(some a).cases_on' n s = s a
none.cases_on' n s = n