coeFnAddHom — Mathlib

English

The coercion from bounded continuous functions to AddMonoidHom is additive: coeFnAddHom is an additive hom.

Русский

Пусть отображение из ограниченных непрерывных функций в аддитивный гомоморфизм — аддитивно сохраняется: coeFnAddHom — аддитивный гомоморфизм.

LaTeX

$$$\text{coeFnAddHom} : (\alpha \to^{\mathrm{b}} \beta) \toplus (\alpha \to \beta)$ is additive: $\bigl( f+g \bigr) \mapsto (f+g)$$$

Lean4

/-- Coercion of a `NormedAddGroupHom` is an `AddMonoidHom`. Similar to `AddMonoidHom.coeFn`. -/
@[simps]
def coeFnAddHom [AddMonoid β] [BoundedAdd β] [ContinuousAdd β] : (α →ᵇ β) →+ α → β
    where
  toFun := (⇑)
  map_zero' := coe_zero
  map_add' := coe_add

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