Init.Data.Option.Lemmas

theorem Option.pbind_congr {α : Type u_1} {β : Type u_2} {o o' : Option α} (ho : o = o') {f : (a : α) → o = some a → Option β} {g : (a : α) → o' = some a → Option β} (hf : ∀ (a : α) (h : o' = some a), 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 : α) → o = some a → Option β} :

o.pbind f = none ↔ o = none ∨ ∃ (a : α), ∃ (h : o = some a), f a h = none

source

theorem Option.isSome_pbind_iff {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} :

(o.pbind f).isSome = true ↔ ∃ (a : α), ∃ (h : o = some a), (f a h).isSome = true

source

@[deprecated "isSome_pbind_iff" (since := "2025-04-01")]

theorem Option.pbind_isSome {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} :

((o.pbind f).isSome = true) = ∃ (a : α), ∃ (h : o = some a), (f a h).isSome = true

source

theorem Option.pbind_eq_some_iff {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} {b : β} :

o.pbind f = some b ↔ ∃ (a : α), ∃ (h : o = some a), 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 : α), none = some a → 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 : α), some a = some a_1 → 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 : α), o = some a → p a} :

pmap f o h = none ↔ o = none

source

@[simp]

theorem Option.isSome_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} :

(pmap f o h).isSome = o.isSome

source

@[simp]

theorem Option.isNone_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} :

(pmap f o h).isNone = o.isNone

source

@[reducible, inline, deprecated Option.isSome_pmap (since := "2025-04-01")]

abbrev Option.pmap_isSome {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o : Option α} {h : ∀ (a : α), o = some a → p a} :

(pmap f o h).isSome = o.isSome

Equations

@Option.pmap_isSome = @Option.isSome_pmap

Instances For

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 : α), o = some a → 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 : α), o = some a → 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 : α), o = some a → 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 : β), Option.map f o = some a → p a) :

pmap g (Option.map f o) H = pmap (fun (a : α) (h : p (f a)) => g (f a) h) o ⋯

source

theorem Option.pmap_or {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {o o' : Option α} {h : ∀ (a : α), o.or o' = some a → p a} :

pmap f (o.or o') h = match o, h with | none, h => pmap f o' ⋯ | some a, h => some (f a ⋯)

source

theorem Option.pmap_pred_congr {α : Type u} {p p' : α → Prop} (hp : ∀ (x : α), p x ↔ p' x) {o o' : Option α} (ho : o = o') (h : ∀ (x : α), o = some x → p x) (x : α) :

o' = some x → p' x

source

theorem Option.pmap_congr {α : Type u} {β : Type v} {p p' : α → Prop} (hp : ∀ (x : α), p x ↔ p' x) {f : (x : α) → p x → β} {f' : (x : α) → p' x → β} (hf : ∀ (x : α) (h : p' x), f x ⋯ = f' x h) {o o' : Option α} (ho : o = o') {h : ∀ (x : α), o = some x → p x} :

pmap f o h = pmap f' o' ⋯

pelim #

source

@[simp]

theorem Option.pelim_none {α✝ : Sort u_1} {b : α✝} {α✝¹ : Type u_2} {f : (a : α✝¹) → none = some a → α✝} :

none.pelim b f = b

source

@[simp]

theorem Option.pelim_some {α✝ : Type u_1} {a : α✝} {α✝¹ : Sort u_2} {b : α✝¹} {f : (a_1 : α✝) → some a = some a_1 → α✝¹} :

(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 : o = some a) => 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 : α), o = some a → p a) (g : γ) (g' : β → γ) :

(pmap f o H).elim g g' = o.pelim g fun (a : α) (h : o = some a) => g' (f a ⋯)

pfilter #

source

theorem Option.pfilter_congr {α : Type u} {o o' : Option α} (ho : o = o') {f : (a : α) → o = some a → Bool} {g : (a : α) → o' = some a → Bool} (hf : ∀ (a : α) (ha : o' = some a), f a ⋯ = g a ha) :

o.pfilter f = o'.pfilter g

source

@[simp]

theorem Option.pfilter_none {α : Type u_1} {p : (a : α) → none = some a → Bool} :

none.pfilter p = none

source

@[simp]

theorem Option.pfilter_some {α : Type u_1} {x : α} {p : (a : α) → some x = some a → Bool} :

(some x).pfilter p = if p x ⋯ = true then some x else none

source

theorem Option.isSome_pfilter_iff {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} :

(o.pfilter p).isSome = true ↔ ∃ (a : α), ∃ (ha : o = some a), p a ha = true

source

theorem Option.isSome_pfilter_iff_get {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} :

(o.pfilter p).isSome = true ↔ ∃ (h : o.isSome = true ), p (o.get h) ⋯ = true

source

theorem Option.isSome_of_isSome_pfilter {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} (h : (o.pfilter p).isSome = true) :

o.isSome = true

source

@[simp]

theorem Option.get_pfilter {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} (h : (o.pfilter p).isSome = true) :

(o.pfilter p).get h = o.get ⋯

source

theorem Option.pfilter_eq_none_iff {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} :

o.pfilter p = none ↔ o = none ∨ ∃ (a : α), ∃ (ha : o = some a), p a ha = false

source

theorem Option.pfilter_eq_some_iff {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} {a : α} :

o.pfilter p = some a ↔ ∃ (ha : o = some a), p a ha = true

source

@[simp]

theorem Option.pfilter_eq_filter {α : Type u_1} {o : Option α} {p : α → Bool} :

(o.pfilter fun (a : α) (x : o = some a) => p a) = Option.filter p o

source

theorem Option.pfilter_eq_pbind_ite {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} :

o.pfilter p = o.pbind fun (a : α) (h : o = some a) => if p a h = true then some a else none

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