Mathlib.Data.Option.NAry

Option.map₂ definition

(f : α → β → γ) (a : Option α) (b : Option β) : Option γ

Full source

/-- 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 `α × β → γ`. -/
def map₂ (f : α → β → γ) (a : Option α) (b : Option β) : Option γ :=
  a.bind fun a => b.map <| f a

Binary map on optional values

Informal description

Given a binary function $ f : \alpha \to \beta \to \gamma $, the function `Option.map₂` lifts $ f $ to operate on optional values, returning `none` if either input is `none` and applying $ f $ to the values otherwise. Mathematically, this corresponds to the image of the function $ f $ viewed as a map $ \alpha \times \beta \to \gamma $.

Option.map₂_def theorem

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

Full source

/-- `Option.map₂` in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism. -/
theorem map₂_def {α β γ : Type u} (f : α → β → γ) (a : Option α) (b : Option β) :
    map₂ f a b = f <$> af <$> a <*> b := by
  cases a <;> rfl

Definition of Binary Map on Options via Applicative Operations

Informal description

For any types $\alpha, \beta, \gamma$ and any binary function $f : \alpha \to \beta \to \gamma$, the binary map operation on optional values satisfies $\mathrm{map}_2\, f\, a\, b = f <\$> a <*\> b$ for all $a : \mathrm{Option}\,\alpha$ and $b : \mathrm{Option}\,\beta$.

Option.map₂_some_some theorem

(f : α → β → γ) (a : α) (b : β) : map₂ f (some a) (some b) = f a b

Full source

@[simp]
theorem map₂_some_some (f : α → β → γ) (a : α) (b : β) : map₂ f (some a) (some b) = f a b := rfl

Binary Map on Some Values Equals Function Application

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and elements $a \in \alpha$, $b \in \beta$, the binary map operation on optional values satisfies $\text{map}_2 f (\text{some } a) (\text{some } b) = f a b$.

Option.map₂_coe_coe theorem

(f : α → β → γ) (a : α) (b : β) : map₂ f a b = f a b

Full source

theorem map₂_coe_coe (f : α → β → γ) (a : α) (b : β) : map₂ f a b = f a b := rfl

Binary Map on Options Preserves Function Application on Non-Optional Values

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and elements $a \in \alpha$, $b \in \beta$, the binary map of options satisfies $\mathrm{map}_2\, f\, a\, b = f\, a\, b$.

Option.map₂_none_left theorem

(f : α → β → γ) (b : Option β) : map₂ f none b = none

Full source

@[simp]
theorem map₂_none_left (f : α → β → γ) (b : Option β) : map₂ f none b = none := rfl

Left None Absorption for Binary Map on Options

Informal description

For any binary function $f \colon \alpha \to \beta \to \gamma$ and any optional value $b \colon \text{Option } \beta$, the binary map operation satisfies $\text{map}_2 f \ \text{none} \ b = \text{none}$.

Option.map₂_none_right theorem

(f : α → β → γ) (a : Option α) : map₂ f a none = none

Full source

@[simp]
theorem map₂_none_right (f : α → β → γ) (a : Option α) : map₂ f a none = none := by cases a <;> rfl

Binary Map with None Right Argument Yields None

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and any optional value $a : \text{Option }\alpha$, the binary map operation satisfies $\text{map}_2\,f\,a\,\text{none} = \text{none}$.

Option.map₂_coe_left theorem

(f : α → β → γ) (a : α) (b : Option β) : map₂ f a b = b.map fun b => f a b

Full source

@[simp]
theorem map₂_coe_left (f : α → β → γ) (a : α) (b : Option β) : map₂ f a b = b.map fun b => f a b :=
  rfl

Binary map with definite left argument reduces to unary map

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, element $a \in \alpha$, and optional value $b \in \text{Option } \beta$, the binary map $\text{map}_2(f, \text{some}(a), b)$ is equal to mapping the function $f(a, \cdot)$ over $b$. In other words, $$\text{map}_2(f, a, b) = b.\text{map} (\lambda b', f(a, b'))$$

