omap — Mathlib

English

Given a function f: β → γ, the operation omap f on Option(α × β) produces none from none, and for some (a, b) returns some (a, f(b)).

Русский

Пусть f: β → γ. Операция omap f над Option(α × β) отправляет none в none, а some (a, b) в some (a, f(b)).

LaTeX

$$$\\mathrm{omap}\; f\\; \\mathrm{none} = \\mathrm{none}$, \\quad $\\mathrm{omap}\\; f\\; (\\mathrm{some}(a,b)) = \\mathrm{some}(a, f(b))$$$

Lean4

/-- Functorial action of the functor `Option (α × _)` -/
@[simp]
def omap (f : β → γ) : Option (α × β) → Option (α × γ)
  | none => none
  | some (a, b) => some (a, f b)

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