English
A version of ENat.map lifted to ENat for OneHom; it defines a map on ENat that agrees with ENat.map on inputs from ℕ.
Русский
Версия ENat.map, переносимая на ENat для OneHom; задаёт отображение на ENat, согласующееся с ENat.map на входах из ℕ.
LaTeX
$$$$ \\text{OneHom.ENatMap}(f)(n) = \\mathrm{ENat.map}(f)(n) \\quad (n \\in \\mathbb{N}^∞) $$$$
Lean4
/-- A version of `ENat.map` for `OneHom`s. -/
-- @[to_additive (attr := simps -fullyApplied)
-- "A version of `ENat.map` for `ZeroHom`s"]
protected def _root_.OneHom.ENatMap {N : Type*} [One N] (f : OneHom ℕ N) : OneHom ℕ∞ (WithTop N)
where
toFun := ENat.map f
map_one' := by simp
