ENatMap — Mathlib

English

A version of ENat.map lifted to ENat for ZeroHom; it defines ENat.map on ENat via a ZeroHom.

Русский

Версия ENat.map, переносимая на ENat для ZeroHom; задаёт ENat.map через ZERO-гомоморфизм.

LaTeX

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

Lean4

/-- A version of `ENat.map` for `ZeroHom`s. -/
protected def _root_.ZeroHom.ENatMap {N : Type*} [Zero N] (f : ZeroHom ℕ N) : ZeroHom ℕ∞ (WithTop N)
    where
  toFun := ENat.map f
  map_zero' := by simp

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