mathlib3 documentation

analysis.normed_space.completion

Normed space structure on the completion of a normed space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

Equations
noncomputable def uniform_space.completion.to_complL {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :

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

Equations