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]
:
Equations
- (_ : UniformContinuousConstSMul 𝕜 E) = (_ : UniformContinuousConstSMul 𝕜 E)
instance
UniformSpace.Completion.instNormedSpaceCompletionToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupInstNormedAddCommGroupCompletionToUniformSpaceToPseudoMetricSpace
(𝕜 : Type u_1)
(E : Type u_2)
[NormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 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]
:
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
@[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]
:
Embedding of a normed space to its completion as a continuous linear map.
Equations
- UniformSpace.Completion.toComplL = LinearIsometry.toContinuousLinearMap UniformSpace.Completion.toComplₗᵢ
Instances For
@[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]
:
instance
UniformSpace.Completion.instNormedRingCompletionToUniformSpaceToPseudoMetricSpace
(A : Type u_3)
[SeminormedRing 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]
:
Equations
- One or more equations did not get rendered due to their size.