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

@[implicit_reducible]

noncomputable 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 }

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

The new distance is uniformly continuous.

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.

@[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 : Completion α) : dist x x = 0

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

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

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.

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.

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

@[implicit_reducible]

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

Metric space structure on the completion of a PseudoMetric space.

Equations

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

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

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

instance UniformSpace.Completion.instIsBoundedSMul {α : Type u} [PseudoMetricSpace α] {M : Type u_1} [Zero M] [Zero α] [SMul M α] [PseudoMetricSpace M] [IsBoundedSMul M α] : IsBoundedSMul M (Completion α)

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 α] [PseudoMetricSpace β] [CompleteSpace β] [T0Space β] {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)

noncomputable def Isometry.extensionHom {α : Type u} {β : Type v} [PseudoMetricSpace α] [Ring α] [IsTopologicalRing α] [IsUniformAddGroup α] [Ring β] [PseudoMetricSpace β] [IsUniformAddGroup β] [IsTopologicalRing β] [CompleteSpace β] [T0Space β] {f : α →+* β} (h : Isometry ⇑f) : UniformSpace.Completion α →+* β

The extension of an isometry to the completion of the domain.

Equations

• h.extensionHom = UniformSpace.Completion.extensionHom f ⋯

@[simp]

theorem Isometry.extensionHom_coe {α : Type u} {β : Type v} [PseudoMetricSpace α] [Ring α] [IsTopologicalRing α] [IsUniformAddGroup α] [Ring β] [PseudoMetricSpace β] [IsUniformAddGroup β] [IsTopologicalRing β] [CompleteSpace β] [T0Space β] {f : α →+* β} (h : Isometry ⇑f) (x : α) : h.extensionHom ↑x = f x

noncomputable def Isometry.mapRingHom {α : Type u} {β : Type v} [PseudoMetricSpace α] [Ring α] [IsTopologicalRing α] [IsUniformAddGroup α] [Ring β] [PseudoMetricSpace β] [IsUniformAddGroup β] [IsTopologicalRing β] {f : α →+* β} (h : Isometry ⇑f) : UniformSpace.Completion α →+* UniformSpace.Completion β

The lift of an isometry to completions.

Equations

• h.mapRingHom = UniformSpace.Completion.mapRingHom f ⋯

theorem Isometry.mapRingHom_coe {α : Type u} {β : Type v} [PseudoMetricSpace α] [Ring α] [IsTopologicalRing α] [IsUniformAddGroup α] [Ring β] [PseudoMetricSpace β] [IsUniformAddGroup β] [IsTopologicalRing β] {f : α →+* β} (h : Isometry ⇑f) (x : α) : h.mapRingHom ↑x = ↑(f x)

theorem Isometry.isometry_mapRingHom {α : Type u} {β : Type v} [PseudoMetricSpace α] [Ring α] [IsTopologicalRing α] [IsUniformAddGroup α] [Ring β] [PseudoMetricSpace β] [IsUniformAddGroup β] [IsTopologicalRing β] {f : α →+* β} (h : Isometry ⇑f) : Isometry ⇑h.mapRingHom