nnnorm_toAdd — Mathlib

English

For any x in the multiplicative version of E, the nnreal norm is preserved when viewing x as an additive element. In symbols: ‖x.toAdd‖₊ = ‖x‖₊.

Русский

Для любого x из мультипликативной структуры E нормa-неотрицательная сохраняется при переходе к аддитивной структуре: ‖x.toAdd‖₊ = ‖x‖₊.

LaTeX

$$$‖x^{\mathrm{toAdd}}‖_{+} = ‖x‖_{+}$$$

Lean4

@[simp]
theorem nnnorm_toAdd (x : Multiplicative E) : ‖(x.toAdd : E)‖₊ = ‖x‖₊ :=
  rfl

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