Documentation

Init.Data.Option.Lemmas

source
theorem Option.mem_iff {α : Type u_1} {a : α} {b : Option α} :
a ∈ b ↔ b = some a
source
theorem Option.mem_some {α : Type u_1} {a b : α} :
a ∈ some b ↔ b = a
source
theorem Option.mem_some_self {α : Type u_1} (a : α) :
a ∈ some a
source
theorem Option.some_ne_none {α : Type u_1} (x : α) :
some x ≠ none
source
theorem Option.forall {α : Type u_1} {p : Option α → Prop} :
(∀ (x : Option α), p x) ↔ p none ∧ ∀ (x : α), p (some x)
source
theorem Option.exists {α : Type u_1} {p : Option α → Prop} :
(∃ (x : Option α), p x) ↔ p none ∨ ∃ (x : α), p (some x)
source
theorem Option.get_mem {α : Type u_1} {o : Option α} (h : o.isSome = true) :
o.get h ∈ o
source
theorem Option.get_of_mem {α : Type u_1} {a : α} {o : Option α} (h : o.isSome = true) :
a ∈ o → o.get h = a
source
@[simp]
theorem Option.not_mem_none {α : Type u_1} (a : α) :
¬a ∈ none
source
theorem Option.getD_of_ne_none {α : Type u_1} {x : Option α} (hx : x ≠ none) (y : α) :
some (x.getD y) = x
source
theorem Option.getD_eq_iff {α : Type u_1} {o : Option α} {a b : α} :
o.getD a = b ↔ o = some b ∨ o = none ∧ a = b
source
@[simp]
theorem Option.get!_none {α : Type u_1} [Inhabited α] :
none.get! = default
source
@[simp]
theorem Option.get!_some {α : Type u_1} [Inhabited α] {a : α} :
(some a).get! = a
source
theorem Option.get_eq_get! {α : Type u_1} [Inhabited α] (o : Option α) {h : o.isSome = true} :
o.get h = o.get!
source
theorem Option.get_eq_getD {α : Type u_1} {fallback : α} (o : Option α) {h : o.isSome = true} :
o.get h = o.getD fallback
source
theorem Option.some_get! {α : Type u_1} [Inhabited α] (o : Option α) :
o.isSome = true → some o.get! = o
source
theorem Option.get!_eq_getD {α : Type u_1} [Inhabited α] (o : Option α) :
o.get! = o.getD default
source
@[reducible, inline, deprecated Option.get!_eq_getD (since := "2024-11-18")]
abbrev Option.get!_eq_getD_default {α : Type u_1} [Inhabited α] (o : Option α) :
o.get! = o.getD default
Equations
source
theorem Option.mem_unique {α : Type u_1} {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) :
a = b
source
theorem Option.ext {α : Type u_1} {o₁ o₂ : Option α} :
(∀ (a : α), a ∈ o₁ ↔ a ∈ o₂) → o₁ = o₂
source
theorem Option.ext_iff {α : Type u_1} {o₁ o₂ : Option α} :
o₁ = o₂ ↔ ∀ (a : α), a ∈ o₁ ↔ a ∈ o₂
source
theorem Option.eq_none_iff_forall_not_mem {α✝ : Type u_1} {o : Option α✝} :
o = none ↔ ∀ (a : α✝), ¬a ∈ o
source
theorem Option.isSome_iff_exists {α✝ : Type u_1} {x : Option α✝} :
x.isSome = true ↔ ∃ (a : α✝), x = some a
source
theorem Option.isSome_eq_isSome {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {y : Option α✝¹} :
x.isSome = y.isSome ↔ (x = none ↔ y = none)
source
@[simp]
theorem Option.not_isSome {α✝ : Type u_1} {a : Option α✝} :
a.isSome = false ↔ a.isNone = true
source
theorem Option.eq_some_iff_get_eq {α✝ : Type u_1} {o : Option α✝} {a : α✝} :
o = some a ↔ ∃ (h : o.isSome = true), o.get h = a
source
theorem Option.eq_some_of_isSome {α : Type u_1} {o : Option α} (h : o.isSome = true) :
o = some (o.get h)
source
theorem Option.isSome_iff_ne_none {α✝ : Type u_1} {o : Option α✝} :
o.isSome = true ↔ o ≠ none
source
theorem Option.not_isSome_iff_eq_none {α✝ : Type u_1} {o : Option α✝} :
¬o.isSome = true ↔ o = none
source
theorem Option.ne_none_iff_isSome {α✝ : Type u_1} {o : Option α✝} :
o ≠ none ↔ o.isSome = true
source
theorem Option.ne_none_iff_exists {α✝ : Type u_1} {o : Option α✝} :
o ≠ none ↔ ∃ (x : α✝), some x = o
source
theorem Option.ne_none_iff_exists' {α✝ : Type u_1} {o : Option α✝} :
o ≠ none ↔ ∃ (x : α✝), o = some x
source
theorem Option.bex_ne_none {α : Type u_1} {p : Option α → Prop} :
(∃ (x : Option α), ∃ (x_1 : x ≠ none), p x) ↔ ∃ (x : α), p (some x)
source
theorem Option.ball_ne_none {α : Type u_1} {p : Option α → Prop} :
(∀ (x : Option α), x ≠ none → p x) ↔ ∀ (x : α), p (some x)
source
@[simp]
theorem Option.pure_def {α : Type u_1} :
pure = some
source
@[simp]
theorem Option.bind_eq_bind {α β : Type u_1} :
bind = Option.bind
source
@[simp]
theorem Option.bind_some {α : Type u_1} (x : Option α) :
x.bind some = x
source
@[simp]
theorem Option.bind_none {α : Type u_1} {β : Type u_2} (x : Option α) :
(x.bind fun (x : α) => none) = none
source
theorem Option.bind_eq_some {α✝ : Type u_1} {b : α✝} {α✝¹ : Type u_2} {x : Option α✝¹} {f : α✝¹ → Option α✝} :
x.bind f = some b ↔ ∃ (a : α✝¹), x = some a ∧ f a = some b
source
@[simp]
theorem Option.bind_eq_none {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β} :
o.bind f = none ↔ ∀ (a : α), o = some a → f a = none
source
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
source
theorem Option.mem_bind_iff {α : Type u_1} {β : Type u_2} {b : β} {o : Option α} {f : α → Option β} :
b ∈ o.bind f ↔ ∃ (a : α), a ∈ o ∧ b ∈ f a
source
theorem Option.bind_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → Option γ} (a : Option α) (b : Option β) :
(a.bind fun (x : α) => b.bind (f x)) = b.bind fun (y : β) => a.bind fun (x : α) => f x y
source
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 fun (y : α) => (f y).bind g
source
theorem Option.bind_congr {α : Type u_1} {β : Type u_2} {o : Option α} {f g : α → Option β} (h : ∀ (a : α), o = some a → f a = g a) :
o.bind f = o.bind g
source
theorem Option.join_eq_some {α✝ : Type u_1} {a : α✝} {x : Option (Option α✝)} :
x.join = some a ↔ x = some (some a)
source
theorem Option.join_ne_none {α✝ : Type u_1} {x : Option (Option α✝)} :
x.join ≠ none ↔ ∃ (z : α✝), x = some (some z)
source
theorem Option.join_ne_none' {α✝ : Type u_1} {x : Option (Option α✝)} :
¬x.join = none ↔ ∃ (z : α✝), x = some (some z)
source
theorem Option.join_eq_none {α✝ : Type u_1} {o : Option (Option α✝)} :
o.join = none ↔ o = none ∨ o = some none
source
theorem Option.bind_id_eq_join {α : Type u_1} {x : Option (Option α)} :
x.bind id = x.join
source
@[simp]
theorem Option.map_eq_map {α✝ α✝¹ : Type u_1} {f : α✝ → α✝¹} :
Functor.map f = Option.map f
source
theorem Option.map_none {α✝ α✝¹ : Type u_1} {f : α✝ → α✝¹} :
f <$> none = none
source
theorem Option.map_some {α✝ α✝¹ : Type u_1} {f : α✝ → α✝¹} {a : α✝} :
f <$> some a = some (f a)
source
@[simp]
theorem Option.map_eq_some' {α✝ : Type u_1} {b : α✝} {α✝¹ : Type u_2} {x : Option α✝¹} {f : α✝¹ → α✝} :
Option.map f x = some b ↔ ∃ (a : α✝¹), x = some a ∧ f a = b
source
theorem Option.map_eq_some {α✝ α✝¹ : Type u_1} {f : α✝ → α✝¹} {x : Option α✝} {b : α✝¹} :
f <$> x = some b ↔ ∃ (a : α✝), x = some a ∧ f a = b
source
@[simp]
theorem Option.map_eq_none' {α✝ : Type u_1} {x : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} :
Option.map f x = none ↔ x = none
source
theorem Option.isSome_map {α α✝ : Type u_1} {f : α → α✝} {x : Option α} :
(f <$> x).isSome = x.isSome
source
@[simp]
theorem Option.isSome_map' {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} :
(Option.map f x).isSome = x.isSome
source
@[simp]
theorem Option.isNone_map' {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} :
(Option.map f x).isNone = x.isNone
source
theorem Option.map_eq_none {α✝ α✝¹ : Type u_1} {f : α✝ → α✝¹} {x : Option α✝} :
f <$> x = none ↔ x = none
source
theorem Option.map_eq_bind {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x : Option α} :
Option.map f x = x.bind (some ∘ f)
source
theorem Option.map_congr {α : Type u_1} {α✝ : Type u_2} {f g : α → α✝} {x : Option α} (h : ∀ (a : α), a ∈ x → f a = g a) :
Option.map f x = Option.map g x
source
@[simp]
theorem Option.map_id_fun {α : Type u} :
Option.map id = id
source
theorem Option.map_id' {α : Type u_1} {x : Option α} :
Option.map (fun (a : α) => a) x = x
source
@[simp]
theorem Option.map_id_fun' {α : Type u} :
(Option.map fun (a : α) => a) = id
source
theorem Option.get_map {α : Type u_1} {β : Type u_2} {f : α → β} {o : Option α} {h : (Option.map f o).isSome = true} :
(Option.map f o).get h = f (o.get ⋯)
source
@[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
source
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)
source
@[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)
source
theorem Option.mem_map_of_mem {α : Type u_1} {β : Type u_2} {x : Option α} {a : α} (g : α → β) (h : a ∈ x) :
g a ∈ Option.map g x
source
theorem Option.map_inj_right {α : Type u_1} {β : Type u_2} {f : α → β} {o o' : Option α} (w : ∀ (x y : α), f x = f y → x = y) :
Option.map f o = Option.map f o' ↔ o = o'
source
@[simp]
theorem Option.map_if {α : Type u_1} {β : Type u_2} {c : Prop} {a : α} {f : α → β} [Decidable c] :
Option.map f (if c then some a else none) = if c then some (f a) else none
source
@[simp]
theorem Option.map_dif {α : Type u_1} {β : Type u_2} {c : Prop} {f : α → β} [Decidable c] {a : c → α} :
Option.map f (if h : c then some (a h) else none) = if h : c then some (f (a h)) else none
source
@[simp]
theorem Option.filter_none {α : Type u_1} (p : α → Bool) :
Option.filter p none = none
source
theorem Option.filter_some {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} :
Option.filter p (some a) = if p a = true then some a else none
source
theorem Option.isSome_of_isSome_filter {α : Type u_1} (p : α → Bool) (o : Option α) (h : (Option.filter p o).isSome = true) :
o.isSome = true
source
@[reducible, inline, deprecated Option.isSome_of_isSome_filter (since := "2025-03-18")]
abbrev Option.isSome_filter_of_isSome {α : Type u_1} (p : α → Bool) (o : Option α) (h : (Option.filter p o).isSome = true) :
o.isSome = true
Equations
source
@[simp]
theorem Option.filter_eq_none {α : Type u_1} {o : Option α} {p : α → Bool} :
Option.filter p o = none ↔ o = none ∨ ∀ (a : α), a ∈ o → ¬p a = true
source
@[simp]
theorem Option.filter_eq_some {α : Type u_1} {a : α} {o : Option α} {p : α → Bool} :
Option.filter p o = some a ↔ a ∈ o ∧ p a = true
source
theorem Option.mem_filter_iff {α : Type u_1} {p : α → Bool} {a : α} {o : Option α} :
a ∈ Option.filter p o ↔ a ∈ o ∧ p a = true
source
@[simp]
theorem Option.all_guard {α : Type u_1} {q : α → Bool} (p : α → Prop) [DecidablePred p] (a : α) :
Option.all q (guard p a) = (!decide (p a) || q a)
source
@[simp]
theorem Option.any_guard {α : Type u_1} {q : α → Bool} (p : α → Prop) [DecidablePred p] (a : α) :
Option.any q (guard p a) = (decide (p a) && q a)
source
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
source
theorem Option.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Option γ} {x : Option α} :
(Option.map f x).bind g = x.bind (g ∘ f)
source
@[simp]
theorem Option.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {x : Option α} :
Option.map g (x.bind f) = x.bind (Option.map g ∘ f)
source
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
source
theorem Option.join_join {α : Type u_1} {x : Option (Option (Option α))} :
x.join.join = (Option.map join x).join
source
theorem Option.mem_of_mem_join {α : Type u_1} {a : α} {x : Option (Option α)} (h : a ∈ x.join) :
some a ∈ x
source
@[simp]
theorem Option.some_orElse {α : Type u_1} (a : α) (x : Option α) :
(some a <|> x) = some a
source
@[simp]
theorem Option.none_orElse {α : Type u_1} (x : Option α) :
(none <|> x) = x
source
@[simp]
theorem Option.orElse_none {α : Type u_1} (x : Option α) :
(x <|> none) = x
source
theorem Option.map_orElse {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {x y : Option α} :
Option.map f (x <|> y) = (Option.map f x <|> Option.map f y)
source
@[simp]
theorem Option.guard_eq_some {α✝ : Type u_1} {p : α✝ → Prop} {a b : α✝} [DecidablePred p] :
guard p a = some b ↔ a = b ∧ p a
source
@[simp]
theorem Option.isSome_guard {α✝ : Type u_1} {p : α✝ → Prop} {a : α✝} [DecidablePred p] :
(guard p a).isSome = true ↔ p a
source
@[reducible, inline, deprecated Option.isSome_guard (since := "2025-03-18")]
abbrev Option.guard_isSome {α✝ : Type u_1} {p : α✝ → Prop} {a : α✝} [DecidablePred p] :
(guard p a).isSome = true ↔ p a
Equations
source
@[simp]
theorem Option.guard_eq_none {α✝ : Type u_1} {p : α✝ → Prop} {a : α✝} [DecidablePred p] :
guard p a = none ↔ ¬p a
source
@[simp]
theorem Option.guard_pos {α✝ : Type u_1} {p : α✝ → Prop} {a : α✝} [DecidablePred p] (h : p a) :
guard p a = some a
source
theorem Option.guard_congr {α : Type u_1} {f g : α → Prop} [DecidablePred f] [DecidablePred g] (h : ∀ (a : α), f a ↔ g a) :
guard f = guard g
source
@[simp]
theorem Option.guard_false {α : Type u_1} :
(guard fun (x : α) => False) = fun (x : α) => none
source
@[simp]
theorem Option.guard_true {α : Type u_1} :
(guard fun (x : α) => True) = some
source
theorem Option.guard_comp {α : Type u_1} {β : Type u_2} {p : α → Prop} [DecidablePred p] {f : β → α} :
guard p ∘ f = Option.map f ∘ guard (p ∘ f)
source
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₁ ∨ liftOrGet f o₁ o₂ = o₂
source
@[simp]
theorem Option.liftOrGet_none_left {α : Type u_1} {f : α → α → α} {b : Option α} :
liftOrGet f none b = b
source
@[simp]
theorem Option.liftOrGet_none_right {α : Type u_1} {f : α → α → α} {a : Option α} :
liftOrGet f a none = a
source
@[simp]
theorem Option.liftOrGet_some_some {α : Type u_1} {f : α → α → α} {a b : α} :
liftOrGet f (some a) (some b) = some (f a b)
source
@[simp]
theorem Option.elim_none {β : Sort u_1} {α : Type u_2} (x : β) (f : α → β) :
none.elim x f = x
source
@[simp]
theorem Option.elim_some {β : Sort u_1} {α : Type u_2} (x : β) (f : α → β) (a : α) :
(some a).elim x f = f a
source
@[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)
source
noncomputable def Option.choice (α : Type u_1) :
Option α

An optional arbitrary element of a given type.

If α is non-empty, then there exists some v : α and this arbitrary element is some v. Otherwise, it is none.

Equations
source
theorem Option.choice_eq {α : Type u_1} [Subsingleton α] (a : α) :
choice α = some a
source
theorem Option.isSome_choice_iff_nonempty {α : Type u_1} :
(choice α).isSome = true ↔ Nonempty α
source
@[reducible, inline, deprecated Option.isSome_choice_iff_nonempty (since := "2025-03-18")]
abbrev Option.choice_isSome_iff_nonempty {α : Type u_1} :
(choice α).isSome = true ↔ Nonempty α
Equations
source
@[simp]
theorem Option.toList_some {α : Type u_1} (a : α) :
(some a).toList = [a]
source
@[simp]
theorem Option.toList_none (α : Type u_1) :
none.toList = []
source
@[simp]
theorem Option.some_or {α✝ : Type u_1} {a : α✝} {o : Option α✝} :
(some a).or o = some a
source
@[simp]
theorem Option.none_or {α✝ : Type u_1} {o : Option α✝} :
none.or o = o
source
theorem Option.or_eq_right_of_none {α : Type u_1} {o o' : Option α} (h : o = none) :
o.or o' = o'
source
@[deprecated Option.some_or (since := "2024-11-03")]
theorem Option.or_some {α✝ : Type u_1} {a : α✝} {o : Option α✝} :
(some a).or o = some a
source
@[simp]
theorem Option.or_some' {α : Type u_1} {a : α} {o : Option α} :
o.or (some a) = some (o.getD a)

This will be renamed to or_some once the existing deprecated lemma is removed.

source
theorem Option.or_eq_bif {α✝ : Type u_1} {o o' : Option α✝} :
o.or o' = bif o.isSome then o else o'
source
@[simp]
theorem Option.isSome_or {α✝ : Type u_1} {o o' : Option α✝} :
(o.or o').isSome = (o.isSome || o'.isSome)
source
@[simp]
theorem Option.isNone_or {α✝ : Type u_1} {o o' : Option α✝} :
(o.or o').isNone = (o.isNone && o'.isNone)
source
@[simp]
theorem Option.or_eq_none {α✝ : Type u_1} {o o' : Option α✝} :
o.or o' = none ↔ o = none ∧ o' = none
source
@[simp]
theorem Option.or_eq_some {α✝ : Type u_1} {o o' : Option α✝} {a : α✝} :
o.or o' = some a ↔ o = some a ∨ o = none ∧ o' = some a
source
theorem Option.or_assoc {α✝ : Type u_1} {o₁ o₂ o₃ : Option α✝} :
(o₁.or o₂).or o₃ = o₁.or (o₂.or o₃)
source
instance Option.instAssociativeOr {α : Type u_1} :
Std.Associative or
source
@[simp]
theorem Option.or_none {α✝ : Type u_1} {o : Option α✝} :
o.or none = o
source
theorem Option.or_eq_left_of_none {α : Type u_1} {o o' : Option α} (h : o' = none) :
o.or o' = o
source
instance Option.instLawfulIdentityOrNone {α : Type u_1} :
Std.LawfulIdentity or none
source
@[simp]
theorem Option.or_self {α✝ : Type u_1} {o : Option α✝} :
o.or o = o
source
instance Option.instIdempotentOpOr {α : Type u_1} :
Std.IdempotentOp or
source
theorem Option.or_eq_orElse {α✝ : Type u_1} {o o' : Option α✝} :
o.or o' = o.orElse fun (x : Unit) => o'
source
theorem Option.map_or {α✝ α✝¹ : Type u_1} {f : α✝ → α✝¹} {o o' : Option α✝} :
f <$> o.or o' = (f <$> o).or (f <$> o')
source
theorem Option.map_or' {α✝ : Type u_1} {o o' : Option α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} :
Option.map f (o.or o') = (Option.map f o).or (Option.map f o')
source
theorem Option.or_of_isSome {α : Type u_1} {o o' : Option α} (h : o.isSome = true) :
o.or o' = o
source
theorem Option.or_of_isNone {α : Type u_1} {o o' : Option α} (h : o.isNone = true) :
o.or o' = o'

beq #

source
@[simp]
theorem Option.none_beq_none {α : Type u_1} [BEq α] :
(none == none) = true
source
@[simp]
theorem Option.none_beq_some {α : Type u_1} [BEq α] (a : α) :
(none == some a) = false
source
@[simp]
theorem Option.some_beq_none {α : Type u_1} [BEq α] (a : α) :
(some a == none) = false
source
@[simp]
theorem Option.some_beq_some {α : Type u_1} [BEq α] {a b : α} :
(some a == some b) = (a == b)
source
@[simp]
theorem Option.reflBEq_iff {α : Type u_1} [BEq α] :
ReflBEq (Option α) ↔ ReflBEq α
source
@[simp]
theorem Option.lawfulBEq_iff {α : Type u_1} [BEq α] :
LawfulBEq (Option α) ↔ LawfulBEq α

ite #

source
@[simp]
theorem Option.dite_none_left_eq_some {β : Type u_1} {a : β} {p : Prop} [Decidable p] {b : ¬p → Option β} :
(if h : p then none else b h) = some a ↔ ∃ (h : ¬p), b h = some a
source
@[simp]
theorem Option.dite_none_right_eq_some {α : Type u_1} {a : α} {p : Prop} [Decidable p] {b : p → Option α} :
(if h : p then b h else none) = some a ↔ ∃ (h : p), b h = some a
source
@[simp]
theorem Option.some_eq_dite_none_left {β : Type u_1} {a : β} {p : Prop} [Decidable p] {b : ¬p → Option β} :
(some a = if h : p then none else b h) ↔ ∃ (h : ¬p), some a = b h
source
@[simp]
theorem Option.some_eq_dite_none_right {α : Type u_1} {a : α} {p : Prop} [Decidable p] {b : p → Option α} :
(some a = if h : p then b h else none) ↔ ∃ (h : p), some a = b h
source
@[simp]
theorem Option.ite_none_left_eq_some {β : Type u_1} {a : β} {p : Prop} [Decidable p] {b : Option β} :
(if p then none else b) = some a ↔ ¬p ∧ b = some a
source
@[simp]
theorem Option.ite_none_right_eq_some {α : Type u_1} {a : α} {p : Prop} [Decidable p] {b : Option α} :
(if p then b else none) = some a ↔ p ∧ b = some a
source
@[simp]
theorem Option.some_eq_ite_none_left {β : Type u_1} {a : β} {p : Prop} [Decidable p] {b : Option β} :
(some a = if p then none else b) ↔ ¬p ∧ some a = b
source
@[simp]
theorem Option.some_eq_ite_none_right {α : Type u_1} {a : α} {p : Prop} [Decidable p] {b : Option α} :
(some a = if p then b else none) ↔ p ∧ some a = b
source
theorem Option.mem_dite_none_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : ¬p → Option α} :
(x ∈ if h : p then none else l h) ↔ ∃ (h : ¬p), x ∈ l h
source
theorem Option.mem_dite_none_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : p → Option α} :
(x ∈ if h : p then l h else none) ↔ ∃ (h : p), x ∈ l h
source
theorem Option.mem_ite_none_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : Option α} :
(x ∈ if p then none else l) ↔ ¬p ∧ x ∈ l
source
theorem Option.mem_ite_none_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : Option α} :
(x ∈ if p then l else none) ↔ p ∧ x ∈ l
source
@[simp]
theorem Option.isSome_dite {β : Type u_1} {p : Prop} [Decidable p] {b : p → β} :
(if h : p then some (b h) else none).isSome = true ↔ p
source
@[simp]
theorem Option.isSome_ite {α✝ : Type u_1} {b : α✝} {p : Prop} [Decidable p] :
(if p then some b else none).isSome = true ↔ p
source
@[simp]
theorem Option.isSome_dite' {β : Type u_1} {p : Prop} [Decidable p] {b : ¬p → β} :
(if h : p then none else some (b h)).isSome = true ↔ ¬p
source
@[simp]
theorem Option.isSome_ite' {α✝ : Type u_1} {b : α✝} {p : Prop} [Decidable p] :
(if p then none else some b).isSome = true ↔ ¬p
source
@[simp]
theorem Option.get_dite {β : Type u_1} {p : Prop} [Decidable p] (b : p → β) (w : (if h : p then some (b h) else none).isSome = true) :
(if h : p then some (b h) else none).get w = b ⋯
source
@[simp]
theorem Option.get_ite {α✝ : Type u_1} {b : α✝} {p : Prop} [Decidable p] (h : (if p then some b else none).isSome = true) :
(if p then some b else none).get h = b
source
@[simp]
theorem Option.get_dite' {β : Type u_1} {p : Prop} [Decidable p] (b : ¬p → β) (w : (if h : p then none else some (b h)).isSome = true) :
(if h : p then none else some (b h)).get w = b ⋯
source
@[simp]
theorem Option.get_ite' {α✝ : Type u_1} {b : α✝} {p : Prop} [Decidable p] (h : (if p then none else some b).isSome = true) :
(if p then none else some b).get h = b

pbind #

source
@[simp]
theorem Option.pbind_none {α✝ : Type u_1} {α✝¹ : Type u_2} {f : (a : α✝) → a ∈ none → Option α✝¹} :
none.pbind f = none
source
@[simp]
theorem Option.pbind_some {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : (a_1 : α✝) → a_1 ∈ some a → Option α✝¹} :
(some a).pbind f = f a ⋯
source
@[simp]
theorem Option.map_pbind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {o : Option α} {f : (a : α) → a ∈ o → Option β} {g : β → γ} :
Option.map g (o.pbind f) = o.pbind fun (a : α) (h : a ∈ o) => Option.map g (f a h)
source
theorem Option.pbind_congr {α : Type u_1} {β : Type u_2} {o o' : Option α} (ho : o = o') {f : (a : α) → a ∈ o → Option β} {g : (a : α) → a ∈ o' → Option β} (hf : ∀ (a : α) (h : a ∈ o'), f a ⋯ = g a h) :
o.pbind f = o'.pbind g
source
theorem Option.pbind_eq_none_iff {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → a ∈ o → Option β} :
o.pbind f = none ↔ o = none ∨ ∃ (a : α), ∃ (h : a ∈ o), f a h = none
source
theorem Option.pbind_isSome {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → a ∈ o → Option β} :
((o.pbind f).isSome = true) = ∃ (a : α), ∃ (h : a ∈ o), (f a h).isSome = true
source
theorem Option.pbind_eq_some_iff {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → a ∈ o → Option β} {b : β} :
o.pbind f = some b ↔ ∃ (a : α), ∃ (h : a ∈ o), f a h = some b

pmap #

source
@[simp]
theorem Option.pmap_none {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), a ∈ none → p a} :
pmap f none h = none
source
@[simp]
theorem Option.pmap_some {α : Type u_1} {β : Type u_2} {a : α} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a_1 : α), a_1 ∈ some a → p a_1} :
pmap f (some a) h = some (f a ⋯)
source
@[simp]
theorem Option.pmap_eq_none_iff {α : Type u_1} {β : Type u_2} {o : Option α} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), a ∈ o → p a} :
pmap f o h = none ↔ o = none
source
@[simp]
theorem Option.pmap_isSome {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), a ∈ o → p a} :
(pmap f o h).isSome = o.isSome
source
@[simp]
theorem Option.pmap_eq_some_iff {α : Type u_1} {β : Type u_2} {b : β} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), a ∈ o → p a} :
pmap f o h = some b ↔ ∃ (a : α), ∃ (h : p a), o = some a ∧ b = f a h
source
@[simp]
theorem Option.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : α → β) (o : Option α) (H : ∀ (a : α), a ∈ o → p a) :
pmap (fun (a : α) (x : p a) => f a) o H = Option.map f o
source
theorem Option.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (o : Option α) (H : ∀ (a : α), a ∈ o → p a) :
Option.map g (pmap f o H) = pmap (fun (a : α) (h : p a) => g (f a h)) o H
source
theorem Option.pmap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (o : Option α) (f : α → β) {p : β → Prop} (g : (b : β) → p b → γ) (H : ∀ (a : β), a ∈ Option.map f o → p a) :
pmap g (Option.map f o) H = pmap (fun (a : α) (h : p (f a)) => g (f a) h) o ⋯

