nnnorm_map' — Mathlib

English

For a suitable isometry-like structure, the NNNorm of f(x) equals the NNNorm of x.

Русский

Для соответствующей структуры изометрии NNNorm сохраняется: ‖f(x)‖₊ = ‖x‖₊.

LaTeX

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

Lean4

@[to_additive (attr := simp) nnnorm_map]
theorem nnnorm_map' [FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) (x : E) : ‖f x‖₊ = ‖x‖₊ :=
  NNReal.eq <| norm_map' f x

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