mathlib3 documentation

topology.metric_space.completion

The completion of a metric space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Completion of uniform spaces are already defined in topology.uniform_space.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
@[protected, instance]
noncomputable def uniform_space.completion.has_dist {α : Type u} [pseudo_metric_space α] :
has_dist (uniform_space.completion α)

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

Equations
source
@[protected]
theorem uniform_space.completion.uniform_continuous_dist {α : Type u} [pseudo_metric_space α] :
uniform_continuous (λ (p : uniform_space.completion α × uniform_space.completion α), has_dist.dist p.fst p.snd)

The new distance is uniformly continuous.

source
@[protected]
theorem uniform_space.completion.continuous_dist {α : Type u} {β : Type v} [pseudo_metric_space α] [topological_space β] {f g : β → uniform_space.completion α} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : β), has_dist.dist (f x) (g x))

The new distance is continuous.

source
@[protected, simp]
theorem uniform_space.completion.dist_eq {α : Type u} [pseudo_metric_space α] (x y : α) :
has_dist.dist ↑x ↑y = has_dist.dist x y

The new distance is an extension of the original distance.

source
@[protected]
theorem uniform_space.completion.dist_self {α : Type u} [pseudo_metric_space α] (x : uniform_space.completion α) :
has_dist.dist x x = 0
source
@[protected]
theorem uniform_space.completion.dist_comm {α : Type u} [pseudo_metric_space α] (x y : uniform_space.completion α) :
has_dist.dist x y = has_dist.dist y x
source
@[protected]
theorem uniform_space.completion.dist_triangle {α : Type u} [pseudo_metric_space α] (x y z : uniform_space.completion α) :
has_dist.dist x z ≤ has_dist.dist x y + has_dist.dist y z
source
@[protected]
theorem uniform_space.completion.mem_uniformity_dist {α : Type u} [pseudo_metric_space α] (s : set (uniform_space.completion α × uniform_space.completion α)) :
s ∈ uniformity (uniform_space.completion α) ↔ ∃ (ε : ℝ) (H : ε > 0), ∀ {a b : uniform_space.completion α}, has_dist.dist a b < ε → (a, b) ∈ s

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

source
@[protected]
theorem uniform_space.completion.eq_of_dist_eq_zero {α : Type u} [pseudo_metric_space α] (x y : uniform_space.completion α) (h : has_dist.dist x y = 0) :
x = y

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

source
@[protected]
theorem uniform_space.completion.uniformity_dist' {α : Type u} [pseudo_metric_space α] :
uniformity (uniform_space.completion α) = ⨅ (ε : {ε // 0 < ε}), filter.principal {p : uniform_space.completion α × uniform_space.completion α | has_dist.dist p.fst p.snd < ε.val}

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

source
@[protected]
theorem uniform_space.completion.uniformity_dist {α : Type u} [pseudo_metric_space α] :
uniformity (uniform_space.completion α) = ⨅ (ε : ℝ) (H : ε > 0), filter.principal {p : uniform_space.completion α × uniform_space.completion α | has_dist.dist p.fst p.snd < ε}
source
@[protected, instance]
noncomputable def uniform_space.completion.metric_space {α : Type u} [pseudo_metric_space α] :
metric_space (uniform_space.completion α)

Metric space structure on the completion of a pseudo_metric space.

Equations
source
theorem uniform_space.completion.coe_isometry {α : Type u} [pseudo_metric_space α] :
isometry coe

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

source
@[protected, simp]
theorem uniform_space.completion.edist_eq {α : Type u} [pseudo_metric_space α] (x y : α) :
has_edist.edist ↑x ↑y = has_edist.edist x y