mathlib documentation

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.

def uniform_space.completion.to_complₗᵢ {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] :

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_group E] [normed_space 𝕜 E] :

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

Equations
@[simp]