nnnorm_eq_sup — Mathlib

English

Similarly, ‖x‖₊ = max{‖x.fst‖₊, ‖ algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd ‖₊}.

Русский

Аналогично, ‖x‖₊ = max{‖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.nnnorm_def`. -/
theorem nnnorm_eq_sup (x : Unitization 𝕜 A) : ‖x‖₊ = ‖x.fst‖₊ ⊔ ‖algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd‖₊ :=
  NNReal.eq <| norm_eq_sup x

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