nnnorm_ofMul — Mathlib

English

Let E be a normed space. For every x in E, the nnreal norm is preserved under the embedding of E into its multiplicative form via ofMul. In symbols: ‖ofMul(x)‖₊ = ‖x‖₊.

Русский

Пусть E — нормированное пространство. Для каждого x ∈ E нормa-неотрицательная сохраняется при отображении в мультипликативную форму через ofMul: ‖ofMul(x)‖₊ = ‖x‖₊.

LaTeX

$$$‖ofMul\,x‖₊ = ‖x‖₊$$$

Lean4

@[simp]
theorem nnnorm_ofMul (x : E) : ‖ofMul x‖₊ = ‖x‖₊ :=
  rfl

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