ENatMap — Mathlib

English

A version of ENat.map for AddHom; ENat.map extends an additive hom from ℕ to ENat(WithTop N).

Русский

Версия ENat.map для AddHom; ENat.map распространяется на ENat(WithTop N) через аддитивный гомоморфизм.

LaTeX

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

Lean4

/-- A version of `WithTop.map` for `AddHom`s. -/
@[simps -fullyApplied]
protected def _root_.AddHom.ENatMap {N : Type*} [Add N] (f : AddHom ℕ N) : AddHom ℕ∞ (WithTop N)
    where
  toFun := ENat.map f
  map_add' := ENat.map_add f

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