Option.map₂_coe_right theorem

(f : α → β → γ) (a : Option α) (b : β) : map₂ f a b = a.map fun a => f a b

Full source

@[simp]
theorem map₂_coe_right (f : α → β → γ) (a : Option α) (b : β) :
    map₂ f a b = a.map fun a => f a b := by cases a <;> rfl

Binary map on optional values with right coefficient

Informal description

Given a binary function $f : \alpha \to \beta \to \gamma$, an optional value $a : \text{Option } \alpha$, and a value $b : \beta$, the binary map $\text{map}_2$ satisfies $\text{map}_2(f, a, b) = \text{map} (\lambda a', f(a', b)) a$.

Option.mem_map₂_iff theorem

{c : γ} : c ∈ map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

Full source

theorem mem_map₂_iff {c : γ} : c ∈ map₂ f a bc ∈ map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c := by
  simp [map₂, bind_eq_some]

Characterization of Membership in Binary Map of Options

Informal description

For any element $c \in \gamma$, $c$ is in the binary map `Option.map₂ f a b` if and only if there exist elements $a' \in a$ and $b' \in b$ such that $f(a', b') = c$.

Option.map₂_eq_some_iff theorem

{c : γ} : map₂ f a b = some c ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

Full source

/-- `simp`-normal form of `mem_map₂_iff`. -/
@[simp]
theorem map₂_eq_some_iff {c : γ} :
    map₂map₂ f a b = some c ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c := by
  simp [map₂, bind_eq_some]

Characterization of Nonempty Result in Binary Map of Options

Informal description

For a binary function $f : \alpha \to \beta \to \gamma$ and optional values $a : \text{Option } \alpha$, $b : \text{Option } \beta$, the result of `map₂ f a b` is `some c` for some $c : \gamma$ if and only if there exist values $a' \in a$ and $b' \in b$ such that $f a' b' = c$.

Option.map₂_eq_none_iff theorem

: map₂ f a b = none ↔ a = none ∨ b = none

Full source

@[simp]
theorem map₂_eq_none_iff : map₂map₂ f a b = none ↔ a = none ∨ b = none := by
  cases a <;> cases b <;> simp

Binary Map Yields None iff Either Argument is None

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and optional values $a : \text{Option }\alpha$, $b : \text{Option }\beta$, the binary map operation $\text{map}_2\,f\,a\,b$ results in $\text{none}$ if and only if either $a$ is $\text{none}$ or $b$ is $\text{none}$.

Option.map₂_swap theorem

(f : α → β → γ) (a : Option α) (b : Option β) : map₂ f a b = map₂ (fun a b => f b a) b a

Full source

theorem map₂_swap (f : α → β → γ) (a : Option α) (b : Option β) :
    map₂ f a b = map₂ (fun a b => f b a) b a := by cases a <;> cases b <;> rfl

Commutativity of Binary Map on Optional Values

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and optional values $a : \text{Option }\alpha$, $b : \text{Option }\beta$, the binary map operation satisfies $\text{map}_2\,f\,a\,b = \text{map}_2\,(\lambda x\,y, f\,y\,x)\,b\,a$.

Option.map_map₂ theorem

(f : α → β → γ) (g : γ → δ) : (map₂ f a b).map g = map₂ (fun a b => g (f a b)) a b

Full source

theorem map_map₂ (f : α → β → γ) (g : γ → δ) :
    (map₂ f a b).map g = map₂ (fun a b => g (f a b)) a b := by cases a <;> cases b <;> rfl

