Documentation

Mathlib.Analysis.Normed.Module.Completion

Normed space structure on the completion of a normed space #

If E is a normed space over 𝕜, then so is UniformSpace.Completion E. In this file we provide necessary instances and define UniformSpace.Completion.toComplₗᵢ - coercion E → UniformSpace.Completion E as a bundled linear isometry.

We also show that if A is a normed algebra over 𝕜, then so is UniformSpace.Completion A.

TODO: Generalise the results here from the concrete completion to any AbstractCompletion.

Embedding of a normed space to its completion as a linear isometry.

Equations
  • UniformSpace.Completion.toComplₗᵢ = { toFun := E, map_add' := , map_smul' := , norm_map' := }
Instances For
    @[simp]
    theorem UniformSpace.Completion.coe_toComplₗᵢ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
    UniformSpace.Completion.toComplₗᵢ = E

    Embedding of a normed space to its completion as a continuous linear map.

    Equations
    • UniformSpace.Completion.toComplL = UniformSpace.Completion.toComplₗᵢ.toContinuousLinearMap
    Instances For
      @[simp]
      theorem UniformSpace.Completion.coe_toComplL {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
      UniformSpace.Completion.toComplL = E
      @[simp]
      theorem UniformSpace.Completion.norm_toComplL {𝕜 : Type u_3} {E : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] :
      UniformSpace.Completion.toComplL = 1