map_add — Mathlib

English

ENat.map distributes over addition: for any function f, (a + b).map f = a.map f + b.map f.

Русский

ENat.map распределяет по сложению: (a + b).map f = a.map f + b.map f.

LaTeX

$$$$ \\mathrm{ENat.map}\;f\\,(a+b) = \\mathrm{ENat.map}\;f\,a + \\mathrm{ENat.map}\;f\,b $$$$

Lean4

@[simp]
protected theorem map_add {β F} [Add β] [FunLike F ℕ β] [AddHomClass F ℕ β] (f : F) (a b : ℕ∞) :
    (a + b).map f = a.map f + b.map f :=
  WithTop.map_add f a b

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