nnnorm_map — Mathlib

English

For every f in the semilinear isometry class, the NN-norm is preserved: ‖f x‖₊ = ‖x‖₊ for all x.

Русский

Для любого f из класса семилинейной изометрии сохранение NN-нормы: ‖f x‖₊ = ‖x‖₊ для всех x.

LaTeX

$$$\|f x\|_{+} = \|x\|_{+}$$$

Lean4

theorem nnnorm_map [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (x : E) : ‖f x‖₊ = ‖x‖₊ :=
  NNReal.eq <| norm_map f x

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