Composition of Mapping with Binary Map on Options

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and any function $g : \gamma \to \delta$, the composition of mapping $g$ over the result of applying `map₂ f` to optional values $a$ and $b$ is equal to applying `map₂` to the function $\lambda a\ b, g(f(a,b))$ with the same optional values $a$ and $b$. In symbols: $$ \text{map}\ g\ (\text{map₂}\ f\ a\ b) = \text{map₂}\ (\lambda a\ b, g(f(a,b)))\ a\ b $$

Option.map₂_map_left theorem

(f : γ → β → δ) (g : α → γ) : map₂ f (a.map g) b = map₂ (fun a b => f (g a) b) a b

Full source

theorem map₂_map_left (f : γ → β → δ) (g : α → γ) :
    map₂ f (a.map g) b = map₂ (fun a b => f (g a) b) a b := by cases a <;> rfl

Compatibility of Binary Map with Left Function Composition

Informal description

For any function $f : \gamma \to \beta \to \delta$, any function $g : \alpha \to \gamma$, and any optional values $a : \text{Option } \alpha$ and $b : \text{Option } \beta$, the following equality holds: \[ \text{map}_2\, f\, (a.\text{map}\, g)\, b = \text{map}_2\, (\lambda a\, b, f\, (g\, a)\, b)\, a\, b. \]

Option.map₂_map_right theorem

(f : α → γ → δ) (g : β → γ) : map₂ f a (b.map g) = map₂ (fun a b => f a (g b)) a b

Full source

theorem map₂_map_right (f : α → γ → δ) (g : β → γ) :
    map₂ f a (b.map g) = map₂ (fun a b => f a (g b)) a b := by cases b <;> rfl

Right Mapping Commutes with Binary Map on Options

Informal description

For any function $f : \alpha \to \gamma \to \delta$, any function $g : \beta \to \gamma$, and any optional values $a : \text{Option }\alpha$ and $b : \text{Option }\beta$, the following equality holds: \[ \text{map₂ } f\ a\ (b.\text{map } g) = \text{map₂ } (\lambda a\ b \Rightarrow f\ a\ (g\ b))\ a\ b \] This means that mapping $g$ over the right argument of $b$ and then applying $f$ via `map₂` is equivalent to applying a modified version of $f$ that first applies $g$ to its second argument.

Option.map₂_curry theorem

(f : α × β → γ) (a : Option α) (b : Option β) : map₂ (curry f) a b = Option.map f (map₂ Prod.mk a b)

Full source

@[simp]
theorem map₂_curry (f : α × β → γ) (a : Option α) (b : Option β) :
    map₂ (curry f) a b = Option.map f (map₂ Prod.mk a b) := (map_map₂ _ _).symm

Currying and Mapping Commute for Binary Map on Options

Informal description

For any function $f : \alpha \times \beta \to \gamma$ and optional values $a : \text{Option }\alpha$, $b : \text{Option }\beta$, the binary map of the curried function $\text{curry}\,f$ applied to $a$ and $b$ is equal to mapping $f$ over the binary map of the pair constructor applied to $a$ and $b$. In symbols: \[ \text{map}_2\, (\text{curry}\, f)\, a\, b = \text{map}\, f\, (\text{map}_2\, \text{Prod.mk}\, a\, b) \] where $\text{curry}\, f\, a\, b = f\, (a, b)$ and $\text{Prod.mk}$ is the pair constructor.

Option.map_uncurry theorem

(f : α → β → γ) (x : Option (α × β)) : x.map (uncurry f) = map₂ f (x.map Prod.fst) (x.map Prod.snd)

Full source

@[simp]
theorem map_uncurry (f : α → β → γ) (x : Option (α × β)) :
    x.map (uncurry f) = map₂ f (x.map Prod.fst) (x.map Prod.snd) := by cases x <;> rfl

