nnnorm_map — Mathlib

English

Let σ: R1 → R2 be a ring homomorphism that is isometric with respect to the given norms. Then for every x ∈ R1, the norm of σ(x) equals the norm of x when measured in the appropriate norm (NNReal).

Русский

Пусть σ: R1 → R2 — кольцевой однопеременный гомоморфизм, сохраняющий норму. Тогда для каждого x ∈ R1 нормa σ(x) равна нормe x (в соответствующей норме NNReal).

LaTeX

$$$‖σx‖_{+} = ‖x‖_{+}$$$

Lean4

@[simp]
theorem nnnorm_map [SeminormedRing R₁] [SeminormedRing R₂] (σ : R₁ →+* R₂) [RingHomIsometric σ] (x : R₁) :
    ‖σ x‖₊ = ‖x‖₊ :=
  NNReal.eq norm_map

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