nnnorm_ofAdd — Mathlib

English

For any x in E, the nnreal norm is preserved when mapping Additive E to NNReal via the natural correspondence. In symbols: ‖ofAdd x‖₊ = ‖x‖₊.

Русский

Для любого x ∈ E норма-неотрицательная сохраняется при отображении Additive E в NNReal через каноническое соответствие: ‖ofAdd x‖₊ = ‖x‖₊.

LaTeX

$$$‖ofAdd\,x‖_{+} = ‖x‖_{+}$$$

Lean4

@[simp]
theorem nnnorm_ofAdd (x : E) : ‖ofAdd x‖₊ = ‖x‖₊ :=
  rfl

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