Equivalence of Mapping Uncurried Function and Binary Map on Projections for Optional Pairs

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and optional pair $x : \text{Option}(\alpha \times \beta)$, mapping the uncurried version of $f$ over $x$ is equivalent to applying the binary map operation to the projections of $x$. That is, $$x.\text{map}(\text{uncurry}\, f) = \text{map}_2\, f\, (x.\text{map}\,\text{fst})\, (x.\text{map}\,\text{snd})$$ where $\text{uncurry}\, f\, (a,b) = f\, a\, b$, $\text{fst}$ is the first projection, and $\text{snd}$ is the second projection.

Option.map₂_assoc theorem

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

Full source

theorem map₂_assoc {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) := by
  cases a <;> cases b <;> cases c <;> simp [h_assoc]

Associativity of Binary Map on Optional Values

Informal description

Given binary functions $f : \delta \to \gamma \to \varepsilon$, $g : \alpha \to \beta \to \delta$, $f' : \alpha \to \varepsilon' \to \varepsilon$, and $g' : \beta \to \gamma \to \varepsilon'$ satisfying the associativity condition: \[ \forall a\,b\,c, \ f(g(a, b), c) = f'(a, g'(b, c)), \] then for any optional values $a : \text{Option }\alpha$, $b : \text{Option }\beta$, and $c : \text{Option }\gamma$, the following equality holds: \[ \text{map}_2\,f\,(\text{map}_2\,g\,a\,b)\,c = \text{map}_2\,f'\,a\,(\text{map}_2\,g'\,b\,c). \]

Option.map₂_comm theorem

{g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : map₂ f a b = map₂ g b a

Full source

theorem map₂_comm {g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : map₂ f a b = map₂ g b a := by
  cases a <;> cases b <;> simp [h_comm]

Commutativity of Binary Map on Optional Values

Informal description

For any binary functions $f : \alpha \to \beta \to \gamma$ and $g : \beta \to \alpha \to \gamma$ such that $f(a, b) = g(b, a)$ for all $a \in \alpha$ and $b \in \beta$, and for any optional values $a : \text{Option }\alpha$ and $b : \text{Option }\beta$, the binary map operation satisfies $\text{map}_2\,f\,a\,b = \text{map}_2\,g\,b\,a$.

Option.map₂_left_comm theorem

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

Full source

theorem map₂_left_comm {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) := by
  cases a <;> cases b <;> cases c <;> simp [h_left_comm]

Left Commutativity of Binary Map on Optional Values

Informal description

Given binary functions $f : \alpha \to \delta \to \varepsilon$, $g : \beta \to \gamma \to \delta$, $f' : \alpha \to \gamma \to \delta'$, and $g' : \beta \to \delta' \to \varepsilon$ satisfying the left-commutativity condition: \[ \forall a\,b\,c, \ f\,a\,(g\,b\,c) = g'\,b\,(f'\,a\,c), \] then for any optional values $a : \text{Option }\alpha$, $b : \text{Option }\beta$, and $c : \text{Option }\gamma$, the following equality holds: \[ \text{map}_2\,f\,a\,(\text{map}_2\,g\,b\,c) = \text{map}_2\,g'\,b\,(\text{map}_2\,f'\,a\,c). \]

Option.map₂_right_comm theorem

 {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

Full source

theorem map₂_right_comm {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 := by
  cases a <;> cases b <;> cases c <;> simp [h_right_comm]

Right Commutativity of Binary Map on Optional Values

Informal description

Let $f : \delta \to \gamma \to \varepsilon$, $g : \alpha \to \beta \to \delta$, $f' : \alpha \to \gamma \to \delta'$, and $g' : \delta' \to \beta \to \varepsilon$ be functions such that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the following right-commutativity condition holds: \[ f(g(a, b), c) = g'(f'(a, c), b). \] Then for any optional values $a : \text{Option } \alpha$, $b : \text{Option } \beta$, and $c : \text{Option } \gamma$, we have: \[ \text{map}_2 f (\text{map}_2 g a b) c = \text{map}_2 g' (\text{map}_2 f' a c) b. \]

