# mathlibdocumentation

analysis.normed_space.completion

# Normed space structure on the completion of a normed space #

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

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

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

@[protected, instance]
@[protected, instance]
noncomputable def uniform_space.completion.normed_space (𝕜 : Type u_1) (E : Type u_2) [normed_field 𝕜] [ E] :
Equations
def uniform_space.completion.to_complₗᵢ {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] :

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

Equations
@[simp]
theorem uniform_space.completion.coe_to_complₗᵢ {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] :
noncomputable def uniform_space.completion.to_complL {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] :

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

Equations
@[simp]
theorem uniform_space.completion.coe_to_complL {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] :
@[simp]
theorem uniform_space.completion.norm_to_complL {𝕜 : Type u_1} {E : Type u_2} [ E] [nontrivial E] :
@[protected, instance]
noncomputable def uniform_space.completion.normed_ring (A : Type u_3)  :
Equations
@[protected, instance]
noncomputable def uniform_space.completion.normed_algebra (𝕜 : Type u_1) [normed_field 𝕜] (A : Type u_3) [ A]  :
Equations