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

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

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

Equations

• UniformSpace.Completion.instDistCompletionToUniformSpace = { dist := UniformSpace.Completion.extension₂ dist }

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

The new distance is uniformly continuous.

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

The new distance is continuous.

@[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.

theorem UniformSpace.Completion.dist_self {α : Type u} [PseudoMetricSpace α] (x : UniformSpace.Completion α) : dist x x = 0

theorem UniformSpace.Completion.dist_comm {α : Type u} [PseudoMetricSpace α] (x : UniformSpace.Completion α) (y : UniformSpace.Completion α) : dist x y = dist y x

theorem UniformSpace.Completion.dist_triangle {α : Type u} [PseudoMetricSpace α] (x : UniformSpace.Completion α) (y : UniformSpace.Completion α) (z : UniformSpace.Completion α) : dist x z ≤ dist x y + dist y z

theorem UniformSpace.Completion.mem_uniformity_dist {α : Type u} [PseudoMetricSpace α] (s : Set (UniformSpace.Completion α × UniformSpace.Completion α)) : s ∈ uniformity (UniformSpace.Completion α) ↔ ∃ ε > 0, ∀ {a b : UniformSpace.Completion α}, dist a b < ε → (a, b) ∈ s

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

theorem UniformSpace.Completion.eq_of_dist_eq_zero {α : Type u} [PseudoMetricSpace α] (x : UniformSpace.Completion α) (y : UniformSpace.Completion α) (h : dist x y = 0) : x = y

If two points are at distance 0, then they coincide.

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

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

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

instance UniformSpace.Completion.instMetricSpace {α : Type u} [PseudoMetricSpace α] : MetricSpace (UniformSpace.Completion α)

Metric space structure on the completion of a pseudo_metric space.

Equations

• UniformSpace.Completion.instMetricSpace = MetricSpace.mk (_ : ∀ {x y : UniformSpace.Completion α}, dist x y = 0 → x = y)

theorem UniformSpace.Completion.coe_isometry {α : Type u} [PseudoMetricSpace α] : Isometry ↑α

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

@[simp]

theorem UniformSpace.Completion.edist_eq {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : edist (↑α x) (↑α y) = edist x y

theorem LipschitzWith.completion_extension {α : Type u} {β : Type v} [PseudoMetricSpace α] [MetricSpace β] [CompleteSpace β] {f : α → β} {K : NNReal} (h : LipschitzWith K f) : LipschitzWith K (UniformSpace.Completion.extension f)

theorem LipschitzWith.completion_map {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {K : NNReal} (h : LipschitzWith K f) : LipschitzWith K (UniformSpace.Completion.map f)

theorem Isometry.completion_extension {α : Type u} {β : Type v} [PseudoMetricSpace α] [MetricSpace β] [CompleteSpace β] {f : α → β} (h : Isometry f) : Isometry (UniformSpace.Completion.extension f)

theorem Isometry.completion_map {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (h : Isometry f) : Isometry (UniformSpace.Completion.map f)