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.
@[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] :
@[protected, instance]
noncomputable
def
uniform_space.completion.normed_space
(𝕜 : Type u_1)
(E : Type u_2)
[normed_field 𝕜]
[normed_group E]
[normed_space 𝕜 E] :
Equations
- uniform_space.completion.normed_space 𝕜 E = {to_module := {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul (uniform_space.completion.has_scalar 𝕜 E)}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}, norm_smul_le := _}
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
- uniform_space.completion.to_complₗᵢ = {to_linear_map := {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}, norm_map' := _}
@[simp]
theorem
uniform_space.completion.coe_to_complₗᵢ
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[normed_group E]
[normed_space 𝕜 E] :
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.
@[simp]
theorem
uniform_space.completion.coe_to_complL
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[normed_group E]
[normed_space 𝕜 E] :
@[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] :