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.

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

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

Equations
source
@[simp]
theorem uniform_space.completion.coe_to_complₗᵢ {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] :
⇑uniform_space.completion.to_complₗᵢ = coe
source
noncomputable def uniform_space.completion.to_complL {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] :
E →L[𝕜] uniform_space.completion E

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

Equations
source
@[simp]
theorem uniform_space.completion.coe_to_complL {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] :
⇑uniform_space.completion.to_complL = coe
source
@[simp]
theorem uniform_space.completion.norm_to_complL {𝕜 : Type u_1} {E : Type u_2} [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [nontrivial E] :
∥uniform_space.completion.to_complL∥ = 1