Basic properties of metric spaces, and instances.

@[instance 100]

instance MetricSpace.instT0Space {γ : Type w} [MetricSpace γ] : T0Space γ

theorem Metric.isUniformEmbedding_iff' {β : Type v} {γ : Type w} [MetricSpace γ] [PseudoMetricSpace β] {f : γ → β} : IsUniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ

A map between metric spaces is a uniform embedding if and only if the distance between f x and f y is controlled in terms of the distance between x and y and conversely.

@[reducible, inline]

abbrev MetricSpace.ofT0PseudoMetricSpace (α : Type u_2) [PseudoMetricSpace α] [T0Space α] : MetricSpace α

If a PseudoMetricSpace is a T₀ space, then it is a MetricSpace.

@[instance 100]

instance MetricSpace.toEMetricSpace {γ : Type w} [MetricSpace γ] : EMetricSpace γ

A metric space induces an emetric space

theorem Metric.isClosed_of_pairwise_le_dist {γ : Type w} [MetricSpace γ] {s : Set γ} {ε : ℝ} (hε : 0 < ε) (hs : s.Pairwise fun (x y : γ) => ε ≤ dist x y) : IsClosed s

theorem Metric.isClosedEmbedding_of_pairwise_le_dist {γ : Type w} [MetricSpace γ] {α : Type u_2} [TopologicalSpace α] [DiscreteTopology α] {ε : ℝ} (hε : 0 < ε) {f : α → γ} (hf : Pairwise fun (x y : α) => ε ≤ dist (f x) (f y)) : Topology.IsClosedEmbedding f

theorem Metric.isUniformEmbedding_bot_of_pairwise_le_dist {α : Type u} [PseudoMetricSpace α] {β : Type u_2} {ε : ℝ} (hε : 0 < ε) {f : β → α} (hf : Pairwise fun (x y : β) => ε ≤ dist (f x) (f y)) : IsUniformEmbedding f

If f : β → α sends any two distinct points to points at distance at least ε > 0, then f is a uniform embedding with respect to the discrete uniformity on β.

@[reducible, inline]

abbrev EMetricSpace.toMetricSpaceOfDist {α : Type u} [EMetricSpace α] (dist : α → α → ℝ) (dist_nonneg : ∀ (x y : α), 0 ≤ dist x y) (h : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)) : MetricSpace α

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.

@[reducible, inline]

abbrev EMetricSpace.toMetricSpace {α : Type u} [EMetricSpace α] (h : ∀ (x y : α), edist x y ≠ ⊤) : MetricSpace α

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.

@[reducible, inline]

abbrev MetricSpace.induced {γ : Type u_2} {β : Type u_3} (f : γ → β) (hf : Function.Injective f) (m : MetricSpace β) : MetricSpace γ

Metric space structure pulled back by an injective function. Injectivity is necessary to ensure that dist x y = 0 only if x = y.

@[reducible, inline]

abbrev IsUniformEmbedding.comapMetricSpace {α : Type u_2} {β : Type u_3} [UniformSpace α] [m : MetricSpace β] (f : α → β) (h : IsUniformEmbedding f) : MetricSpace α

Pull back a metric space structure by a uniform embedding. This is a version of MetricSpace.induced useful in case if the domain already has a UniformSpace structure.

@[reducible, inline]

