ENatMap — Mathlib

English

A version of ENat.map for AddMonoidHom; ENat.map lifts a ℕ →+ α to ENat(WithTop α).

Русский

Версия ENat.map для AddMonoidHom; ENat.map поднимает ℕ →+ α до ENat(WithTop α).

LaTeX

$$$$ \\text{AddMonoidHom.ENatMap}(f)(n) = \\mathrm{ENat.map}(f)(n) \\quad (n \\in \\mathbb{N}^∞) $$$$

Lean4

/-- A version of `WithTop.map` for `AddMonoidHom`s. -/
@[simps -fullyApplied]
protected def _root_.AddMonoidHom.ENatMap {N : Type*} [AddZeroClass N] (f : ℕ →+ N) : ℕ∞ →+ WithTop N :=
  { ZeroHom.ENatMap f.toZeroHom, AddHom.ENatMap f.toAddHom with toFun := ENat.map f }

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