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.

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

Equations

• ⋯ = ⋯

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.

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

• UniformSpace.Completion.toComplₗᵢ = let __src := UniformSpace.Completion.toCompl; { toLinearMap := { toAddHom := { toFun := ↑E, map_add' := ⋯ }, map_smul' := ⋯ }, norm_map' := ⋯ }

@[simp]

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

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ₗᵢ

@[simp]

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

@[simp]

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

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.

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.