PseudoMetricSpace.le_two_mul_dist_ofPreNNDist
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),
(∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))) →
∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
The theorem `PseudoMetricSpace.le_two_mul_dist_ofPreNNDist` states that for any type `X` and a function `d` from `X` to `X` that outputs nonnegative real numbers (`NNReal`), satisfying the properties that `d x x` equals 0 and `d x y` equals `d y x` for all `x` and `y` in `X`, and a triangle-like inequality that `d` of `x₁` and `x₄` is less than or equal to two times the maximum of `d x₁ x₂`, `d x₂ x₃`, and `d x₃ x₄` for any `x₁`, `x₂`, `x₃`, and `x₄` in `X`. Then, the distance `d x y` is less than or equal to two times the pseudometric distance between `x` and `y` for all `x` and `y` in `X`, where the pseudometric distance is defined as the largest distance satisfying `dist x y ≤ d x y`.
More concisely: If `d` is a function from a type `X` to non-negative real numbers satisfying the properties of a pseudo-metric, then for all `x, y` in `X`, the distance `d(x, y)` is less than or equal to twice the pseudo-metric distance between `x` and `y`.
|
UniformSpace.metrizable_uniformity
theorem UniformSpace.metrizable_uniformity :
∀ (X : Type u_2) [inst : UniformSpace X] [inst_1 : (uniformity X).IsCountablyGenerated],
∃ I, PseudoMetricSpace.toUniformSpace = inst
This theorem states that if `X` is a uniform space and its uniformity filter is countably generated, then there exists a pseudometric space structure that is compatible with the uniform space structure on `X`. This theorem provides a way to induce a pseudometric space structure from a uniform space structure, under certain conditions. However, the theorem also suggests that it's better to use `UniformSpace.pseudoMetricSpace` or `UniformSpace.metricSpace` for this purpose.
More concisely: If a uniform space `X` has a countably generated uniformity filter, then it admits a compatible pseudometric.
|
UniformSpace.metrizableSpace
theorem UniformSpace.metrizableSpace :
∀ {X : Type u_1} [inst : UniformSpace X] [inst_1 : (uniformity X).IsCountablyGenerated] [inst_2 : T0Space X],
TopologicalSpace.MetrizableSpace X
The theorem `UniformSpace.metrizableSpace` states that for any type `X` equipped with a `UniformSpace` structure, given that the uniformity `𝓤 X` is countably generated and `X` is a `T0Space` (a topological space where for any two distinct points there exists a neighborhood of one that does not contain the other), then `X` is a `MetrizableSpace` (a topological space that is homeomorphic to some metric space). This theorem is not an instance to avoid producing loops in instance search.
More concisely: If a uniform space X is T0 and its uniformity is countably generated, then X is metrizable.
|