Option.map_map₂_distrib theorem

 {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'} (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
  (map₂ f a b).map g = map₂ f' (a.map g₁) (b.map g₂)

Full source

theorem map_map₂_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
    (map₂ f a b).map g = map₂ f' (a.map g₁) (b.map g₂) := by
  cases a <;> cases b <;> simp [h_distrib]

Distributivity of Map over Binary Map on Options

Informal description

Let $g : \gamma \to \delta$, $f' : \alpha' \to \beta' \to \delta$, $g_1 : \alpha \to \alpha'$, and $g_2 : \beta \to \beta'$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the equality $g(f(a, b)) = f'(g_1(a), g_2(b))$ holds. Then for any optional values $a : \text{Option } \alpha$ and $b : \text{Option } \beta$, the following equality holds: \[ \text{map } g (\text{map}_2 f a b) = \text{map}_2 f' (\text{map } g_1 a) (\text{map } g_2 b). \]

Option.map_map₂_distrib_left theorem

 {g : γ → δ} {f' : α' → β → δ} {g' : α → α'} (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
  (map₂ f a b).map g = map₂ f' (a.map g') b

Full source

/-- Symmetric statement to `Option.map₂_map_left_comm`. -/
theorem map_map₂_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
    (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
    (map₂ f a b).map g = map₂ f' (a.map g') b := by cases a <;> cases b <;> simp [h_distrib]

Left Distributivity of Map over Binary Map on Options

Informal description

Let $g : \gamma \to \delta$, $f' : \alpha' \to \beta \to \delta$, and $g' : \alpha \to \alpha'$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the equality $g(f(a, b)) = f'(g'(a), b)$ holds. Then, for any optional values $a : \text{Option } \alpha$ and $b : \text{Option } \beta$, the following equality holds: \[ \text{map } g (\text{map}_2 f a b) = \text{map}_2 f' (\text{map } g' a) b. \]

Option.map_map₂_distrib_right theorem

 {g : γ → δ} {f' : α → β' → δ} {g' : β → β'} (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) :
  (map₂ f a b).map g = map₂ f' a (b.map g')

Full source

/-- Symmetric statement to `Option.map_map₂_right_comm`. -/
theorem map_map₂_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) : (map₂ f a b).map g = map₂ f' a (b.map g') := by
  cases a <;> cases b <;> simp [h_distrib]

Right Distributivity of Map over Binary Map on Options

Informal description

Let $g : \gamma \to \delta$, $f' : \alpha \to \beta' \to \delta$, and $g' : \beta \to \beta'$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the equality $g(f(a, b)) = f'(a, g'(b))$ holds. Then, for any optional values $a : \text{Option } \alpha$ and $b : \text{Option } \beta$, the following equality holds: \[ \text{map } g (\text{map}_2 f a b) = \text{map}_2 f' a (\text{map } g' b). \]

Option.map₂_map_left_comm theorem

 {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ} (h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) :
  map₂ f (a.map g) b = (map₂ f' a b).map g'

Full source

/-- Symmetric statement to `Option.map_map₂_distrib_left`. -/
theorem map₂_map_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
    (h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) : map₂ f (a.map g) b = (map₂ f' a b).map g' := by
  cases a <;> cases b <;> simp [h_left_comm]

Left-commutativity of binary map with precomposition on options

Informal description

Let $f : \alpha' \to \beta \to \gamma$, $g : \alpha \to \alpha'$, $f' : \alpha \to \beta \to \delta$, and $g' : \delta \to \gamma$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the following left-commutativity condition holds: \[ f(g(a), b) = g'(f'(a, b)) \] Then for any optional value $a : \text{Option } \alpha$ and any value $b : \beta$, we have: \[ \text{map}_2 f (\text{map } g a) b = \text{map } g' (\text{map}_2 f' a b) \]

