toComplₗᵢ — Mathlib

English

There is a canonical embedding of a normed space E into its completion, realized as a linear isometry.

Русский

Существует каноническое вложение нормированного пространства E в его завершение, реализованное как линейное изометрическое отображение.

LaTeX

$$toCompl\_l i : E \to \mathrm{Completion}(E) is a linear isometry$$

Lean4

/-- Embedding of a normed space to its completion as a linear isometry. -/
def toComplₗᵢ : E →ₗᵢ[𝕜] Completion E :=
  { toCompl with
    toFun := (↑)
    map_smul' := coe_smul
    norm_map' := norm_coe }

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