Extended metric spaces

This file is devoted to the definition and study of EMetricSpaces, i.e., metric spaces in which the distance is allowed to take the value ∞. This extended distance is called edist, and takes values in ℝ≥0∞.

Many definitions and theorems expected on emetric spaces are already introduced on uniform spaces and topological spaces. For example: open and closed sets, compactness, completeness, continuity and uniform continuity.

The class EMetricSpace therefore extends UniformSpace (and TopologicalSpace).

Since a lot of elementary properties don't require eq_of_edist_eq_zero we start setting up the theory of PseudoEMetricSpace, where we don't require edist x y = 0 → x = y and we specialize to EMetricSpace at the end.

theorem uniformity_dist_of_mem_uniformity {α : Type u} {β : Type v} [LT β] {U : Filter (α × α)} (z : β) (D : α → α → β) (H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s) : U = ⨅ (ε : β), ⨅ (_ : ε > z), Filter.principal {p : α × α | D p.1 p.2 < ε}

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

class EDist (α : Type u_2) : Type u_2

EDist α means that α is equipped with an extended distance.

• edist : α → α → ENNReal

  Extended distance between two points

theorem EDist.ext_iff {α : Type u_2} {x y : EDist α} : x = y ↔ edist = edist

theorem EDist.ext {α : Type u_2} {x y : EDist α} (edist : edist = edist) : x = y

def Metric.eball {α : Type u} [EDist α] (x : α) (ε : ENNReal) : Set α

Metric.eball x ε is the set of all points y with edist y x < ε

Equations

• Metric.eball x ε = {y : α | edist y x < ε}

@[simp]

theorem Metric.mem_eball {α : Type u} [EDist α] {x y : α} {ε : ENNReal} : y ∈ eball x ε ↔ edist y x < ε

theorem Metric.eball_subset_eball {α : Type u} {x : α} {ε₁ ε₂ : ENNReal} [EDist α] (h : ε₁ ≤ ε₂) : eball x ε₁ ⊆ eball x ε₂

@[reducible]

noncomputable def uniformSpaceOfEDist {α : Type u} (edist : α → α → ENNReal) (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) : UniformSpace α

Creating a uniform space from an extended distance.

Equations

• uniformSpaceOfEDist edist edist_self edist_comm edist_triangle = UniformSpace.ofFun edist edist_self edist_comm edist_triangle uniformSpaceOfEDist._proof_1

@[reducible]

noncomputable def uniformSpaceOfEDistOfHasBasis {α : Type u} [TopologicalSpace α] (edist : α → α → ENNReal) (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) (basis : ∀ (x : α), (nhds x).HasBasis (fun (c : ENNReal) => 0 < c) fun (c : ENNReal) => {y : α | edist x y < c}) : UniformSpace α

Creating a uniform space from an extended distance. We assume that there is a preexisting topology, for which the neighborhoods can be expressed using the distance, and we make sure that the uniform space structure we construct has a topology which is defeq to the original one.

Equations

• uniformSpaceOfEDistOfHasBasis edist edist_self edist_comm edist_triangle basis = UniformSpace.ofFunOfHasBasis edist edist_self edist_comm edist_triangle uniformSpaceOfEDistOfHasBasis._proof_1 basis

class PseudoEMetricSpace (α : Type u) extends EDist α : Type u

A pseudo extended metric space is a type endowed with a ℝ≥0∞-valued distance edist satisfying reflexivity edist x x = 0, commutativity edist x y = edist y x, and the triangle inequality edist x z ≤ edist x y + edist y z.

Note that we do not require edist x y = 0 → x = y. See extended metric spaces (EMetricSpace) for the similar class with that stronger assumption.

Any pseudo extended metric space is a topological space and a uniform space (see TopologicalSpace, UniformSpace), where the topology and uniformity come from the metric. Note that a T1 pseudo extended metric space is just an extended metric space.

We make the uniformity/topology part of the data instead of deriving it from the metric. This e.g. ensures that we do not get a diamond when doing [PseudoEMetricSpace α] [PseudoEMetricSpace β] : TopologicalSpace (α × β): The product metric and product topology agree, but not definitionally so. See Note [forgetful inheritance].

• edist : α → α → ENNReal
• edist_self (x : α) : edist x x = 0
• edist_comm (x y : α) : edist x y = edist y x
• edist_triangle (x y z : α) : edist x z ≤ edist x y + edist y z
• toUniformSpace : UniformSpace α
• uniformity_edist : uniformity α = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | edist p.1 p.2 < ε}

