coeFnMonoidHom — Mathlib

English

The coercion from C_c(α,β) to α → β is a additive monoid homomorphism: it preserves addition and maps zero to the zero function.

Русский

Отображение из C_c(α,β) в α → β является аддитивным гомоморфионом моноидов: сохраняет сложение и ноль переходит в ноль-функцию.

LaTeX

$$$$(\mathrm{coeFnMonoidHom})(f+g) = (\mathrm{coeFnMonoidHom})(f) + (\mathrm{coeFnMonoidHom})(g)$$ and$$ (\mathrm{coeFnMonoidHom})(0) = 0, $$$$

Lean4

/-- Coercion to a function as a `AddMonoidHom`. Similar to `AddMonoidHom.coeFn`. -/
def coeFnMonoidHom [AddMonoid β] [ContinuousAdd β] : C_c(α, β) →+ α → β
    where
  toFun f := f
  map_zero' := coe_zero
  map_add' := coe_add

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