norm_eq_sup — Mathlib

English

In a RegularNormedAlgebra setting, ‖x‖ = ‖x.fst‖ ⊔ ‖ algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd ‖.

Русский

В условиях RegularNormedAlgebra выполняется ‖x‖ = ‖x.fst‖ ⊔ ‖ algebraMap 𝕜 (End_K(A)) x.fst + mul 𝕜 A x.snd ‖.

LaTeX

$$$$\\|x\\| = \\max\\{\\|x.fst\\|,\\|\\mathrm{algebraMap}_{𝕜}(A \\to_L[𝕜] A)(x.fst) + mul_{𝕜} A\\ x.snd\\|\\}.$$$$

Lean4

/-- This is often the more useful lemma to rewrite the norm as opposed to `Unitization.norm_def`. -/
theorem norm_eq_sup (x : Unitization 𝕜 A) : ‖x‖ = ‖x.fst‖ ⊔ ‖algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd‖ := by
  rw [norm_def, splitMul_apply, Prod.norm_def]

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