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.NormedSpace.to_uniformContinuousConstSMul (𝕜 : Type u_1) (E : Type u_2) [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] :

UniformContinuousConstSMul 𝕜 E

Equations

UniformSpace.Completion.NormedSpace.to_uniformContinuousConstSMul = UniformSpace.Completion.NormedSpace.to_uniformContinuousConstSMul.proof_1

source

instance UniformSpace.Completion.instNormedSpaceCompletionToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupInstNormedAddCommGroupCompletionToUniformSpaceToPseudoMetricSpace (𝕜 : Type u_1) (E : Type u_2) [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] :

NormedSpace 𝕜 (UniformSpace.Completion E)

Equations

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

source

def UniformSpace.Completion.toComplₗᵢ {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] :

E →ₗᵢ[𝕜] UniformSpace.Completion E

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

Equations

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

Instances For

source

@[simp]

theorem UniformSpace.Completion.coe_toComplₗᵢ {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] :

↑UniformSpace.Completion.toComplₗᵢ = ↑E

source

def UniformSpace.Completion.toComplL {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] :

E →L[𝕜] UniformSpace.Completion E

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

Equations

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

Instances For

source

@[simp]

theorem UniformSpace.Completion.coe_toComplL {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] :

↑UniformSpace.Completion.toComplL = ↑E

source

@[simp]

theorem UniformSpace.Completion.norm_toComplL {𝕜 : Type u_3} {E : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] :

‖UniformSpace.Completion.toComplL‖ = 1

source

instance UniformSpace.Completion.instNormedRingCompletionToUniformSpaceToPseudoMetricSpace (A : Type u_3) [SeminormedRing A] :

NormedRing (UniformSpace.Completion A)

Equations

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

source

instance UniformSpace.Completion.instNormedAlgebraCompletionToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedRingInstNormedRingCompletionToUniformSpaceToPseudoMetricSpace (𝕜 : Type u_1) [NormedField 𝕜] (A : Type u_3) [SeminormedCommRing A] [NormedAlgebra 𝕜 A] [UniformContinuousConstSMul 𝕜 A] :

NormedAlgebra 𝕜 (UniformSpace.Completion A)

Equations

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