norm_toComplL — Mathlib

English

The operator norm of the embedding toComplL is equal to 1 (alternative formulation).

Русский

Нормa оператора вложения toComplL равна 1 (альтернативная формулировка).

LaTeX

$$\|toComplL\| = 1$$

Lean4

@[simp]
theorem norm_toComplL {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [Nontrivial E] : ‖(toComplL : E →L[𝕜] Completion E)‖ = 1 :=
  (toComplₗᵢ : E →ₗᵢ[𝕜] Completion E).norm_toContinuousLinearMap

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