# The completion of a metric space #

Completion of uniform spaces are already defined in `Topology.UniformSpace.Completion`. We show here that the uniform space completion of a metric space inherits a metric space structure, by extending the distance to the completion and checking that it is indeed a distance, and that it defines the same uniformity as the already defined uniform structure on the completion

source
instance UniformSpace.Completion.instDist {α : Type u} [PseudoMetricSpace α] :
Dist (Completion α)

The distance on the completion is obtained by extending the distance on the original space, by uniform continuity.

Equations

- UniformSpace.Completion.instDist = { dist := UniformSpace.Completion.extension₂ dist }

source
theorem UniformSpace.Completion.uniformContinuous_dist {α : Type u} [PseudoMetricSpace α] :
UniformContinuous fun (p : Completion α × Completion α) => dist p.1 p.2

The new distance is uniformly continuous.

source
theorem UniformSpace.Completion.continuous_dist {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f g : β → Completion α} (hf : Continuous f) (hg : Continuous g) :
Continuous fun (x : β) => dist (f x) (g x)

The new distance is continuous.

source
@[simp]
theorem UniformSpace.Completion.dist_eq {α : Type u} [PseudoMetricSpace α] (x y : α) :
dist ↑x ↑y = dist x y

The new distance is an extension of the original distance.

source
theorem UniformSpace.Completion.dist_self {α : Type u} [PseudoMetricSpace α] (x : Completion α) :
dist x x = 0
source
theorem UniformSpace.Completion.dist_comm {α : Type u} [PseudoMetricSpace α] (x y : Completion α) :
dist x y = dist y x
source
theorem UniformSpace.Completion.dist_triangle {α : Type u} [PseudoMetricSpace α] (x y z : Completion α) :
dist x z ≤ dist x y + dist y z
source
theorem UniformSpace.Completion.mem_uniformity_dist {α : Type u} [PseudoMetricSpace α] (s : Set (Completion α × Completion α)) :
s ∈ uniformity (Completion α) ↔ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Elements of the uniformity (defined generally for completions) can be characterized in terms of the distance.

source
theorem UniformSpace.Completion.uniformity_dist' {α : Type u} [PseudoMetricSpace α] :
uniformity (Completion α) = ⨅ (ε : { ε : ℝ // 0 < ε }), Filter.principal {p : Completion α × Completion α | dist p.1 p.2 < ↑ε}

Reformulate `Completion.mem_uniformity_dist` in terms that are suitable for the definition of the metric space structure.

source
theorem UniformSpace.Completion.uniformity_dist {α : Type u} [PseudoMetricSpace α] :
uniformity (Completion α) = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : Completion α × Completion α | dist p.1 p.2 < ε}
source
instance UniformSpace.Completion.instMetricSpace {α : Type u} [PseudoMetricSpace α] :
MetricSpace (Completion α)

Metric space structure on the completion of a pseudo_metric space.

Equations

- UniformSpace.Completion.instMetricSpace = MetricSpace.ofT0PseudoMetricSpace (UniformSpace.Completion α)

source
theorem UniformSpace.Completion.coe_isometry {α : Type u} [PseudoMetricSpace α] :
Isometry coe'

The embedding of a metric space in its completion is an isometry.

source
@[simp]
theorem UniformSpace.Completion.edist_eq {α : Type u} [PseudoMetricSpace α] (x y : α) :
edist ↑x ↑y = edist x y
source
instance UniformSpace.Completion.instIsBoundedSMul {α : Type u} [PseudoMetricSpace α] {M : Type u_1} [Zero M] [Zero α] [SMul M α] [PseudoMetricSpace M] [IsBoundedSMul M α] :
IsBoundedSMul M (Completion α)
source
theorem LipschitzWith.completion_extension {α : Type u} {β : Type v} [PseudoMetricSpace α] [MetricSpace β] [CompleteSpace β] {f : α → β} {K : NNReal} (h : LipschitzWith K f) :
LipschitzWith K (UniformSpace.Completion.extension f)
source
theorem LipschitzWith.completion_map {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {K : NNReal} (h : LipschitzWith K f) :
LipschitzWith K (UniformSpace.Completion.map f)
source
theorem Isometry.completion_extension {α : Type u} {β : Type v} [PseudoMetricSpace α] [MetricSpace β] [CompleteSpace β] {f : α → β} (h : Isometry f) :
Isometry (UniformSpace.Completion.extension f)
source
theorem Isometry.completion_map {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (h : Isometry f) :
Isometry (UniformSpace.Completion.map f)