UniformSpace.Completion.dist_eq
theorem UniformSpace.Completion.dist_eq :
∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), dist (↑α x) (↑α y) = dist x y
The theorem `UniformSpace.Completion.dist_eq` states that for any type `α` that has a `PseudoMetricSpace` instance (that is, `α` forms a pseudometric space), and for any two elements `x` and `y` of this type, the distance between the completions of `x` and `y` (denoted as `↑α x` and `↑α y`) is equal to the distance between `x` and `y` themselves. In other words, the distance function in the completion of the space extends the original distance function in the pseudometric space.
More concisely: For any pseudometric space (α, d), the completion distances ↑α(x, y) equal the original distances d(x, y) for all x, y ∈ α.
|
UniformSpace.Completion.uniformContinuous_dist
theorem UniformSpace.Completion.uniformContinuous_dist :
∀ {α : Type u} [inst : PseudoMetricSpace α], UniformContinuous fun p => dist p.1 p.2
The theorem states that in the context of a pseudo metric space `α`, the distance function, which takes a pair of points and returns the distance between them, is uniformly continuous. This means that, as the pair of points `(p.1, p.2)` gets arbitrarily close together (tends to the diagonal), the distance between the points `dist p.1 p.2` also gets arbitrarily close. This holds true no matter where the points `p.1` and `p.2` are located in the pseudo metric space `α`.
More concisely: In a pseudo metric space, the distance function is uniformly continuous.
|
UniformSpace.Completion.mem_uniformity_dist
theorem UniformSpace.Completion.mem_uniformity_dist :
∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set (UniformSpace.Completion α × UniformSpace.Completion α)),
s ∈ uniformity (UniformSpace.Completion α) ↔
∃ ε > 0, ∀ {a b : UniformSpace.Completion α}, dist a b < ε → (a, b) ∈ s
This theorem is about the uniformity in the context of the completion of a pseudo metric space. It states that for any set of pairs of elements in the completion of a pseudo metric space, the set belongs to the uniformity of the completion if and only if there exists a positive real number ε such that for any pair of elements in the completion, if the distance between these elements is less than ε, then this pair is in the set.
More concisely: A set of pairs in the completion of a pseudo metric space belongs to its uniformity if and only if it contains all pairs of elements with distance less than some positive real number.
|
UniformSpace.Completion.uniformity_dist'
theorem UniformSpace.Completion.uniformity_dist' :
∀ {α : Type u} [inst : PseudoMetricSpace α],
uniformity (UniformSpace.Completion α) = ⨅ ε, Filter.principal {p | dist p.1 p.2 < ↑ε}
The theorem `UniformSpace.Completion.uniformity_dist'` states that for any type `α` with a `PseudoMetricSpace` structure, the uniformity on the Hausdorff completion of `α` is equivalent to the infimum of all principal filters of sets, where each set consists of pairs whose distance is less than a positive real number `ε`. This theorem is a reformulation of `Completion.mem_uniformity_dist`, designed to be suitable for defining the metrics space structure.
More concisely: The uniformity on the Hausdorff completion of a pseudometric space is equivalent to the infimum of all filters of pairs with distance less than a positive real number.
|
UniformSpace.Completion.coe_isometry
theorem UniformSpace.Completion.coe_isometry : ∀ {α : Type u} [inst : PseudoMetricSpace α], Isometry ↑α
The theorem states that the embedding of a pseudometric space into its completion is an isometry. In other words, for any pseudometric space `α`, the function that embeds `α` into its completion preserves the extended distance (`edist`) between any two points. This means that the extended distance between any two points in `α` is the same as the extended distance between their images in the completion of `α`.
More concisely: The embedding of a pseudometric space into its completion preserves extended distances, i.e., for any pseudometric spaces `α`, the extended distance between any two points in `α` equals the extended distance between their images in the completion of `α`.
|
UniformSpace.Completion.continuous_dist
theorem UniformSpace.Completion.continuous_dist :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β]
{f g : β → UniformSpace.Completion α}, Continuous f → Continuous g → Continuous fun x => dist (f x) (g x)
This theorem states that the distance function in the Hausdorff completion of a given type `α` is continuous. More specifically, given any two types `α` and `β` where `α` is a pseudo metric space and `β` is a topological space, if we have two functions `f` and `g` mapping from `β` to the Hausdorff completion of `α` which are continuous, then a function that takes an input from `β` and returns the distance between `f` and `g` at that input is also continuous. The Hausdorff completion of `α` is defined as the separation quotient of the Cauchy filters on `α`.
More concisely: Given two continuous functions from a topological space `β` to the Hausdorff completion of a pseudo metric space `α`, the function that maps an input in `β` to the distance between the image of that input under each function is also continuous.
|
UniformSpace.Completion.eq_of_dist_eq_zero
theorem UniformSpace.Completion.eq_of_dist_eq_zero :
∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : UniformSpace.Completion α), dist x y = 0 → x = y
This theorem states that in the Hausdorff completion of a given type `α` that is also a pseudometric space, if the distance between two elements `x` and `y` is zero, then `x` is equal to `y`. In other words, in this specific completion of a pseudometric space, there are no two distinct elements that have zero distance between them.
More concisely: In the Hausdorff completion of a pseudometric space, two equal elements have zero distance.
|