enorm_map — Mathlib

English

If σ: R1 → R2 is an isometric ring homomorphism, then the extended nonnegative real norm is preserved: ‖σx‖ₑ = ‖x‖ₑ for all x ∈ R1.

Русский

Пусть σ: R1 → R2 — изометрический кольцевой однородник, тогда расширенная норма в ℝ≥0 сохраняется: ‖σx‖ₑ = ‖x‖ₑ для всех x ∈ R1.

LaTeX

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

Lean4

@[simp]
theorem enorm_map [SeminormedRing R₁] [SeminormedRing R₂] (σ : R₁ →+* R₂) [RingHomIsometric σ] (x : R₁) :
    ‖σ x‖ₑ = ‖x‖ₑ :=
  congrArg ENNReal.ofNNReal <| nnnorm_map σ x

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