map — Mathlib

English

Lift a function to germs: a function op : β → γ induces a map on germs.

Русский

Поднять отображение к зародышам: отображение op : β → γ порождает отображение на зародышах.

LaTeX

$$$ \mathrm{map}(op) : \mathrm{Germ}(l, \beta) \to \mathrm{Germ}(l, \gamma)$$$

Lean4

/-- Lift a function `β → γ` to a function `Germ l β → Germ l γ`. -/
def map (op : β → γ) : Germ l β → Germ l γ :=
  map' (op ∘ ·) fun _ _ H => H.mono fun _ H => congr_arg op H

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