Option.map_map₂_right_comm theorem

 {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ} (h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) :
  map₂ f a (b.map g) = (map₂ f' a b).map g'

Full source

/-- Symmetric statement to `Option.map_map₂_distrib_right`. -/
theorem map_map₂_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
    (h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) :
    map₂ f a (b.map g) = (map₂ f' a b).map g' := by cases a <;> cases b <;> simp [h_right_comm]

Right-commutativity of Binary Map with Postcomposition on Options

Informal description

Let $f : \alpha \to \beta' \to \gamma$, $g : \beta \to \beta'$, $f' : \alpha \to \beta \to \delta$, and $g' : \delta \to \gamma$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the following right-commutativity condition holds: \[ f(a, g(b)) = g'(f'(a, b)) \] Then for any optional value $a : \text{Option } \alpha$ and any value $b : \text{Option } \beta$, we have: \[ \text{map}_2 f a (b \text{ mapped by } g) = \text{map } g' (\text{map}_2 f' a b) \]

Option.map_map₂_antidistrib theorem

 {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'} (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
  (map₂ f a b).map g = map₂ f' (b.map g₁) (a.map g₂)

Full source

theorem map_map₂_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
    (map₂ f a b).map g = map₂ f' (b.map g₁) (a.map g₂) := by
  cases a <;> cases b <;> simp [h_antidistrib]

Antidistributivity of Postcomposition over Binary Map on Options

Informal description

Let $f : \alpha \to \beta \to \gamma$, $g : \gamma \to \delta$, $f' : \beta' \to \alpha' \to \delta$, $g_1 : \beta \to \beta'$, and $g_2 : \alpha \to \alpha'$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the following antidistributivity condition holds: \[ g(f(a, b)) = f'(g_1(b), g_2(a)) \] Then for any optional values $a \in \text{Option } \alpha$ and $b \in \text{Option } \beta$, we have: \[ \text{map}_2 f a b \text{ followed by } g = \text{map}_2 f' (b \text{ mapped by } g_1) (a \text{ mapped by } g_2) \]

Option.map_map₂_antidistrib_left theorem

 {g : γ → δ} {f' : β' → α → δ} {g' : β → β'} (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
  (map₂ f a b).map g = map₂ f' (b.map g') a

Full source

/-- Symmetric statement to `Option.map₂_map_left_anticomm`. -/
theorem map_map₂_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
    (map₂ f a b).map g = map₂ f' (b.map g') a := by
  cases a <;> cases b <;> simp [h_antidistrib]

Antidistributivity of Postcomposition over Binary Map on Options (Left Version)

Informal description

Let $f : \alpha \to \beta \to \gamma$, $g : \gamma \to \delta$, $f' : \beta' \to \alpha \to \delta$, and $g' : \beta \to \beta'$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the following antidistributivity condition holds: \[ g(f(a, b)) = f'(g'(b), a) \] Then for any optional values $a \in \text{Option } \alpha$ and $b \in \text{Option } \beta$, we have: \[ \text{map}_2 f a b \text{ followed by } g = \text{map}_2 f' (b \text{ mapped by } g') a \]

Option.map_map₂_antidistrib_right theorem

 {g : γ → δ} {f' : β → α' → δ} {g' : α → α'} (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
  (map₂ f a b).map g = map₂ f' b (a.map g')

Full source

/-- Symmetric statement to `Option.map_map₂_right_anticomm`. -/
theorem map_map₂_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
    (map₂ f a b).map g = map₂ f' b (a.map g') := by cases a <;> cases b <;> simp [h_antidistrib]

Antidistributivity of Postcomposition over Binary Map on Options (Right Version)

Informal description

Let $f : \alpha \to \beta \to \gamma$, $g : \gamma \to \delta$, $f' : \beta \to \alpha' \to \delta$, and $g' : \alpha \to \alpha'$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the following antidistributivity condition holds: \[ g(f(a, b)) = f'(b, g'(a)) \] Then for any optional values $a \in \text{Option } \alpha$ and $b \in \text{Option } \beta$, we have: \[ \text{map}_2 f a b \text{ followed by } g = \text{map}_2 f' b (a \text{ mapped by } g') \]

