Metrizable uniform spaces

In this file we prove that a uniform space with countably generated uniformity filter is pseudometrizable: there exists a PseudoMetricSpace structure that generates the same uniformity. The proof follows Sergey Melikhov, Metrizable uniform spaces.

Main definitions

• PseudoMetricSpace.ofPreNNDist: given a function d : X → X → ℝ≥0 such that d x x = 0 and d x y = d y x for all x y : X, constructs the maximal pseudo metric space structure such that NNDist x y ≤ d x y for all x y : X.

• UniformSpace.pseudoMetricSpace: given a uniform space X with countably generated 𝓤 X, constructs a PseudoMetricSpace X instance that is compatible with the uniform space structure.

• UniformSpace.metricSpace: given a T₀ uniform space X with countably generated 𝓤 X, constructs a MetricSpace X instance that is compatible with the uniform space structure.

Main statements

• UniformSpace.metrizable_uniformity: if X is a uniform space with countably generated 𝓤 X, then there exists a PseudoMetricSpace structure that is compatible with this UniformSpace structure. Use UniformSpace.pseudoMetricSpace or UniformSpace.metricSpace instead.

• UniformSpace.pseudoMetrizableSpace: a uniform space with countably generated 𝓤 X is pseudo metrizable.

• UniformSpace.metrizableSpace: a T₀ uniform space with countably generated 𝓤 X is metrizable. This is not an instance to avoid loops.

Tags

metrizable space, uniform space

noncomputable def PseudoMetricSpace.ofPreNNDist {X : Type u_1} (d : X → X → NNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) : PseudoMetricSpace X

The maximal pseudo metric space structure on X such that dist x y ≤ d x y for all x y, where d : X → X → ℝ≥0 is a function such that d x x = 0 and d x y = d y x for all x, y.

Equations

• One or more equations did not get rendered due to their size.

theorem PseudoMetricSpace.dist_ofPreNNDist {X : Type u_1} (d : X → X → NNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) (x y : X) : dist x y = ↑(⨅ (l : List X), (List.zipWith d (x :: l) (l ++ [y])).sum)

theorem PseudoMetricSpace.dist_ofPreNNDist_le {X : Type u_1} (d : X → X → NNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) (x y : X) : dist x y ≤ ↑(d x y)

theorem PseudoMetricSpace.le_two_mul_dist_ofPreNNDist {X : Type u_1} (d : X → X → NNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) (hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * (d x₁ x₂ ⊔ (d x₂ x₃ ⊔ d x₃ x₄))) (x y : X) : ↑(d x y) ≤ 2 * dist x y

Consider a function d : X → X → ℝ≥0 such that d x x = 0 and d x y = d y x for all x, y. Let dist be the largest pseudometric distance such that dist x y ≤ d x y, see PseudoMetricSpace.ofPreNNDist. Suppose that d satisfies the following triangle-like inequality: d x₁ x₄ ≤ 2 * max (d x₁ x₂, d x₂ x₃, d x₃ x₄). Then d x y ≤ 2 * dist x y for all x, y.

theorem UniformSpace.metrizable_uniformity (X : Type u_2) [UniformSpace X] [(uniformity X).IsCountablyGenerated] : ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst✝

If X is a uniform space with countably generated uniformity filter, there exists a PseudoMetricSpace structure compatible with the UniformSpace structure. Use UniformSpace.pseudoMetricSpace or UniformSpace.metricSpace instead.

noncomputable def UniformSpace.pseudoMetricSpace (X : Type u_2) [UniformSpace X] [(uniformity X).IsCountablyGenerated] : PseudoMetricSpace X

A PseudoMetricSpace instance compatible with a given UniformSpace structure.

Equations

• UniformSpace.pseudoMetricSpace X = ⋯.choose.replaceUniformity ⋯

noncomputable def UniformSpace.metricSpace (X : Type u_2) [UniformSpace X] [(uniformity X).IsCountablyGenerated] [T0Space X] : MetricSpace X

A MetricSpace instance compatible with a given UniformSpace structure.

Equations

• UniformSpace.metricSpace X = MetricSpace.ofT0PseudoMetricSpace X

@[instance 100]

instance UniformSpace.pseudoMetrizableSpace {X : Type u_1} [UniformSpace X] [(uniformity X).IsCountablyGenerated] : TopologicalSpace.PseudoMetrizableSpace X

A uniform space with countably generated 𝓤 X is pseudo metrizable.

theorem UniformSpace.metrizableSpace {X : Type u_1} [UniformSpace X] [(uniformity X).IsCountablyGenerated] [T0Space X] : TopologicalSpace.MetrizableSpace X

A T₀ uniform space with countably generated 𝓤 X is metrizable. This is not an instance to avoid loops.

theorem TotallyBounded.isSeparable {X : Type u_1} [UniformSpace X] [i : (uniformity X).IsCountablyGenerated] {s : Set X} (h : TotallyBounded s) : TopologicalSpace.IsSeparable s

A totally bounded set is separable in countably generated uniform spaces. This can be obtained from the more general EMetric.subset_countable_closure_of_almost_dense_set.

@[instance 100]

instance DiscreteTopology.metrizableSpace {α : Type u_2} [TopologicalSpace α] [DiscreteTopology α] : TopologicalSpace.MetrizableSpace α