theorem PseudoEMetricSpace.ext {α : Type u_2} {m m' : PseudoEMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m'

Two pseudo emetric space structures with the same edistance function coincide.

theorem PseudoEMetricSpace.ext_iff {α : Type u_2} {m m' : PseudoEMetricSpace α} : m = m' ↔ m.toEDist = m'.toEDist

theorem uniformity_pseudoedist {α : Type u} [PseudoEMetricSpace α] : uniformity α = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | edist p.1 p.2 < ε}

Reformulation of the uniform structure in terms of the extended distance

theorem uniformSpace_edist {α : Type u} [PseudoEMetricSpace α] : PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist ⋯ ⋯ ⋯

theorem uniformity_basis_edist {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 < ε}

theorem Metric.nhds_basis_eball {α : Type u} {x : α} [PseudoEMetricSpace α] : (nhds x).HasBasis (fun (ε : ENNReal) => 0 < ε) (eball x)

theorem mem_uniformity_edist {α : Type u} [PseudoEMetricSpace α] {s : Set (α × α)} : s ∈ uniformity α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s

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

theorem EMetric.nhds_eq {α : Type u} {x : α} [PseudoEMetricSpace α] : nhds x = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal (Metric.eball x ε)

theorem EMetric.mem_nhds_iff {α : Type u} {x : α} {s : Set α} [PseudoEMetricSpace α] : s ∈ nhds x ↔ ∃ ε > 0, Metric.eball x ε ⊆ s

theorem Metric.nhdsWithin_basis_eball {α : Type u} {x : α} {s : Set α} [PseudoEMetricSpace α] : (nhdsWithin x s).HasBasis (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => eball x ε ∩ s

theorem EMetric.mem_nhdsWithin_iff {α : Type u} {x : α} {s t : Set α} [PseudoEMetricSpace α] : s ∈ nhdsWithin x t ↔ ∃ ε > 0, Metric.eball x ε ∩ t ⊆ s

theorem EMetric.isOpen_iff {α : Type u} {s : Set α} [PseudoEMetricSpace α] : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s

@[simp]

theorem Metric.isOpen_eball {α : Type u} {x : α} [PseudoEMetricSpace α] {r : ENNReal} : IsOpen (eball x r)

class WeakPseudoEMetricSpace (α : Type u) [τ : TopologicalSpace α] extends EDist α : Type u

A WeakPseudoEMetricSpace is a topological space endowed with a ℝ≥0∞-value distance edist which is almost an extended pseudometric space: the edist is reflexive, commutative and satisfies the triangle inequality, but the topology on α need not equal the topology induced by the edist. (It must be at least as fine, and agree with it on eballs of finite radius.)

This generalises both pseudo extended metric spaces and ℝ≥0∞ (which have an extended distance, which does not induce the order topology there).

• edist : α → α → ENNReal
• edist_self (x : α) : edist x x = 0
• edist_comm (x y : α) : edist x y = edist y x
• edist_triangle (x y z : α) : edist x z ≤ edist x y + edist y z
• topology_le : (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace ≤ τ

  The topology on α is at most as fine as the topology generated by the edist.

• topology_eq_on_restrict (x : α) (r : ENNReal) : IsOpen (Subtype.val ⁻¹' Metric.eball x r)

  The ambient topology on α matches the edist topology on eballs.

theorem WeakPseudoEMetricSpace.ext {α : Type u_2} [TopologicalSpace α] {m m' : WeakPseudoEMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m'

theorem WeakPseudoEMetricSpace.ext_iff {α : Type u_2} [TopologicalSpace α] {m m' : WeakPseudoEMetricSpace α} : m = m' ↔ m.toEDist = m'.toEDist

@[instance_reducible]

instance PseudoEMetricSpace.toWeakPseudoEMetricSpace (α : Type u) [inst : PseudoEMetricSpace α] : WeakPseudoEMetricSpace α

Every PseudoEMetricSpace has a WeakPseudoEMetricSpace structure by using the topology induced by edist.

Equations

• PseudoEMetricSpace.toWeakPseudoEMetricSpace α = { toEDist := inst.toEDist, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, topology_le := ⋯, topology_eq_on_restrict := ⋯ }

theorem edist_triangle_left {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y z : α) : edist x y ≤ edist z x + edist z y

Triangle inequality for the extended distance

theorem edist_triangle_right {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y z : α) : edist x y ≤ edist x z + edist y z

theorem edist_congr_right {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y z : α} (h : edist x y = 0) : edist x z = edist y z

theorem edist_congr_left {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y z : α} (h : edist x y = 0) : edist z x = edist z y

theorem edist_congr {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {w x y z : α} (hl : edist w x = 0) (hr : edist y z = 0) : edist w y = edist x z

theorem edist_triangle4 {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y z t : α) : edist x t ≤ edist x y + edist y z + edist z t

@[reducible, inline]

noncomputable abbrev PseudoEMetricSpace.ofEDist {α : Type u} (edist : α → α → ENNReal) (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) : PseudoEMetricSpace α

Make a PseudoEMetricSpace from a metric. Warning: the uniformity and topology included herein are the ones generated by the metric. If the type has a pre-existing topology or uniformity, PseudoEMetricSpace.ofEDistOfTopology should be used instead.

Equations

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

theorem EMetric.toUniformSpace_ofEDist {α : Type u} [EDist α] (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) : PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist edist_self edist_comm edist_triangle

theorem EMetric.mk_uniformity_basis {α : Type u} [PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ENNReal), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε) : (uniformity α).HasBasis p fun (x : β) => {p : α × α | edist p.1 p.2 < f x}

Given f : β → ℝ≥0∞, if f sends {i | p i} to a set of positive numbers accumulating to zero, then f i-neighborhoods of the diagonal form a basis of 𝓤 α.

For specific bases see uniformity_basis_edist, uniformity_basis_edist', uniformity_basis_edist_nnreal, and uniformity_basis_edist_inv_nat.

theorem EMetric.mk_uniformity_basis_le {α : Type u} [PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ENNReal), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε) : (uniformity α).HasBasis p fun (x : β) => {p : α × α | edist p.1 p.2 ≤ f x}

Given f : β → ℝ≥0∞, if f sends {i | p i} to a set of positive numbers accumulating to zero, then closed f i-neighborhoods of the diagonal form a basis of 𝓤 α.

For specific bases see uniformity_basis_edist_le and uniformity_basis_edist_le'.

theorem uniformity_basis_edist_le {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 ≤ ε}

theorem uniformity_basis_edist' {α : Type u} [PseudoEMetricSpace α] (ε' : ENNReal) (hε' : 0 < ε') : (uniformity α).HasBasis (fun (ε : ENNReal) => ε ∈ Set.Ioo 0 ε') fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 < ε}

theorem uniformity_basis_edist_le' {α : Type u} [PseudoEMetricSpace α] (ε' : ENNReal) (hε' : 0 < ε') : (uniformity α).HasBasis (fun (ε : ENNReal) => ε ∈ Set.Ioo 0 ε') fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 ≤ ε}

theorem uniformity_basis_edist_nnreal {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun (ε : NNReal) => 0 < ε) fun (ε : NNReal) => {p : α × α | edist p.1 p.2 < ↑ε}

theorem uniformity_basis_edist_nnreal_le {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun (ε : NNReal) => 0 < ε) fun (ε : NNReal) => {p : α × α | edist p.1 p.2 ≤ ↑ε}

theorem uniformity_basis_edist_inv_nat {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {p : α × α | edist p.1 p.2 < (↑n)⁻¹}

theorem uniformity_basis_edist_inv_two_pow {α : Type u} [PseudoEMetricSpace α] : (uniformity α).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {p : α × α | edist p.1 p.2 < 2⁻¹ ^ n}

theorem edist_mem_uniformity {α : Type u} [PseudoEMetricSpace α] {ε : ENNReal} (ε0 : 0 < ε) : {p : α × α | edist p.1 p.2 < ε} ∈ uniformity α

Fixed size neighborhoods of the diagonal belong to the uniform structure

@[instance 900]

instance EMetric.instIsCountablyGeneratedUniformity {α : Type u} [PseudoEMetricSpace α] : (uniformity α).IsCountablyGenerated

theorem EMetric.uniformContinuousOn_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a : α}, a ∈ s → ∀ {b : α}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

ε-δ characterization of uniform continuity on a set for pseudoemetric spaces

theorem EMetric.uniformContinuous_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε

ε-δ characterization of uniform continuity on pseudoemetric spaces

@[reducible, inline]

abbrev PseudoEMetricSpace.replaceUniformity {α : Type u_2} [U : UniformSpace α] (m : PseudoEMetricSpace α) (H : uniformity α = uniformity α) : PseudoEMetricSpace α

Auxiliary function to replace the uniformity on a pseudoemetric space with a uniformity which is equal to the original one, but maybe not defeq. This is useful if one wants to construct a pseudoemetric space with a specified uniformity. See Note [forgetful inheritance] explaining why having definitionally the right uniformity is often important. See note [reducible non-instances].

Equations

• m.replaceUniformity H = { toEDist := m.toEDist, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, toUniformSpace := U, uniformity_edist := ⋯ }

@[reducible, inline]

abbrev PseudoEMetricSpace.induced {α : Type u_2} {β : Type u_3} (f : α → β) (m : PseudoEMetricSpace β) : PseudoEMetricSpace α

The extended pseudometric induced by a function taking values in a pseudoemetric space. See note [reducible non-instances].

Equations

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

@[reducible, inline]

abbrev WeakPseudoEMetricSpace.IsInducing {α : Type u_2} {β : Type u_3} [e : TopologicalSpace α] [n : TopologicalSpace β] {f : α → β} (hf : Topology.IsInducing f) (m : WeakPseudoEMetricSpace β) : WeakPseudoEMetricSpace α

WeakPseudoEMetricSpace can be induced backwards.

Equations

• WeakPseudoEMetricSpace.IsInducing hf m = { edist := fun (x y : α) => edist (f x) (f y), edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, topology_le := ⋯, topology_eq_on_restrict := ⋯ }

@[instance_reducible]

instance instWeakPseudoEMetricSpaceSubtype {α : Type u_2} {p : α → Prop} [TopologicalSpace α] [WeakPseudoEMetricSpace α] : WeakPseudoEMetricSpace (Subtype p)

Weak pseudo-emetric space instance on subsets of weak pseudo-emetric spaces

Equations

• instWeakPseudoEMetricSpaceSubtype = WeakPseudoEMetricSpace.IsInducing ⋯ inst✝

@[instance_reducible]

instance instPseudoEMetricSpaceSubtype {α : Type u_2} {p : α → Prop} [PseudoEMetricSpace α] : PseudoEMetricSpace (Subtype p)

Pseudoemetric space instance on subsets of pseudoemetric spaces

Equations

• instPseudoEMetricSpaceSubtype = PseudoEMetricSpace.induced Subtype.val inst✝

theorem Subtype.edist_eq {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {p : α → Prop} (x y : Subtype p) : edist x y = edist ↑x ↑y

The extended pseudodistance on a subset of a pseudoemetric space is the restriction of the original pseudodistance, by definition.

@[simp]

theorem Subtype.edist_mk_mk {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {p : α → Prop} {x y : α} (hx : p x) (hy : p y) : edist ⟨x, hx⟩ ⟨y, hy⟩ = edist x y

The extended pseudodistance on a subtype of a pseudoemetric space is the restriction of the original pseudodistance, by definition.

@[reducible]

noncomputable def PseudoEMetricSpace.ofEDistOfTopology {α : Type u_2} [TopologicalSpace α] (d : α → α → ENNReal) (h_self : ∀ (x : α), d x x = 0) (h_comm : ∀ (x y : α), d x y = d y x) (h_triangle : ∀ (x y z : α), d x z ≤ d x y + d y z) (h_basis : ∀ (x : α), (nhds x).HasBasis (fun (c : ENNReal) => 0 < c) fun (c : ENNReal) => {y : α | d x y < c}) : PseudoEMetricSpace α

Consider an extended distance on a topological space, for which the neighborhoods can be expressed in terms of the distance. Then we define the emetric space structure associated to this distance, with a topology defeq to the initial one.

Equations

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

@[instance_reducible]

instance instPseudoEMetricSpaceULift {α : Type u_2} [PseudoEMetricSpace α] : PseudoEMetricSpace (ULift.{u_3, u_2} α)

Equations

• instPseudoEMetricSpaceULift = PseudoEMetricSpace.induced ULift.down inst✝

theorem ULift.edist_eq {α : Type u_2} [PseudoEMetricSpace α] (x y : ULift.{u_3, u_2} α) : edist x y = edist x.down y.down

@[simp]

theorem ULift.edist_up_up {α : Type u_2} [PseudoEMetricSpace α] (x y : α) : edist { down := x } { down := y } = edist x y

@[instance_reducible]

instance Prod.pseudoEMetricSpaceMax {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : PseudoEMetricSpace (α × β)

The product of two pseudoemetric spaces, with the max distance, is an extended pseudometric 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

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

theorem Prod.edist_eq {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x y : α × β) : edist x y = max (edist x.1 y.1) (edist x.2 y.2)

theorem Metric.mem_eball' {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : y ∈ eball x ε ↔ edist x y < ε

def Metric.closedEBall {α : Type u_4} [h : EDist α] (x : α) (ε : ENNReal) : Set α

Metric.closedEBall x ε is the set of all points y with edist y x ≤ ε

Equations

• Metric.closedEBall x ε = {y : α | edist y x ≤ ε}

@[simp]

theorem Metric.mem_closedEBall {ε : ENNReal} {α : Type u_4} [EDist α] {x y : α} : y ∈ closedEBall x ε ↔ edist y x ≤ ε

theorem Metric.mem_closedEBall' {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : y ∈ closedEBall x ε ↔ edist x y ≤ ε

@[simp]

theorem Metric.closedEBall_top {α : Type u_4} [EDist α] (x : α) : closedEBall x ⊤ = Set.univ

theorem Metric.eball_subset_closedEBall {ε : ENNReal} {α : Type u_4} [EDist α] {x : α} : eball x ε ⊆ closedEBall x ε

theorem Metric.pos_of_mem_eball {ε : ENNReal} {α : Type u_4} [EDist α] {x y : α} (hy : y ∈ eball x ε) : 0 < ε

theorem Metric.mem_eball_self {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x : α} {ε : ENNReal} (h : 0 < ε) : x ∈ eball x ε

theorem Metric.mem_closedEBall_self {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x : α} {ε : ENNReal} : x ∈ closedEBall x ε

theorem Metric.mem_eball_comm {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : x ∈ eball y ε ↔ y ∈ eball x ε

theorem Metric.mem_closedEBall_comm {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : x ∈ closedEBall y ε ↔ y ∈ closedEBall x ε

theorem Metric.closedEBall_subset_closedEBall {ε₁ ε₂ : ENNReal} {α : Type u_4} [EDist α] {x : α} (h : ε₁ ≤ ε₂) : closedEBall x ε₁ ⊆ closedEBall x ε₂

theorem Metric.eball_disjoint {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal} (h : ε₁ + ε₂ ≤ edist x y) : Disjoint (eball x ε₁) (eball y ε₂)

theorem Metric.eball_subset {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal} (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y ≠ ⊤) : eball x ε₁ ⊆ eball y ε₂

theorem Metric.exists_eball_subset_eball {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} (h : y ∈ eball x ε) : ∃ ε' > 0, eball y ε' ⊆ eball x ε

theorem Metric.eball_eq_empty_iff {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x : α} {ε : ENNReal} : eball x ε = ∅ ↔ ε = 0

theorem Metric.ordConnected_setOfPred_closedEBall_subset {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r : ENNReal | closedEBall x r ⊆ s}.OrdConnected

@[deprecated Metric.ordConnected_setOfPred_closedEBall_subset (since := "2026-07-09")]

theorem Metric.ordConnected_setOf_closedEBall_subset {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r : ENNReal | closedEBall x r ⊆ s}.OrdConnected

Alias of Metric.ordConnected_setOfPred_closedEBall_subset.

theorem Metric.ordConnected_setOfPred_eball_subset {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r : ENNReal | eball x r ⊆ s}.OrdConnected

@[deprecated Metric.ordConnected_setOfPred_eball_subset (since := "2026-07-09")]

theorem Metric.ordConnected_setOf_eball_subset {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r : ENNReal | eball x r ⊆ s}.OrdConnected

Alias of Metric.ordConnected_setOfPred_eball_subset.

@[instance_reducible]

def Metric.edistLtTopSetoid {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] : Setoid α

Relation “two points are at a finite edistance” is an equivalence relation.

Equations

• Metric.edistLtTopSetoid = { r := fun (x y : α) => edist x y < ⊤, iseqv := ⋯ }

@[simp]

theorem Metric.eball_zero {α : Type u_4} [EDist α] {x : α} : eball x 0 = ∅

theorem Metric.nhds_basis_closedEBall {α : Type u_4} [PseudoEMetricSpace α] {x : α} : (nhds x).HasBasis (fun (ε : ENNReal) => 0 < ε) (closedEBall x)

theorem Metric.nhdsWithin_basis_closedEBall {α : Type u_4} [PseudoEMetricSpace α] {s : Set α} {x : α} : (nhdsWithin x s).HasBasis (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => closedEBall x ε ∩ s

theorem EMetric.mem_closure_iff {α : Type u_2} [PseudoEMetricSpace α] {x : α} {s : Set α} : x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε

ε-characterization of the closure in pseudoemetric spaces

theorem EMetric.dense_iff {α : Type u_2} [PseudoEMetricSpace α] {s : Set α} : Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.eball x r ∩ s).Nonempty

theorem EMetric.tendsto_nhds {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, edist (u x) a < ε

theorem EMetric.tendsto_atTop {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} : Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, edist (u n) a < ε

theorem EMetric.tendsto_nhdsWithin_nhdsWithin {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] {s : Set α} [PseudoEMetricSpace β] {f : α → β} {t : Set β} {a : α} {b : β} : Filter.Tendsto f (nhdsWithin a s) (nhdsWithin b t) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

theorem EMetric.tendsto_nhdsWithin_nhds {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] {s : Set α} [PseudoEMetricSpace β] {f : α → β} {a : α} {b : β} : Filter.Tendsto f (nhdsWithin a s) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

theorem EMetric.tendsto_nhds_nhds {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {a : α} {b : β} : Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) b < ε

theorem EMetric.continuousAt_iff {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {a : α} : ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε

theorem EMetric.continuousWithinAt_iff {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {a : α} {s : Set α} : ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε

theorem EMetric.continuousOn_iff {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} : ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, edist a b < δ → edist (f a) (f b) < ε

theorem EMetric.continuous_iff {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : Continuous f ↔ ∀ (b : α), ∀ ε > 0, ∃ δ > 0, ∀ (a : α), edist a b < δ → edist (f a) (f b) < ε

theorem EMetric.continuousAt_iff' {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhds b, edist (f x) (f b) < ε

theorem EMetric.continuousWithinAt_iff' {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} : ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, edist (f x) (f b) < ε

theorem EMetric.continuousOn_iff' {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, edist (f x) (f b) < ε

theorem EMetric.continuous_iff' {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (a : β), ∀ ε > 0, ∀ᶠ (x : β) in nhds a, edist (f x) (f a) < ε

theorem Metric.isClosed_eball_top {α : Type u_2} [PseudoEMetricSpace α] {x : α} : IsClosed (eball x ⊤)

theorem Metric.eball_mem_nhds {α : Type u_2} [PseudoEMetricSpace α] (x : α) {ε : ENNReal} (ε0 : 0 < ε) : eball x ε ∈ nhds x

theorem Metric.closedEBall_mem_nhds {α : Type u_2} [PseudoEMetricSpace α] (x : α) {ε : ENNReal} (ε0 : 0 < ε) : closedEBall x ε ∈ nhds x

theorem Metric.eball_prod_same {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal) : eball x r ×ˢ eball y r = eball (x, y) r

theorem Metric.closedEBall_prod_same {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal) : closedEBall x r ×ˢ closedEBall y r = closedEBall (x, y) r

@[instance_reducible]

instance Subtype.instEDist {α : Type u_3} [EDist α] {p : α → Prop} : EDist (Subtype p)

Equations

• Subtype.instEDist = { edist := fun (x y : Subtype p) => edist ↑x ↑y }

@[simp]

theorem Subtype.preimage_eball {α : Type u_3} [EDist α] {p : α → Prop} (a : { a : α // p a }) (r : ENNReal) : val ⁻¹' Metric.eball (↑a) r = Metric.eball a r

@[simp]

theorem Subtype.preimage_closedEBall {α : Type u_3} [EDist α] {p : α → Prop} (a : { a : α // p a }) (r : ENNReal) : val ⁻¹' Metric.closedEBall (↑a) r = Metric.closedEBall a r

@[simp]

theorem Subtype.image_eball {α : Type u_3} [EDist α] {p : α → Prop} (a : { a : α // p a }) (r : ENNReal) : val '' Metric.eball a r = Metric.eball (↑a) r ∩ {a : α | p a}

@[simp]

theorem Subtype.image_closedEBall {α : Type u_3} [EDist α] {p : α → Prop} (a : { a : α // p a }) (r : ENNReal) : val '' Metric.closedEBall a r = Metric.closedEBall (↑a) r ∩ {a : α | p a}

class EMetricSpace (α : Type u) extends PseudoEMetricSpace α : Type u

An extended metric space is a type endowed with a ℝ≥0∞-valued distance edist satisfying edist x y = 0 ↔ x = y, commutativity edist x y = edist y x, and the triangle inequality edist x z ≤ edist x y + edist y z.

See pseudo extended metric spaces (PseudoEMetricSpace) for the similar class with the edist x y = 0 ↔ x = y assumption weakened to edist x x = 0.

Any extended metric space is a T1 topological space and a uniform space (see TopologicalSpace, T1Space, UniformSpace), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric. This e.g. ensures that we do not get a diamond when doing [EMetricSpace α] [EMetricSpace β] : TopologicalSpace (α × β): The product metric and product topology agree, but not definitionally so. See Note [forgetful inheritance].

• edist : α → α → ENNReal
• edist_self (x : α) : edist x x = 0
• edist_comm (x y : α) : edist x y = edist y x
• edist_triangle (x y z : α) : edist x z ≤ edist x y + edist y z
• toUniformSpace : UniformSpace α
• uniformity_edist : uniformity α = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | edist p.1 p.2 < ε}
• eq_of_edist_eq_zero {x y : α} : edist x y = 0 → x = y

theorem EMetricSpace.ext {α : Type u_3} {m m' : EMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m'

theorem EMetricSpace.ext_iff {α : Type u_3} {m m' : EMetricSpace α} : m = m' ↔ m.toEDist = m'.toEDist

class WeakEMetricSpace (α : Type u) [TopologicalSpace α] extends WeakPseudoEMetricSpace α : Type u

A weak extended metric space extends a WeakPseudoEMetricSpace with the condition edist x y = 0 ↔ x = y.

• edist : α → α → ENNReal
• edist_self (x : α) : edist x x = 0
• edist_comm (x y : α) : edist x y = edist y x
• edist_triangle (x y z : α) : edist x z ≤ edist x y + edist y z
• topology_le : (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace ≤ inst✝
• topology_eq_on_restrict (x : α) (r : ENNReal) : IsOpen (Subtype.val ⁻¹' Metric.eball x r)
• eq_of_edist_eq_zero {x y : α} : edist x y = 0 → x = y

theorem WeakEMetricSpace.ext {α : Type u_3} [TopologicalSpace α] {m m' : WeakEMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m'

theorem WeakEMetricSpace.ext_iff {α : Type u_3} [TopologicalSpace α] {m m' : WeakEMetricSpace α} : m = m' ↔ m.toEDist = m'.toEDist

@[instance_reducible]

instance EMetricSpace.toWeakEMetricSpace (α : Type u) [EMetricSpace α] : WeakEMetricSpace α

Every EMetricSpace has a WeakEMetricSpace structure by using the topology induced by its edist.

Equations

• EMetricSpace.toWeakEMetricSpace α = { toWeakPseudoEMetricSpace := PseudoEMetricSpace.toWeakPseudoEMetricSpace α, eq_of_edist_eq_zero := ⋯ }

@[simp]

theorem edist_eq_zero {γ : Type w} [TopologicalSpace γ] [WeakEMetricSpace γ] {x y : γ} : edist x y = 0 ↔ x = y

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

@[simp]

theorem zero_eq_edist {γ : Type w} [TopologicalSpace γ] [WeakEMetricSpace γ] {x y : γ} : 0 = edist x y ↔ x = y

theorem edist_le_zero {γ : Type w} [TopologicalSpace γ] [WeakEMetricSpace γ] {x y : γ} : edist x y ≤ 0 ↔ x = y

@[simp]

theorem edist_pos {γ : Type w} [TopologicalSpace γ] [WeakEMetricSpace γ] {x y : γ} : 0 < edist x y ↔ x ≠ y

@[simp]

theorem Metric.closedEBall_zero {γ : Type w} [TopologicalSpace γ] [WeakEMetricSpace γ] (x : γ) : closedEBall x 0 = {x}

theorem eq_of_forall_edist_le {γ : Type w} [TopologicalSpace γ] [WeakEMetricSpace γ] {x y : γ} (h : ∀ ε > 0, edist x y ≤ ε) : x = y

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

@[reducible, inline]

abbrev EMetricSpace.replaceUniformity {γ : Type u_3} [U : UniformSpace γ] (m : EMetricSpace γ) (H : uniformity γ = uniformity γ) : EMetricSpace γ

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. See Note [forgetful inheritance] explaining why having definitionally the right uniformity is often important. See note [reducible non-instances].

Equations

• m.replaceUniformity H = { toEDist := m.toEDist, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, toUniformSpace := U, uniformity_edist := ⋯, eq_of_edist_eq_zero := ⋯ }

@[reducible, inline]

abbrev EMetricSpace.replaceTopology {γ : Type u_3} [T : TopologicalSpace γ] (m : EMetricSpace γ) (H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace) : EMetricSpace γ

Auxiliary function to replace the topology on an emetric space with a topology 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 topology. See Note [forgetful inheritance] explaining why having definitionally the right topology is often important. See note [reducible non-instances].

Equations

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

@[reducible, inline]

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

The extended metric induced by an injective function taking values in an emetric space. See Note [reducible non-instances].

Equations

• EMetricSpace.induced f hf m = { toPseudoEMetricSpace := PseudoEMetricSpace.induced f m.toPseudoEMetricSpace, eq_of_edist_eq_zero := ⋯ }

@[instance_reducible]

instance instEMetricSpaceSubtype {α : Type u_3} {p : α → Prop} [EMetricSpace α] : EMetricSpace (Subtype p)

EMetric space instance on subsets of emetric spaces

Equations

• instEMetricSpaceSubtype = EMetricSpace.induced Subtype.val ⋯ inst✝

@[instance_reducible]

instance instEMetricSpaceMulOpposite {α : Type u_3} [EMetricSpace α] : EMetricSpace αᵐᵒᵖ

EMetric space instance on the multiplicative opposite of an emetric space.

Equations

• instEMetricSpaceMulOpposite = EMetricSpace.induced MulOpposite.unop ⋯ inst✝

@[instance_reducible]

instance instEMetricSpaceAddOpposite {α : Type u_3} [EMetricSpace α] : EMetricSpace αᵃᵒᵖ

EMetric space instance on the additive opposite of an emetric space.

Equations

• instEMetricSpaceAddOpposite = EMetricSpace.induced AddOpposite.unop ⋯ inst✝

@[instance_reducible]

instance instEMetricSpaceULift {α : Type u_3} [EMetricSpace α] : EMetricSpace (ULift.{u_4, u_3} α)

Equations

• instEMetricSpaceULift = EMetricSpace.induced ULift.down ⋯ inst✝

theorem uniformity_edist {γ : Type u_3} [EMetricSpace γ] : uniformity γ = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : γ × γ | edist p.1 p.2 < ε}

Reformulation of the uniform structure in terms of the extended distance

Additive, Multiplicative

The distance on those type synonyms is inherited without change.

@[instance_reducible]

instance instEDistAdditive {X : Type u_1} [EDist X] : EDist (Additive X)

Equations

• instEDistAdditive = inst✝

@[instance_reducible]

instance instEDistMultiplicative {X : Type u_1} [EDist X] : EDist (Multiplicative X)

Equations

• instEDistMultiplicative = inst✝

@[simp]

theorem edist_ofMul {X : Type u_1} [EDist X] (a b : X) : edist (Additive.ofMul a) (Additive.ofMul b) = edist a b

@[simp]

theorem edist_ofAdd {X : Type u_1} [EDist X] (a b : X) : edist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = edist a b

@[simp]

theorem edist_toMul {X : Type u_1} [EDist X] (a b : Additive X) : edist (Additive.toMul a) (Additive.toMul b) = edist a b

@[simp]

theorem edist_toAdd {X : Type u_1} [EDist X] (a b : Multiplicative X) : edist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = edist a b

@[instance_reducible]

instance instPseudoEMetricSpaceAdditive {X : Type u_1} [PseudoEMetricSpace X] : PseudoEMetricSpace (Additive X)

Equations

• instPseudoEMetricSpaceAdditive = inst✝

@[instance_reducible]

instance instPseudoEMetricSpaceMultiplicative {X : Type u_1} [PseudoEMetricSpace X] : PseudoEMetricSpace (Multiplicative X)

Equations

• instPseudoEMetricSpaceMultiplicative = inst✝

@[instance_reducible]

instance instEMetricSpaceAdditive {X : Type u_1} [EMetricSpace X] : EMetricSpace (Additive X)

Equations

• instEMetricSpaceAdditive = inst✝

@[instance_reducible]

instance instEMetricSpaceMultiplicative {X : Type u_1} [EMetricSpace X] : EMetricSpace (Multiplicative X)

Equations

• instEMetricSpaceMultiplicative = inst✝

Order dual

The distance on this type synonym is inherited without change.

@[instance_reducible]

instance instEDistOrderDual {X : Type u_1} [EDist X] : EDist Xᵒᵈ

Equations

• instEDistOrderDual = inst✝

@[simp]

theorem edist_toDual {X : Type u_1} [EDist X] (a b : X) : edist (OrderDual.toDual a) (OrderDual.toDual b) = edist a b

@[simp]

theorem edist_ofDual {X : Type u_1} [EDist X] (a b : Xᵒᵈ) : edist (OrderDual.ofDual a) (OrderDual.ofDual b) = edist a b

@[reducible, inline]

abbrev WeakEMetricSpace.induced {α : Type u_3} {β : Type u_4} [n : TopologicalSpace β] {f : α → β} (hf : Function.Injective f) (m : WeakEMetricSpace β) : WeakEMetricSpace α

The WeakEMetric space induced by pulling back a topology along an injective function.

Equations

• WeakEMetricSpace.induced hf m = { toWeakPseudoEMetricSpace := WeakPseudoEMetricSpace.IsInducing ⋯ m.toWeakPseudoEMetricSpace, eq_of_edist_eq_zero := ⋯ }

@[instance_reducible]

instance instWeakEMetricSpaceSubtype {α : Type u_3} {p : α → Prop} [TopologicalSpace α] [WeakEMetricSpace α] : WeakEMetricSpace (Subtype p)

WeakEMetricSpace instance on subsets of emetric spaces

Equations

• instWeakEMetricSpaceSubtype = WeakEMetricSpace.induced ⋯ inst✝

@[instance_reducible]

instance instWeakPseudoEMetricSpaceOrderDual {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] : WeakPseudoEMetricSpace Xᵒᵈ

Equations

• instWeakPseudoEMetricSpaceOrderDual = inst✝

@[instance_reducible]

instance instWeakEMetricSpaceOrderDual {X : Type u_1} [TopologicalSpace X] [WeakEMetricSpace X] : WeakEMetricSpace Xᵒᵈ

Equations

• instWeakEMetricSpaceOrderDual = inst✝

@[instance_reducible]

instance instPseudoEMetricSpaceOrderDual {X : Type u_1} [PseudoEMetricSpace X] : PseudoEMetricSpace Xᵒᵈ

Equations

• instPseudoEMetricSpaceOrderDual = inst✝

@[instance_reducible]

instance instEMetricSpaceOrderDual {X : Type u_1} [EMetricSpace X] : EMetricSpace Xᵒᵈ

Equations

• instEMetricSpaceOrderDual = inst✝