Construct a uniform structure from a distance function and metric space axioms
The distance function (given an ambient metric space on α), which returns a nonnegative real number dist x y given x y : α.
Metric space
Each metric 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 a metric_space structure, the uniformity fields are not necessary, they will be filled in by default. In the same way, each metric space induces an emetric space structure. It is included in the structure, but filled in by default.
When one instantiates a metric space structure, for instance a product structure, this makes it possible to use a uniform structure and an edistance that are exactly the ones for the uniform spaces product and the emetric spaces products, thereby ensuring that everything in defeq in diamonds.
The triangle (polygon) inequality for sequences of points; finset.Ico version.
The triangle (polygon) inequality for sequences of points; finset.range version.
A version of dist_le_Ico_sum_dist with each intermediate distance replaced with an upper estimate.
A version of dist_le_range_sum_dist with each intermediate distance replaced with an upper estimate.
Distance as a nonnegative real number.
Express nndist in terms of edist
Express edist in terms of nndist
In a metric space, the extended distance is always finite
nndist x x vanishes
Express dist in terms of nndist
Express nndist in terms of dist
Deduce the equality of points with the vanishing of the nonnegative distance
Characterize the equality of points with the vanishing of the nonnegative distance
Triangle inequality for the nonnegative distance
Express dist in terms of edist
ball x ε is the set of all points y with dist y x < ε
closed_ball x ε is the set of all points y with dist y x ≤ ε
A metric space space is totally bounded if one can reconstruct up to any ε>0 any element of the space from finitely many data.
Expressing the uniformity in terms of edist
A metric space induces an emetric space
Balls defined using the distance or the edistance coincide
Closed balls defined using the distance or the edistance coincide
One gets a metric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the metric space and the emetric space. In this definition, the distance is given separately, to be able to prescribe some expression which is not defeq to the push-forward of the edistance to reals.
One gets a metric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the metric space and the emetric space.
Instantiate the reals as a metric space.
In a metric space, Cauchy sequences are characterized by the fact that, eventually, the distance between its elements is arbitrarily small
A variation around the metric characterization of Cauchy sequences
A Cauchy sequence on the natural numbers is bounded.
Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.
ε-characterization of the closure in metric spaces
A finite product of metric spaces is a metric space, with the sup distance.
Any compact set in a metric space can be covered by finitely many balls of a given positive radius
A metric space is proper if all closed balls are compact.
A proper space is locally compact
A proper space is complete
A proper metric space is separable, and therefore second countable. Indeed, any ball is compact, and therefore admits a countable dense subset. Taking a countable union over the balls centered at a fixed point and with integer radius, one obtains a countable set which is dense in the whole space.
A metric space is second countable if, for every ε > 0, there is a countable set which is ε-dense.
A metric space space is second countable if one can reconstruct up to any ε>0 any element of the space from countably many data.
Boundedness of a subset of a metric space. We formulate the definition to work even in the empty space.
Subsets of a bounded set are also bounded
Closed balls are bounded
Open balls are bounded
Given a point, a bounded subset is included in some ball around this point
The union of two bounded sets is bounded iff each of the sets is bounded
A finite union of bounded sets is bounded
A compact set is bounded
A finite set is bounded
A singleton is bounded
Characterization of the boundedness of the range of a function
In a compact space, all sets are bounded
In a proper space, a set is compact if and only if it is closed and bounded
The diameter of a set in a metric space. To get controllable behavior even when the diameter should be infinite, we express it in terms of the emetric.diameter
The diameter of a set is always nonnegative
The empty set has zero diameter
A singleton has zero diameter
Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.
An unbounded set has zero diameter. If you would prefer to get the value ∞, use emetric.diam. This lemma makes it possible to avoid side conditions in some situations
If s ⊆ t, then the diameter of s is bounded by that of t, provided t is bounded.
The distance between two points in a set is controlled 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 a union is controlled by the sum of the diameters, and the distance between any two points in each of the sets. This lemma is true without any side condition, since it is obviously true if s ∪ t is unbounded.
If two sets intersect, the diameter of the union is bounded by the sum of the diameters.
The diameter of a closed ball of radius r is at most 2 r.
The diameter of a ball of radius r is at most 2 r.