rmap — Mathlib

English

right map of sums: maps the right component by g and leaves the left component unchanged.

Русский

правое отображение суммы: отображает правый компонент функцией g и сохраняет левый компонент без изменений.

LaTeX

$$$\\mathrm{rmap} : (\\beta \\to \\gamma) \\to (\\alpha \\oplus \\beta) \\to (\\alpha \\oplus \\gamma)$$$

Lean4

/-- right map of `⊕` -/
def rmap (f : β → γ) : α ⊕ β → α ⊕ γ
  | Sum.inl a => Sum.inl a
  | Sum.inr b => Sum.inr (f b)

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