# Basic properties of metric spaces, and instances. #

source
@[instance 100]
instance MetricSpace.instT0Space {γ : Type w} [MetricSpace γ] :
T0Space γ
source
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.

source
@[reducible, inline]
abbrev MetricSpace.ofT0PseudoMetricSpace (α : Type u_2) [PseudoMetricSpace α] [T0Space α] :
MetricSpace α

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

Equations

- MetricSpace.ofT0PseudoMetricSpace α = { toPseudoMetricSpace := inst✝¹, eq_of_dist_eq_zero := ⋯ }

Instances For

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

A metric space induces an emetric space

Equations

- MetricSpace.toEMetricSpace = EMetricSpace.ofT0PseudoEMetricSpace γ

source
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
source
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
source
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 `β`.

source
@[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.

Equations

- EMetricSpace.toMetricSpaceOfDist dist dist_nonneg h = MetricSpace.ofT0PseudoMetricSpace α

Instances For

source
@[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.

Equations

- EMetricSpace.toMetricSpace h = EMetricSpace.toMetricSpaceOfDist (fun (x1 x2 : α) => (edist x1 x2).toReal) ⋯ ⋯

Instances For

source
@[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`.

Equations

- MetricSpace.induced f hf m = { toPseudoMetricSpace := PseudoMetricSpace.induced f m.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯ }

Instances For

source
@[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.

Equations

- IsUniformEmbedding.comapMetricSpace f h = (MetricSpace.induced f ⋯ m).replaceUniformity ⋯

Instances For

source
@[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.

Equations

- Topology.IsEmbedding.comapMetricSpace f h = (MetricSpace.induced f ⋯ m).replaceTopology ⋯

Instances For

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

- Subtype.metricSpace = MetricSpace.induced Subtype.val ⋯ inst✝

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

- MulOpposite.instMetricSpace = MetricSpace.induced MulOpposite.unop ⋯ inst✝

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

- AddOpposite.instMetricSpace = MetricSpace.induced AddOpposite.unop ⋯ inst✝

source
instance Real.metricSpace :
MetricSpace ℝ

Instantiate the reals as a metric space.

Equations

- Real.metricSpace = MetricSpace.ofT0PseudoMetricSpace ℝ

source
instance instMetricSpaceNNReal :
MetricSpace NNReal
Equations

- instMetricSpaceNNReal = Subtype.metricSpace

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

- instMetricSpaceULift = MetricSpace.induced ULift.down ⋯ inst✝

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

- Prod.metricSpaceMax = MetricSpace.ofT0PseudoMetricSpace (γ × β)

source
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.

Equations

- metricSpacePi = MetricSpace.ofT0PseudoMetricSpace ((b : β) → X b)

source
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.

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

- SeparationQuotient.instDist = { dist := SeparationQuotient.lift₂ dist ⋯ }

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

- SeparationQuotient.instMetricSpace = EMetricSpace.toMetricSpaceOfDist dist ⋯ ⋯

source
@[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.

Equations

- m.replaceEDist d hd = { edist := d, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, toUniformSpace := PseudoEMetricSpace.toUniformSpace, uniformity_edist := ⋯ }

Instances For

source
theorem PseudoEMetricSpace.replaceEDist_eq {X : Type u_2} (m : PseudoEMetricSpace X) (d : X → X → ENNReal) (hd : d = edist) :
m.replaceEDist d hd = m
source
@[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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem PseudoMetricSpace.replaceDist_eq {X : Type u_2} (m : PseudoMetricSpace X) (d : X → X → ℝ) (hd : d = dist) :
m.replaceDist d hd = m
source
@[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.

Equations

- m.replaceEDist d hd = { edist := d, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, uniformity_edist := ⋯, eq_of_edist_eq_zero := ⋯ }

Instances For

source
theorem EMetricSpace.replaceEDist_eq {X : Type u_2} (m : EMetricSpace X) (d : X → X → ENNReal) (hd : d = edist) :
m.replaceEDist d hd = m
source
@[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.

Equations

- m.replaceDist d hd = { dist := d, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯, uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }

Instances For

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