Characterizing uniformities associated to a (generalized) distance function D in terms of the elements of the uniformity.

Creating a uniform space from an extended distance.

Extended metric spaces, with an extended distance edist possibly taking the value ∞

Each emetric space induces a canonical uniform_space and hence a canonical topological_space. This is enforced in the type class definition, by extending the uniform_space structure. When instantiating an emetric_space structure, the uniformity fields are not necessary, they will be filled in by default. There is a default value for the uniformity, that can be substituted in cases of interest, for instance when instantiating an emetric_space structure on a product.

Continuity of edist is finally proving in topology.instances.ennreal

Characterize the equality of points by the vanishing of their extended distance

Triangle inequality for the extended distance

Two points coincide if their distance is < ε for all positive ε

Reformulation of the uniform structure in terms of the extended distance

Reformulation of the uniform structure in terms of the extended distance on a subtype

Characterization of the elements of the uniformity in terms of the extended distance

Fixed size neighborhoods of the diagonal belong to the uniform structure

ε-δ characterization of uniform continuity on emetric spaces

ε-δ characterization of uniform embeddings on emetric spaces

ε-δ characterization of Cauchy sequences on emetric spaces

An emetric space is separated

Auxiliary function to replace the uniformity on an emetric space with a uniformity which is equal to the original one, but maybe not defeq. This is useful if one wants to construct an emetric space with a specified uniformity.

The extended metric induced by an injective function taking values in an emetric space.

Emetric space instance on subsets of emetric spaces

The extended distance on a subset of an emetric space is the restriction of the original distance, by definition

The product of two emetric spaces, with the max distance, is an extended metric spaces. We make sure that the uniform structure thus constructed is the one corresponding to the product of uniform spaces, to avoid diamond problems.

The product of a finite number of emetric spaces, with the max distance, is still an emetric space. This construction would also work for infinite products, but it would not give rise to the product topology. Hence, we only formalize it in the good situation of finitely many spaces.

emetric.ball x ε is the set of all points y with edist y x < ε

emetric.closed_ball x ε is the set of all points y with edist y x ≤ ε

ε-characterization of the closure in emetric spaces

In an emetric space, Cauchy sequences are characterized by the fact that, eventually, the edistance between its elements is arbitrarily small

A variation around the emetric characterization of Cauchy sequences

A compact set in an emetric space is separable, i.e., it is the closure of a countable set

A separable emetric space is second countable: one obtains a countable basis by taking the balls centered at points in a dense subset, and with rational radii. We do not register this as an instance, as there is already an instance going in the other direction from second countable spaces to separable spaces, and we want to avoid loops.

The diameter of a set in an emetric space, named emetric.diam

If two points belong to some set, their edistance is bounded by the diameter of the set

If the distance between any two points in a set is bounded by some constant, this constant bounds the diameter.

The diameter of the empty set vanishes

The diameter of a singleton vanishes

The diameter is monotonous with respect to inclusion

The diameter of a union is controlled by the diameter of the sets, and the edistance between two points in the sets.