Binary map of options

This file defines the binary map of Option. This is mostly useful to define pointwise operations on intervals.

Main declarations

• Option.map₂: Binary map of options.

Notes

This file is very similar to the n-ary section of Mathlib/Data/Set/Basic.lean, to Mathlib/Data/Finset/NAry.lean and to Mathlib/Order/Filter/NAry.lean. Please keep them in sync.

We do not define Option.map₃ as its only purpose so far would be to prove properties of Option.map₂ and casing already fulfills this task.

def Option.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Option α) (b : Option β) : Option γ

The image of a binary function f : α → β → γ as a function Option α → Option β → Option γ. Mathematically this should be thought of as the image of the corresponding function α × β → γ.

Equations

• Option.map₂ f a b = a.bind fun (a : α) => Option.map (f a) b

theorem Option.map₂_def {α β γ : Type u} (f : α → β → γ) (a : Option α) (b : Option β) : map₂ f a b = f <$> a <*> b

Option.map₂ in terms of monadic operations. Note that this can't be taken as the definition because of the lack of universe polymorphism.

@[simp]

theorem Option.map₂_some_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β) : map₂ f (some a) (some b) = some (f a b)

theorem Option.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β) : map₂ f (some a) (some b) = some (f a b)

@[simp]

theorem Option.map₂_none_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : Option β) : map₂ f none b = none

@[simp]

theorem Option.map₂_none_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Option α) : map₂ f a none = none

@[simp]

theorem Option.map₂_coe_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : Option β) : map₂ f (some a) b = Option.map (fun (b : β) => f a b) b

@[simp]

theorem Option.map₂_coe_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Option α) (b : β) : map₂ f a (some b) = Option.map (fun (a : α) => f a b) a

theorem Option.mem_map₂_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β} {c : γ} : c ∈ map₂ f a b ↔ ∃ (a' : α), ∃ (b' : β), a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

@[simp]

theorem Option.map₂_eq_some_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β} {c : γ} : map₂ f a b = some c ↔ ∃ (a' : α), ∃ (b' : β), a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

simp-normal form of mem_map₂_iff.

@[simp]

theorem Option.map₂_eq_none_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β} : map₂ f a b = none ↔ a = none ∨ b = none

theorem Option.map₂_swap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : Option α) (b : Option β) : map₂ f a b = map₂ (fun (a : β) (b : α) => f b a) b a

theorem Option.map_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} (f : α → β → γ) (g : γ → δ) : Option.map g (map₂ f a b) = map₂ (fun (a : α) (b : β) => g (f a b)) a b

theorem Option.map₂_map_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} (f : γ → β → δ) (g : α → γ) : map₂ f (Option.map g a) b = map₂ (fun (a : α) (b : β) => f (g a) b) a b

theorem Option.map₂_map_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} (f : α → γ → δ) (g : β → γ) : map₂ f a (Option.map g b) = map₂ (fun (a : α) (b : β) => f a (g b)) a b

@[simp]

theorem Option.map₂_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α × β → γ) (a : Option α) (b : Option β) : map₂ (Function.curry f) a b = Option.map f (map₂ Prod.mk a b)

@[simp]

theorem Option.map_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (x : Option (α × β)) : Option.map (Function.uncurry f) x = map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)

Algebraic replacement rules

A collection of lemmas to transfer associativity, commutativity, distributivity, ... of operations to the associativity, commutativity, distributivity, ... of Option.map₂ of those operations. The proof pattern is map₂_lemma operation_lemma. For example, map₂_comm mul_comm proves that map₂ (*) a b = map₂ (*) g f in a CommSemigroup.

theorem Option.map₂_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {c : Option γ} {ε : Type u_8} {ε' : Type u_9} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'} (h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) : map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c)

theorem Option.map₂_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β} {g : β → α → γ} (h_comm : ∀ (a : α) (b : β), f a b = g b a) : map₂ f a b = map₂ g b a

theorem Option.map₂_left_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {c : Option γ} {δ' : Type u_7} {ε : Type u_8} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε} (h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) : map₂ f a (map₂ g b c) = map₂ g' b (map₂ f' a c)

theorem Option.map₂_right_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {c : Option γ} {δ' : Type u_7} {ε : Type u_8} {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε} (h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) : map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b

theorem Option.map_map₂_distrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β} {α' : Type u_5} {β' : Type u_6} {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) : Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ a) (Option.map g₂ b)

The following symmetric restatement are needed because unification has a hard time figuring all the functions if you symmetrize on the spot. This is also how the other n-ary APIs do it.

theorem Option.map_map₂_distrib_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β} {α' : Type u_5} {g : γ → δ} {f' : α' → β → δ} {g' : α → α'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b) : Option.map g (map₂ f a b) = map₂ f' (Option.map g' a) b

Symmetric statement to Option.map₂_map_left_comm.

theorem Option.map_map₂_distrib_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β} {β' : Type u_6} {g : γ → δ} {f' : α → β' → δ} {g' : β → β'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)) : Option.map g (map₂ f a b) = map₂ f' a (Option.map g' b)

Symmetric statement to Option.map_map₂_right_comm.

theorem Option.map₂_map_left_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {α' : Type u_5} {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ} (h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)) : map₂ f (Option.map g a) b = Option.map g' (map₂ f' a b)

Symmetric statement to Option.map_map₂_distrib_left.

theorem Option.map_map₂_right_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {β' : Type u_6} {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ} (h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)) : map₂ f a (Option.map g b) = Option.map g' (map₂ f' a b)

Symmetric statement to Option.map_map₂_distrib_right.

theorem Option.map_map₂_antidistrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β} {α' : Type u_5} {β' : Type u_6} {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) : Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ b) (Option.map g₂ a)

theorem Option.map_map₂_antidistrib_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β} {β' : Type u_6} {g : γ → δ} {f' : β' → α → δ} {g' : β → β'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a) : Option.map g (map₂ f a b) = map₂ f' (Option.map g' b) a

Symmetric statement to Option.map₂_map_left_anticomm.

theorem Option.map_map₂_antidistrib_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β} {α' : Type u_5} {g : γ → δ} {f' : β → α' → δ} {g' : α → α'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)) : Option.map g (map₂ f a b) = map₂ f' b (Option.map g' a)

Symmetric statement to Option.map_map₂_right_anticomm.

theorem Option.map₂_map_left_anticomm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {α' : Type u_5} {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ} (h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)) : map₂ f (Option.map g a) b = Option.map g' (map₂ f' b a)

Symmetric statement to Option.map_map₂_antidistrib_left.

theorem Option.map_map₂_right_anticomm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {β' : Type u_6} {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ} (h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)) : map₂ f a (Option.map g b) = Option.map g' (map₂ f' b a)

Symmetric statement to Option.map_map₂_antidistrib_right.

theorem Option.map₂_left_identity {α : Type u_1} {β : Type u_2} {f : α → β → β} {a : α} (h : ∀ (b : β), f a b = b) (o : Option β) : map₂ f (some a) o = o

If a is a left identity for a binary operation f, then some a is a left identity for Option.map₂ f.

theorem Option.map₂_right_identity {α : Type u_1} {β : Type u_2} {f : α → β → α} {b : β} (h : ∀ (a : α), f a b = a) (o : Option α) : map₂ f o (some b) = o

If b is a right identity for a binary operation f, then some b is a right identity for Option.map₂ f.