Extended metric spaces #
Further results about extended metric spaces.
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 edist_le_Ico_sum_edist with each intermediate distance replaced
with an upper estimate.
A version of edist_le_range_sum_edist with each intermediate distance replaced
with an upper estimate.
Alias of EMetric.isUniformInducing_iff.
ε-δ characterization of uniform embeddings on pseudoemetric spaces
Alias of EMetric.isUniformEmbedding_iff.
ε-δ characterization of uniform embeddings on pseudoemetric spaces
If a map between pseudoemetric spaces is a uniform embedding then the edistance between f x
and f y is controlled in terms of the distance between x and y.
In fact, this lemma holds for a IsUniformInducing map.
TODO: generalize?
Alias of EMetric.controlled_of_isUniformEmbedding.
If a map between pseudoemetric spaces is a uniform embedding then the edistance between f x
and f y is controlled in terms of the distance between x and y.
In fact, this lemma holds for a IsUniformInducing map.
TODO: generalize?
ε-δ characterization of Cauchy sequences on pseudoemetric spaces
A very useful criterion to show that a space is complete is to show that all sequences
which satisfy a bound of the form edist (u n) (u m) < B N for all n m ≥ N are
converging. This is often applied for B N = 2^{-N}, i.e., with a very fast convergence to
0, which makes it possible to use arguments of converging series, while this is impossible
to do in general for arbitrary Cauchy sequences.
A sequentially complete pseudoemetric space is complete.
Expressing locally uniform convergence on a set using edist.
Expressing uniform convergence on a set using edist.
Expressing locally uniform convergence using edist.
Expressing uniform convergence using edist.
Alias of the forward direction of EMetric.inseparable_iff.
In a pseudoemetric space, Cauchy sequences are characterized by the fact that, eventually, the pseudoedistance between its elements is arbitrarily small
A variation around the emetric characterization of Cauchy sequences
A variation of the emetric characterization of Cauchy sequences that deals with
ℝ≥0 upper bounds.
A compact set in a pseudo emetric space is separable, i.e., it is a subset of the closure of a countable set.
A sigma compact pseudo emetric space has second countable topology.
An emetric space is separated
A map between emetric spaces is a uniform embedding if and only if the edistance between f x
and f y is controlled in terms of the distance between x and y and conversely.
Alias of EMetric.isUniformEmbedding_iff'.
A map between emetric spaces is a uniform embedding if and only if the edistance between f x
and f y is controlled in terms of the distance between x and y and conversely.
If a PseudoEMetricSpace is a T₀ space, then it is an EMetricSpace.
Equations
- Eq (EMetricSpace.ofT0PseudoEMetricSpace α) { toPseudoEMetricSpace := inst✝¹, eq_of_edist_eq_zero := ⋯ }
Instances For
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.
Equations
Instances For
A compact set in an emetric space is separable, i.e., it is the closure of a countable set.
Separation quotient #
Equations
- Eq instEDistSeparationQuotient { edist := SeparationQuotient.lift₂ EDist.edist ⋯ }
Instances For
Equations
Instances For
If a set s is separable in a (pseudo extended) metric space, then it admits a countable dense
subset. This is not obvious, as the countable set whose closure covers s given by the definition
of separability does not need in general to be contained in s.
If a set s is separable, then the corresponding subtype is separable in a (pseudo extended)
metric space. This is not obvious, as the countable set whose closure covers s does not need in
general to be contained in s.