mathlib3 documentation

data.option.n_ary

Binary map of options #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

Notes #

This file is very similar to data.set.n_ary, data.finset.n_ary and order.filter.n_ary. 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_3} {γ : Type u_5} (f : α β γ) (a : option α) (b : 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
theorem option.map₂_def {α β γ : Type u_1} (f : α β γ) (a : option α) (b : option β) :
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_3} {γ : Type u_5} (f : α β γ) (a : α) (b : β) :
theorem option.map₂_coe_coe {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α β γ) (a : α) (b : β) :
@[simp]
theorem option.map₂_none_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α β γ) (b : option β) :
@[simp]
theorem option.map₂_none_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α β γ) (a : option α) :
@[simp]
theorem option.map₂_coe_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α β γ) (a : α) (b : option β) :
option.map₂ f a b = option.map (λ (b : β), f a b) b
@[simp]
theorem option.map₂_coe_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α β γ) (a : option α) (b : β) :
option.map₂ f a b = option.map (λ (a : α), f a b) a
@[simp]
theorem option.mem_map₂_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {a : option α} {b : option β} {c : γ} :
c option.map₂ f a b (a' : α) (b' : β), a' a b' b f a' b' = c
@[simp]
theorem option.map₂_eq_none_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {a : option α} {b : option β} :
theorem option.map₂_swap {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α β γ) (a : option α) (b : option β) :
option.map₂ f a b = option.map₂ (λ (a : β) (b : α), f b a) b a
theorem option.map_map₂ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {a : option α} {b : option β} (f : α β γ) (g : γ δ) :
option.map g (option.map₂ f a b) = option.map₂ (λ (a : α) (b : β), g (f a b)) a b
theorem option.map₂_map_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {a : option α} {b : option β} (f : γ β δ) (g : α γ) :
option.map₂ f (option.map g a) b = option.map₂ (λ (a : α) (b : β), f (g a) b) a b
theorem option.map₂_map_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {a : option α} {b : option β} (f : α γ δ) (g : β γ) :
option.map₂ f a (option.map g b) = option.map₂ (λ (a : α) (b : β), f a (g b)) a b
@[simp]
theorem option.map₂_curry {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α × β γ) (a : option α) (b : option β) :
@[simp]
theorem option.map_uncurry {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α β γ) (x : option × β)) :

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 comm_semigroup.

theorem option.map₂_assoc {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {a : option α} {b : option β} {c : option γ} {f : δ γ ε} {g : α β δ} {f' : α ε' ε} {g' : β γ ε'} (h_assoc : (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) :
theorem option.map₂_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α β γ} {a : option α} {b : option β} {g : β α γ} (h_comm : (a : α) (b : β), f a b = g b a) :
theorem option.map₂_left_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {a : option α} {b : option β} {c : option γ} {f : α δ ε} {g : β γ δ} {f' : α γ δ'} {g' : β δ' ε} (h_left_comm : (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) :
theorem option.map₂_right_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {a : option α} {b : option β} {c : option γ} {f : δ γ ε} {g : α β δ} {f' : α γ δ'} {g' : δ' β ε} (h_right_comm : (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) :
theorem option.map_map₂_distrib {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α β γ} {a : option α} {b : option β} {g : γ δ} {f' : α' β' δ} {g₁ : α α'} {g₂ : β β'} (h_distrib : (a : α) (b : β), g (f a b) = f' (g₁ a) (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_5} {δ : Type u_7} {f : α β γ} {a : option α} {b : option β} {g : γ δ} {f' : α' β δ} {g' : α α'} (h_distrib : (a : α) (b : β), g (f a b) = f' (g' a) b) :

Symmetric statement to option.map₂_map_left_comm.

theorem option.map_map₂_distrib_right {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α β γ} {a : option α} {b : option β} {g : γ δ} {f' : α β' δ} {g' : β β'} (h_distrib : (a : α) (b : β), g (f a b) = f' a (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_5} {δ : Type u_7} {a : option α} {b : option β} {f : α' β γ} {g : α α'} {f' : α β δ} {g' : δ γ} (h_left_comm : (a : α) (b : β), f (g a) b = g' (f' a b)) :

Symmetric statement to option.map_map₂_distrib_left.

theorem option.map_map₂_right_comm {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {a : option α} {b : option β} {f : α β' γ} {g : β β'} {f' : α β δ} {g' : δ γ} (h_right_comm : (a : α) (b : β), f a (g b) = g' (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} {γ : Type u_5} {δ : Type u_7} {f : α β γ} {a : option α} {b : option β} {g : γ δ} {f' : β' α' δ} {g₁ : β β'} {g₂ : α α'} (h_antidistrib : (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) :
theorem option.map_map₂_antidistrib_left {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α β γ} {a : option α} {b : option β} {g : γ δ} {f' : β' α δ} {g' : β β'} (h_antidistrib : (a : α) (b : β), g (f a b) = f' (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_5} {δ : Type u_7} {f : α β γ} {a : option α} {b : option β} {g : γ δ} {f' : β α' δ} {g' : α α'} (h_antidistrib : (a : α) (b : β), g (f a b) = f' b (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_5} {δ : Type u_7} {a : option α} {b : option β} {f : α' β γ} {g : α α'} {f' : β α δ} {g' : δ γ} (h_left_anticomm : (a : α) (b : β), f (g a) b = g' (f' b a)) :

Symmetric statement to option.map_map₂_antidistrib_left.

theorem option.map_map₂_right_anticomm {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {a : option α} {b : option β} {f : α β' γ} {g : β β'} {f' : β α δ} {g' : δ γ} (h_right_anticomm : (a : α) (b : β), f a (g b) = g' (f' b a)) :

Symmetric statement to option.map_map₂_antidistrib_right.

theorem option.map₂_left_identity {α : Type u_1} {β : Type u_3} {f : α β β} {a : α} (h : (b : β), f a b = b) (o : option β) :

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_3} {f : α β α} {b : β} (h : (a : α), f a b = a) (o : option α) :

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