pelim #

source
@[simp]
theorem Option.pelim_none {α✝ : Sort u_1} {b : α✝} {α✝¹ : Type u_2} {f : (a : α✝¹) → a ∈ none → α✝} :
none.pelim b f = b
source
@[simp]
theorem Option.pelim_some {α✝ : Type u_1} {a : α✝} {α✝¹ : Sort u_2} {b : α✝¹} {f : (a_1 : α✝) → a_1 ∈ some a → α✝¹} :
(some a).pelim b f = f a ⋯
source
@[simp]
theorem Option.pelim_eq_elim {α✝ : Type u_1} {o : Option α✝} {α✝¹ : Sort u_2} {b : α✝¹} {f : α✝ → α✝¹} :
(o.pelim b fun (a : α✝) (x : a ∈ o) => f a) = o.elim b f
source
@[simp]
theorem Option.elim_pmap {α : Type u_1} {β : Type u_2} {γ : Sort u_3} {p : α → Prop} (f : (a : α) → p a → β) (o : Option α) (H : ∀ (a : α), a ∈ o → p a) (g : γ) (g' : β → γ) :
(pmap f o H).elim g g' = o.pelim g fun (a : α) (h : a ∈ o) => g' (f a ⋯)

LT and LE #

source
@[simp]
theorem Option.not_lt_none {α : Type u_1} [LT α] {a : Option α} :
¬a < none
source
@[simp]
theorem Option.none_lt_some {α : Type u_1} [LT α] {a : α} :
none < some a
source
@[simp]
theorem Option.some_lt_some {α : Type u_1} [LT α] {a b : α} :
some a < some b ↔ a < b
source
@[simp]
theorem Option.none_le {α : Type u_1} [LE α] {a : Option α} :
none ≤ a
source
@[simp]
theorem Option.not_some_le_none {α : Type u_1} [LE α] {a : α} :
¬some a ≤ none
source
@[simp]
theorem Option.some_le_some {α : Type u_1} [LE α] {a b : α} :
some a ≤ some b ↔ a ≤ b

min and max #

source
theorem Option.min_eq_left {α : Type u_1} [LE α] [Min α] (min_eq_left : ∀ (x y : α), x ≤ y → min x y = x) {a b : Option α} (h : a ≤ b) :
min a b = a
source
theorem Option.min_eq_right {α : Type u_1} [LE α] [Min α] (min_eq_right : ∀ (x y : α), y ≤ x → min x y = y) {a b : Option α} (h : b ≤ a) :
min a b = b
source
theorem Option.min_eq_left_of_lt {α : Type u_1} [LT α] [Min α] (min_eq_left : ∀ (x y : α), x < y → min x y = x) {a b : Option α} (h : a < b) :
min a b = a
source
theorem Option.min_eq_right_of_lt {α : Type u_1} [LT α] [Min α] (min_eq_right : ∀ (x y : α), y < x → min x y = y) {a b : Option α} (h : b < a) :
min a b = b
source
theorem Option.min_eq_or {α : Type u_1} [LE α] [Min α] (min_eq_or : ∀ (x y : α), min x y = x ∨ min x y = y) {a b : Option α} :
min a b = a ∨ min a b = b
source
theorem Option.min_le_left {α : Type u_1} [LE α] [Min α] (min_le_left : ∀ (x y : α), min x y ≤ x) {a b : Option α} :
min a b ≤ a
source
theorem Option.min_le_right {α : Type u_1} [LE α] [Min α] (min_le_right : ∀ (x y : α), min x y ≤ y) {a b : Option α} :
min a b ≤ b
source
theorem Option.le_min {α : Type u_1} [LE α] [Min α] (le_min : ∀ (x y z : α), x ≤ min y z ↔ x ≤ y ∧ x ≤ z) {a b c : Option α} :
a ≤ min b c ↔ a ≤ b ∧ a ≤ c
source
theorem Option.max_eq_left {α : Type u_1} [LE α] [Max α] (max_eq_left : ∀ (x y : α), x ≤ y → max x y = y) {a b : Option α} (h : a ≤ b) :
max a b = b
source
theorem Option.max_eq_right {α : Type u_1} [LE α] [Max α] (max_eq_right : ∀ (x y : α), y ≤ x → max x y = x) {a b : Option α} (h : b ≤ a) :
max a b = a
source
theorem Option.max_eq_left_of_lt {α : Type u_1} [LT α] [Max α] (max_eq_left : ∀ (x y : α), x < y → max x y = y) {a b : Option α} (h : a < b) :
max a b = b
source
theorem Option.max_eq_right_of_lt {α : Type u_1} [LT α] [Max α] (max_eq_right : ∀ (x y : α), y < x → max x y = x) {a b : Option α} (h : b < a) :
max a b = a
source
theorem Option.max_eq_or {α : Type u_1} [LE α] [Max α] (max_eq_or : ∀ (x y : α), max x y = x ∨ max x y = y) {a b : Option α} :
max a b = a ∨ max a b = b
source
theorem Option.left_le_max {α : Type u_1} [LE α] [Max α] (le_refl : ∀ (x : α), x ≤ x) (left_le_max : ∀ (x y : α), x ≤ max x y) {a b : Option α} :
a ≤ max a b
source
theorem Option.right_le_max {α : Type u_1} [LE α] [Max α] (le_refl : ∀ (x : α), x ≤ x) (right_le_max : ∀ (x y : α), y ≤ max x y) {a b : Option α} :
b ≤ max a b
source
theorem Option.max_le {α : Type u_1} [LE α] [Max α] (max_le : ∀ (x y z : α), max x y ≤ z ↔ x ≤ z ∧ y ≤ z) {a b c : Option α} :
max a b ≤ c ↔ a ≤ c ∧ b ≤ c