Option.map₂_map_left_anticomm theorem

 {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ} (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) :
  map₂ f (a.map g) b = (map₂ f' b a).map g'

Full source

/-- Symmetric statement to `Option.map_map₂_antidistrib_left`. -/
theorem map₂_map_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
    (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) :
    map₂ f (a.map g) b = (map₂ f' b a).map g' := by cases a <;> cases b <;> simp [h_left_anticomm]

Anticommutativity of Binary Map with Left Mapping

Informal description

Let $f : \alpha' \to \beta \to \gamma$, $g : \alpha \to \alpha'$, $f' : \beta \to \alpha \to \delta$, and $g' : \delta \to \gamma$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the following anticommutativity condition holds: \[ f(g(a), b) = g'(f'(b, a)) \] Then for any optional value $a \in \text{Option } \alpha$ and any value $b \in \beta$, we have: \[ \text{map}_2 f (a.\text{map} g) b = (\text{map}_2 f' b a).\text{map} g' \]

Option.map_map₂_right_anticomm theorem

 {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ} (h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) :
  map₂ f a (b.map g) = (map₂ f' b a).map g'

Full source

/-- Symmetric statement to `Option.map_map₂_antidistrib_right`. -/
theorem map_map₂_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
    (h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) :
    map₂ f a (b.map g) = (map₂ f' b a).map g' := by cases a <;> cases b <;> simp [h_right_anticomm]

Anticommutativity of Binary Map with Right Mapping

Informal description

Let $f : \alpha \to \beta' \to \gamma$, $g : \beta \to \beta'$, $f' : \beta \to \alpha \to \delta$, and $g' : \delta \to \gamma$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the following anticommutativity condition holds: \[ f(a, g(b)) = g'(f'(b, a)) \] Then for any optional values $a \in \text{Option } \alpha$ and $b \in \text{Option } \beta$, we have: \[ \text{map}_2 f a (b.\text{map} g) = (\text{map}_2 f' b a).\text{map} g' \]

Option.map₂_left_identity theorem

{f : α → β → β} {a : α} (h : ∀ b, f a b = b) (o : Option β) : map₂ f (some a) o = o

Full source

/-- If `a` is a left identity for a binary operation `f`, then `some a` is a left identity for
`Option.map₂ f`. -/
lemma map₂_left_identity {f : α → β → β} {a : α} (h : ∀ b, f a b = b) (o : Option β) :
    map₂ f (some a) o = o := by
  cases o; exacts [rfl, congr_arg some (h _)]

Left Identity Preservation under Option.map₂

Informal description

Let $f : \alpha \to \beta \to \beta$ be a binary operation and $a \in \alpha$ be a left identity for $f$ (i.e., $f(a, b) = b$ for all $b \in \beta$). Then for any optional value $o \in \text{Option} \beta$, the lifted operation satisfies $\text{map}_2 f (\text{some } a) o = o$.

Option.map₂_right_identity theorem

{f : α → β → α} {b : β} (h : ∀ a, f a b = a) (o : Option α) : map₂ f o (some b) = o

Full source

/-- If `b` is a right identity for a binary operation `f`, then `some b` is a right identity for
`Option.map₂ f`. -/
lemma map₂_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (o : Option α) :
    map₂ f o (some b) = o := by
  simp [h, map₂]

Right identity preservation under binary map of options

Informal description

Let $f : \alpha \to \beta \to \alpha$ be a binary operation and $b \in \beta$ be a right identity for $f$ (i.e., $f(a, b) = a$ for all $a \in \alpha$). Then for any optional value $o \in \text{Option}(\alpha)$, the binary map $\text{map}_2(f, o, \text{some}(b)) = o$.

Mathlib.Data.Option.NAry

Main declarations

Notes