coeFnAddMonoidHom — Mathlib

English

The evaluation map that sends a seminorm to its function x ↦ p(x) is an AddMonoidHom from Seminorm 𝕜 E to the space of functions E → ℝ.

Русский

Оценочная карта, отправляющая полунорму на отображение p: E → ℝ, является гомоморфизмом аддитивных моноидов.

LaTeX

$$$ \text{coeFnAddMonoidHom}: \ Seminorm 𝕜 E \to AddMonoidHom( E, \mathbb{R} ) \quad\text{with}\quad (p)\mapsto (x \mapsto p(x))$$$

Lean4

/-- `coeFn` as an `AddMonoidHom`. Helper definition for showing that `Seminorm 𝕜 E` is a module. -/
@[simps]
def coeFnAddMonoidHom : AddMonoidHom (Seminorm 𝕜 E) (E → ℝ)
    where
  toFun := (↑)
  map_zero' := coe_zero
  map_add' := coe_add

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