nnnormHom — Mathlib

English

The NNReal norm defines a MonoidWithZeroHom from α to ℝ≥0, with toFun = ‖·‖₊, preserving zero, one, and multiplication.

Русский

NNReal-норма задаёт моноидально-нулевой гомоморфизм, где toFun = ‖·‖₊ и сохраняются 0, 1 и умножение.

LaTeX

$$$\\text{nnnormHom}:\\ α \\to_*^0 ℝ_{≥0}$ with \\toFun(x)=\\|x\\|_{+},\\; \\text{map_zero}'=\\text{nnnorm_zero},\\; \\text{map_one}'=\\text{nnnorm_one},\\; \\text{map_mul}'=\\text{nnnorm_mul}$$$

Lean4

/-- `nnnorm` as a `MonoidWithZeroHom`. -/
@[simps]
def nnnormHom : α →*₀ ℝ≥0 where
  toFun := (‖·‖₊)
  map_zero' := nnnorm_zero
  map_one' := nnnorm_one
  map_mul' := nnnorm_mul

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