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

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

We also show that if `A` is a normed algebra over `𝕜`, then so is `UniformSpace.Completion A`.

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

source
instance UniformSpace.Completion.instNormedSpace (𝕜 : Type u_1) (E : Type u_2) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
NormedSpace 𝕜 (Completion E)
Equations

- UniformSpace.Completion.instNormedSpace 𝕜 E = { toModule := UniformSpace.Completion.instModule, norm_smul_le := ⋯ }

source
def UniformSpace.Completion.toComplₗᵢ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
E →ₗᵢ[𝕜] Completion E

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

Equations

- UniformSpace.Completion.toComplₗᵢ = { toFun := UniformSpace.Completion.coe', map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem UniformSpace.Completion.coe_toComplₗᵢ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
⇑toComplₗᵢ = coe'
source
def UniformSpace.Completion.toComplL {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
E →L[𝕜] Completion E

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

Equations

- UniformSpace.Completion.toComplL = UniformSpace.Completion.toComplₗᵢ.toContinuousLinearMap

Instances For

source
@[simp]
theorem UniformSpace.Completion.coe_toComplL {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
⇑toComplL = coe'
source
@[simp]
theorem UniformSpace.Completion.norm_toComplL {𝕜 : Type u_3} {E : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] :
‖toComplL‖ = 1
source
instance UniformSpace.Completion.instNormedRing (A : Type u_3) [SeminormedRing A] :
NormedRing (Completion A)
Equations

- One or more equations did not get rendered due to their size.

source
instance UniformSpace.Completion.instNormedCommRing (A : Type u_3) [SeminormedCommRing A] :
NormedCommRing (Completion A)
Equations

- One or more equations did not get rendered due to their size.

source
instance UniformSpace.Completion.instNormedAlgebra (𝕜 : Type u_1) (A : Type u_3) [NormedField 𝕜] [SeminormedCommRing A] [NormedAlgebra 𝕜 A] :
NormedAlgebra 𝕜 (Completion A)
Equations

- UniformSpace.Completion.instNormedAlgebra 𝕜 A = { toAlgebra := UniformSpace.Completion.algebra A 𝕜, norm_smul_le := ⋯ }

source
instance UniformSpace.Completion.instNormedFieldOfCompletableTopField (A : Type u_3) [NormedField A] [CompletableTopField A] :
NormedField (Completion A)
Equations

- One or more equations did not get rendered due to their size.