map₂_def — Mathlib

English

The binary map operation map₂ f on options a and b can be expressed in terms of the functor/applicative structure as map₂ f a b = f <$> a <*> b.

Русский

Бинарное отображение map₂ f над опциями a и b выражается через структуру отображения как map₂ f a b = f <$> a <*> b.

LaTeX

$$$ \mathrm{map}_2 f\ a\ b = f\ <$>\ a\ <*>\ b $$$

Lean4

/-- `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 <$> a <*> b := by
  cases a <;> rfl

Похожие утверждения