abbrev Topology.IsEmbedding.comapMetricSpace {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [m : MetricSpace β] (f : α → β) (h : IsEmbedding f) : MetricSpace α

Pull back a metric space structure by an embedding. This is a version of MetricSpace.induced useful in case if the domain already has a TopologicalSpace structure.

instance Subtype.metricSpace {α : Type u_2} {p : α → Prop} [MetricSpace α] : MetricSpace (Subtype p)

instance MulOpposite.instMetricSpace {α : Type u_2} [MetricSpace α] : MetricSpace αᵐᵒᵖ

instance AddOpposite.instMetricSpace {α : Type u_2} [MetricSpace α] : MetricSpace αᵃᵒᵖ

instance Real.metricSpace : MetricSpace ℝ

Instantiate the reals as a metric space.

instance instMetricSpaceNNReal : MetricSpace NNReal

theorem NNReal.isUniformEmbedding_coe : IsUniformEmbedding toReal

theorem NNReal.isEmbedding_coe : Topology.IsEmbedding toReal

instance instMetricSpaceULift {β : Type v} [MetricSpace β] : MetricSpace (ULift.{u_2, v} β)

instance Prod.metricSpaceMax {β : Type v} {γ : Type w} [MetricSpace γ] [MetricSpace β] : MetricSpace (γ × β)

instance metricSpacePi {β : Type v} {X : β → Type u_2} [Fintype β] [(b : β) → MetricSpace (X b)] : MetricSpace ((b : β) → X b)

A finite product of metric spaces is a metric space, with the sup distance.

theorem Metric.secondCountable_of_countable_discretization {α : Type u} [PseudoMetricSpace α] (H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε) : SecondCountableTopology α

A metric space is second countable if one can reconstruct up to any ε>0 any element of the space from countably many data.

instance SeparationQuotient.instDist {α : Type u} [PseudoMetricSpace α] : Dist (SeparationQuotient α)

theorem SeparationQuotient.dist_mk {α : Type u} [PseudoMetricSpace α] (p q : α) : dist (mk p) (mk q) = dist p q

instance SeparationQuotient.instMetricSpace {α : Type u} [PseudoMetricSpace α] : MetricSpace (SeparationQuotient α)

@[reducible, inline]

abbrev PseudoEMetricSpace.replaceEDist {X : Type u_2} (m : PseudoEMetricSpace X) (d : X → X → ENNReal) (hd : d = edist) : PseudoEMetricSpace X

Build new pseudoemetric space from an old one where the edistance is provably (but typically non-definitionally) equal to some given edistance. We also provide convenience versions for PseudoMetric, Emetric and Metric spaces.

theorem PseudoEMetricSpace.replaceEDist_eq {X : Type u_2} (m : PseudoEMetricSpace X) (d : X → X → ENNReal) (hd : d = edist) : m.replaceEDist d hd = m

@[reducible, inline]

abbrev PseudoMetricSpace.replaceDist {X : Type u_2} (m : PseudoMetricSpace X) (d : X → X → ℝ) (hd : d = dist) : PseudoMetricSpace X

Build new pseudometric space from an old one where the distance is provably (but typically non-definitionally) equal to some given distance. We also provide convenience versions for PseudoEMetric, Emetric and Metric spaces.

theorem PseudoMetricSpace.replaceDist_eq {X : Type u_2} (m : PseudoMetricSpace X) (d : X → X → ℝ) (hd : d = dist) : m.replaceDist d hd = m

@[reducible, inline]

abbrev EMetricSpace.replaceEDist {X : Type u_2} (m : EMetricSpace X) (d : X → X → ENNReal) (hd : d = edist) : EMetricSpace X

Build new emetric space from an old one where the edistance is provably (but typically non-definitionally) equal to some given edistance. We also provide convenience versions for PseudoEMetric, PseudoMetric and Metric spaces.

theorem EMetricSpace.replaceEDist_eq {X : Type u_2} (m : EMetricSpace X) (d : X → X → ENNReal) (hd : d = edist) : m.replaceEDist d hd = m

@[reducible, inline]

abbrev MetricSpace.replaceDist {X : Type u_2} (m : MetricSpace X) (d : X → X → ℝ) (hd : d = dist) : MetricSpace X

Build new metric space from an old one where the distance is provably (but typically non-definitionally) equal to some given distance. We also provide convenience versions for PseudoEMetric, PseudoMatric and EMetric spaces.

theorem MetricSpace.replaceDist_eq {X : Type u_2} (m : MetricSpace X) (d : X → X → ℝ) (hd : d = dist) : m.replaceDist d hd = m