nnnorm_toMul — Mathlib

English

Let E be a normed space. For every element x in the additive version of E, the nonnegative norm is preserved when viewed in E via the canonical additive-to-multiplicative identification. In symbols: ‖toMul(x)‖₊ = ‖x‖₊.

Русский

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

LaTeX

$$$\|\mathrm{toMul}(x)\|_{+} = \|x\|_{+}$$$

Lean4

@[simp]
theorem nnnorm_toMul (x : Additive E) : ‖(x.toMul : E)‖₊ = ‖x‖₊ :=
  rfl

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