nnnorm_ofDual — Mathlib

English

For any x in Eᵒᵈ, the nnreal norm coincides with the nnreal norm of its image under the dual-to- NNReal correspondence, i.e., ‖ofDual x‖₊ = ‖x‖₊.

Русский

Для любого x ∈ Eᵒᵈ нормa nnreal совпадает с нормой образа через соответствие двойственности и NNReal: ‖ofDual x‖₊ = ‖x‖₊.

LaTeX

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

Lean4

@[simp]
theorem nnnorm_ofDual (x : Eᵒᵈ) : ‖ofDual x‖₊ = ‖x‖₊ :=
  rfl

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