HepLean Documentation

Mathlib.Data.Option.NAry

Binary map of options #

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 the n-ary section of Mathlib.Data.Set.Basic, to Mathlib.Data.Finset.NAry and to Mathlib.Order.Filter.NAry. Please keep them in sync. (porting note - only some of these may exist right now!)

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

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
Instances For
    theorem Option.map₂_def {α : Type u} {β : Type u} {γ : Type u} (f : αβγ) (a : Option α) (b : Option β) :
    Option.map₂ f a b = Seq.seq (f <$> a) fun (x : Unit) => 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 : β) :
    Option.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 : β) :
    Option.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 β) :
    Option.map₂ f none b = none
    @[simp]
    theorem Option.map₂_none_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : Option α) :
    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 β) :
    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 : β) :
    Option.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 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_2} {γ : Type u_3} {f : αβγ} {a : Option α} {b : Option β} :
    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 β) :
    Option.map₂ f a b = Option.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 (Option.map₂ f a b) = Option.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 : αγ) :
    Option.map₂ f (Option.map g a) b = Option.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 : βγ) :
    Option.map₂ f a (Option.map g b) = Option.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 β) :
    @[simp]
    theorem Option.map_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} (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 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)) :
    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) :
    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)) :
    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) :
    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)) :

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

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

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

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

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

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

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

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

    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 β) :
    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 α) :
    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.