lmap — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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