# Extended metric spaces #

This file is devoted to the definition and study of `EMetricSpace`s, 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.

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

source
class EDist (α : Type u_2) :
Type u_2

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

- edist : α → α → ENNReal

  Extended distance between two points

Instances

source
theorem EDist.ext_iff {α : Type u_2} {x y : EDist α} :
x = y ↔ edist = edist
source
theorem EDist.ext {α : Type u_2} {x y : EDist α} (edist : edist = edist) :
x = y
source
@[reducible]
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

Instances For

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

Instances For

source
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 < ε}

Instances

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

source
theorem PseudoEMetricSpace.ext_iff {α : Type u_2} {m m' : PseudoEMetricSpace α} :
m = m' ↔ m.toEDist = m'.toEDist
source
theorem edist_triangle_left {α : Type u} [PseudoEMetricSpace α] (x y z : α) :
edist x y ≤ edist z x + edist z y

Triangle inequality for the extended distance

source
theorem edist_triangle_right {α : Type u} [PseudoEMetricSpace α] (x y z : α) :
edist x y ≤ edist x z + edist y z
source
theorem edist_congr_right {α : Type u} [PseudoEMetricSpace α] {x y z : α} (h : edist x y = 0) :
edist x z = edist y z
source
theorem edist_congr_left {α : Type u} [PseudoEMetricSpace α] {x y z : α} (h : edist x y = 0) :
edist z x = edist z y
source
theorem edist_congr {α : Type u} [PseudoEMetricSpace α] {w x y z : α} (hl : edist w x = 0) (hr : edist y z = 0) :
edist w y = edist x z
source
theorem edist_triangle4 {α : Type u} [PseudoEMetricSpace α] (x y z t : α) :
edist x t ≤ edist x y + edist y z + edist z t
source
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

source
theorem uniformSpace_edist {α : Type u} [PseudoEMetricSpace α] :
PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist ⋯ ⋯ ⋯
source
theorem uniformity_basis_edist {α : Type u} [PseudoEMetricSpace α] :
(uniformity α).HasBasis (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 < ε}
source
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

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

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

source
theorem uniformity_basis_edist_le {α : Type u} [PseudoEMetricSpace α] :
(uniformity α).HasBasis (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 ≤ ε}
source
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 < ε}
source
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 ≤ ε}
source
theorem uniformity_basis_edist_nnreal {α : Type u} [PseudoEMetricSpace α] :
(uniformity α).HasBasis (fun (ε : NNReal) => 0 < ε) fun (ε : NNReal) => {p : α × α | edist p.1 p.2 < ↑ε}
source
theorem uniformity_basis_edist_nnreal_le {α : Type u} [PseudoEMetricSpace α] :
(uniformity α).HasBasis (fun (ε : NNReal) => 0 < ε) fun (ε : NNReal) => {p : α × α | edist p.1 p.2 ≤ ↑ε}
source
theorem uniformity_basis_edist_inv_nat {α : Type u} [PseudoEMetricSpace α] :
(uniformity α).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {p : α × α | edist p.1 p.2 < (↑n)⁻¹}
source
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}
source
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

source
@[instance 900]
instance EMetric.instIsCountablyGeneratedUniformity {α : Type u} [PseudoEMetricSpace α] :
(uniformity α).IsCountablyGenerated
source
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

source
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

source
@[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 := ⋯ }

Instances For

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

Instances For

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

source
theorem Subtype.edist_eq {α : Type u} [PseudoEMetricSpace α] {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.

source
@[simp]
theorem Subtype.edist_mk_mk {α : Type u} [PseudoEMetricSpace α] {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.

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

Instances For

source
instance MulOpposite.instPseudoEMetricSpace {α : Type u_2} [PseudoEMetricSpace α] :
PseudoEMetricSpace α ᵐᵒᵖ

Pseudoemetric space instance on the multiplicative opposite of a pseudoemetric space.

Equations

- MulOpposite.instPseudoEMetricSpace = PseudoEMetricSpace.induced MulOpposite.unop inst✝

source
instance AddOpposite.instPseudoEMetricSpace {α : Type u_2} [PseudoEMetricSpace α] :
PseudoEMetricSpace α ᵃᵒᵖ

Pseudoemetric space instance on the additive opposite of a pseudoemetric space.

Equations

- AddOpposite.instPseudoEMetricSpace = PseudoEMetricSpace.induced AddOpposite.unop inst✝

source
theorem MulOpposite.edist_unop {α : Type u} [PseudoEMetricSpace α] (x y : α ᵐᵒᵖ) :
edist (unop x) (unop y) = edist x y
source
theorem AddOpposite.edist_unop {α : Type u} [PseudoEMetricSpace α] (x y : α ᵃᵒᵖ) :
edist (unop x) (unop y) = edist x y
source
theorem MulOpposite.edist_op {α : Type u} [PseudoEMetricSpace α] (x y : α) :
edist (op x) (op y) = edist x y
source
theorem AddOpposite.edist_op {α : Type u} [PseudoEMetricSpace α] (x y : α) :
edist (op x) (op y) = edist x y
source
instance instPseudoEMetricSpaceULift {α : Type u} [PseudoEMetricSpace α] :
PseudoEMetricSpace (ULift.{u_2, u} α)
Equations

- instPseudoEMetricSpaceULift = PseudoEMetricSpace.induced ULift.down inst✝

source
theorem ULift.edist_eq {α : Type u} [PseudoEMetricSpace α] (x y : ULift.{u_2, u} α) :
edist x y = edist x.down y.down
source
@[simp]
theorem ULift.edist_up_up {α : Type u} [PseudoEMetricSpace α] (x y : α) :
edist { down := x } { down := y } = edist x y
source
instance Prod.pseudoEMetricSpaceMax {α : Type u} {β : Type v} [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.

source
theorem Prod.edist_eq {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x y : α × β) :
edist x y = max (edist x.1 y.1) (edist x.2 y.2)
source
def EMetric.ball {α : Type u} [PseudoEMetricSpace α] (x : α) (ε : ENNReal) :
Set α

`EMetric.ball x ε` is the set of all points `y` with `edist y x < ε`

Equations

- EMetric.ball x ε = {y : α | edist y x < ε}

Instances For

source
@[simp]
theorem EMetric.mem_ball {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε : ENNReal} :
y ∈ ball x ε ↔ edist y x < ε
source
theorem EMetric.mem_ball' {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε : ENNReal} :
y ∈ ball x ε ↔ edist x y < ε
source
def EMetric.closedBall {α : Type u} [PseudoEMetricSpace α] (x : α) (ε : ENNReal) :
Set α

`EMetric.closedBall x ε` is the set of all points `y` with `edist y x ≤ ε`

Equations

- EMetric.closedBall x ε = {y : α | edist y x ≤ ε}

Instances For

source
@[simp]
theorem EMetric.mem_closedBall {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε : ENNReal} :
y ∈ closedBall x ε ↔ edist y x ≤ ε
source
theorem EMetric.mem_closedBall' {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε : ENNReal} :
y ∈ closedBall x ε ↔ edist x y ≤ ε
source
@[simp]
theorem EMetric.closedBall_top {α : Type u} [PseudoEMetricSpace α] (x : α) :
closedBall x ⊤ = Set.univ
source
theorem EMetric.ball_subset_closedBall {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} :
ball x ε ⊆ closedBall x ε
source
theorem EMetric.pos_of_mem_ball {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε : ENNReal} (hy : y ∈ ball x ε) :
0 < ε
source
theorem EMetric.mem_ball_self {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} (h : 0 < ε) :
x ∈ ball x ε
source
theorem EMetric.mem_closedBall_self {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} :
x ∈ closedBall x ε
source
theorem EMetric.mem_ball_comm {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε : ENNReal} :
x ∈ ball y ε ↔ y ∈ ball x ε
source
theorem EMetric.mem_closedBall_comm {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε : ENNReal} :
x ∈ closedBall y ε ↔ y ∈ closedBall x ε
source
theorem EMetric.ball_subset_ball {α : Type u} [PseudoEMetricSpace α] {x : α} {ε₁ ε₂ : ENNReal} (h : ε₁ ≤ ε₂) :
ball x ε₁ ⊆ ball x ε₂
source
theorem EMetric.closedBall_subset_closedBall {α : Type u} [PseudoEMetricSpace α] {x : α} {ε₁ ε₂ : ENNReal} (h : ε₁ ≤ ε₂) :
closedBall x ε₁ ⊆ closedBall x ε₂
source
theorem EMetric.ball_disjoint {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal} (h : ε₁ + ε₂ ≤ edist x y) :
Disjoint (ball x ε₁) (ball y ε₂)
source
theorem EMetric.ball_subset {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal} (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y ≠ ⊤) :
ball x ε₁ ⊆ ball y ε₂
source
theorem EMetric.exists_ball_subset_ball {α : Type u} [PseudoEMetricSpace α] {x y : α} {ε : ENNReal} (h : y ∈ ball x ε) :
∃ ε' > 0, ball y ε' ⊆ ball x ε
source
theorem EMetric.ball_eq_empty_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} :
ball x ε = ∅ ↔ ε = 0
source
theorem EMetric.ordConnected_setOf_closedBall_subset {α : Type u} [PseudoEMetricSpace α] (x : α) (s : Set α) :
{r : ENNReal | closedBall x r ⊆ s}.OrdConnected
source
theorem EMetric.ordConnected_setOf_ball_subset {α : Type u} [PseudoEMetricSpace α] (x : α) (s : Set α) :
{r : ENNReal | ball x r ⊆ s}.OrdConnected
source
def EMetric.edistLtTopSetoid {α : Type u} [PseudoEMetricSpace α] :
Setoid α

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

Equations

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

Instances For

source
@[simp]
theorem EMetric.ball_zero {α : Type u} [PseudoEMetricSpace α] {x : α} :
ball x 0 = ∅
source
theorem EMetric.nhds_basis_eball {α : Type u} [PseudoEMetricSpace α] {x : α} :
(nhds x).HasBasis (fun (ε : ENNReal) => 0 < ε) (ball x)
source
theorem EMetric.nhdsWithin_basis_eball {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} :
(nhdsWithin x s).HasBasis (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => ball x ε ∩ s
source
theorem EMetric.nhds_basis_closed_eball {α : Type u} [PseudoEMetricSpace α] {x : α} :
(nhds x).HasBasis (fun (ε : ENNReal) => 0 < ε) (closedBall x)
source
theorem EMetric.nhdsWithin_basis_closed_eball {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} :
(nhdsWithin x s).HasBasis (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => closedBall x ε ∩ s
source
theorem EMetric.nhds_eq {α : Type u} [PseudoEMetricSpace α] {x : α} :
nhds x = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal (ball x ε)
source
theorem EMetric.mem_nhds_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} :
s ∈ nhds x ↔ ∃ ε > 0, ball x ε ⊆ s
source
theorem EMetric.mem_nhdsWithin_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {s t : Set α} :
s ∈ nhdsWithin x t ↔ ∃ ε > 0, ball x ε ∩ t ⊆ s
source
theorem EMetric.tendsto_nhdsWithin_nhdsWithin {α : Type u} {β : Type v} [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 < ε
source
theorem EMetric.tendsto_nhdsWithin_nhds {α : Type u} {β : Type v} [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 < ε
source
theorem EMetric.tendsto_nhds_nhds {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {a : α} {b : β} :
Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) b < ε
source
theorem EMetric.isOpen_iff {α : Type u} [PseudoEMetricSpace α] {s : Set α} :
IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s
source
@[simp]
theorem EMetric.isOpen_ball {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} :
IsOpen (ball x ε)
source
theorem EMetric.isClosed_ball_top {α : Type u} [PseudoEMetricSpace α] {x : α} :
IsClosed (ball x ⊤)
source
theorem EMetric.ball_mem_nhds {α : Type u} [PseudoEMetricSpace α] (x : α) {ε : ENNReal} (ε0 : 0 < ε) :
ball x ε ∈ nhds x
source
theorem EMetric.closedBall_mem_nhds {α : Type u} [PseudoEMetricSpace α] (x : α) {ε : ENNReal} (ε0 : 0 < ε) :
closedBall x ε ∈ nhds x
source
theorem EMetric.ball_prod_same {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal) :
ball x r ×ˢ ball y r = ball (x, y) r
source
theorem EMetric.closedBall_prod_same {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal) :
closedBall x r ×ˢ closedBall y r = closedBall (x, y) r
source
theorem EMetric.mem_closure_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} :
x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε

ε-characterization of the closure in pseudoemetric spaces

source
theorem EMetric.tendsto_nhds {α : Type u} {β : Type v} [PseudoEMetricSpace α] {f : Filter β} {u : β → α} {a : α} :
Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, edist (u x) a < ε
source
theorem EMetric.tendsto_atTop {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} :
Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, edist (u n) a < ε
source
theorem EMetric.subset_countable_closure_of_almost_dense_set {α : Type u} [PseudoEMetricSpace α] (s : Set α) (hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε) :
∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

For a set `s` in a pseudo emetric space, if for every `ε > 0` there exists a countable set that is `ε`-dense in `s`, then there exists a countable subset `t ⊆ s` that is dense in `s`.

source
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

Instances

source
theorem EMetricSpace.ext {α : Type u_2} {m m' : EMetricSpace α} (h : m.toEDist = m'.toEDist) :
m = m'
source
theorem EMetricSpace.ext_iff {α : Type u_2} {m m' : EMetricSpace α} :
m = m' ↔ m.toEDist = m'.toEDist
source
@[simp]
theorem edist_eq_zero {γ : Type w} [EMetricSpace γ] {x y : γ} :
edist x y = 0 ↔ x = y

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

source
@[simp]
theorem zero_eq_edist {γ : Type w} [EMetricSpace γ] {x y : γ} :
0 = edist x y ↔ x = y
source
theorem edist_le_zero {γ : Type w} [EMetricSpace γ] {x y : γ} :
edist x y ≤ 0 ↔ x = y
source
@[simp]
theorem edist_pos {γ : Type w} [EMetricSpace γ] {x y : γ} :
0 < edist x y ↔ x ≠ y
source
@[simp]
theorem EMetric.closedBall_zero {γ : Type w} [EMetricSpace γ] (x : γ) :
closedBall x 0 = {x}
source
theorem eq_of_forall_edist_le {γ : Type w} [EMetricSpace γ] {x y : γ} (h : ∀ ε > 0, edist x y ≤ ε) :
x = y

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

source
@[reducible, inline]
abbrev EMetricSpace.replaceUniformity {γ : Type u_2} [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 := ⋯ }

Instances For

source
@[reducible, inline]
abbrev EMetricSpace.replaceTopology {γ : Type u_2} [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.

Instances For

source
@[reducible, inline]
abbrev EMetricSpace.induced {γ : Type u_2} {β : Type u_3} (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 := ⋯ }

Instances For

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

EMetric space instance on subsets of emetric spaces

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

source
theorem uniformity_edist {γ : Type w} [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.

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

- instEDistAdditive = inst✝

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

- instEDistMultiplicative = inst✝

source
@[simp]
theorem edist_ofMul {X : Type u_1} [EDist X] (a b : X) :
edist (Additive.ofMul a) (Additive.ofMul b) = edist a b
source
@[simp]
theorem edist_ofAdd {X : Type u_1} [EDist X] (a b : X) :
edist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = edist a b
source
@[simp]
theorem edist_toMul {X : Type u_1} [EDist X] (a b : Additive X) :
edist (Additive.toMul a) (Additive.toMul b) = edist a b
source
@[simp]
theorem edist_toAdd {X : Type u_1} [EDist X] (a b : Multiplicative X) :
edist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = edist a b
source
instance instPseudoEMetricSpaceAdditive {X : Type u_1} [PseudoEMetricSpace X] :
PseudoEMetricSpace (Additive X)
Equations

- instPseudoEMetricSpaceAdditive = inst✝

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

- instPseudoEMetricSpaceMultiplicative = inst✝

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

- instEMetricSpaceAdditive = inst✝

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

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

- instEDistOrderDual = inst✝

source
@[simp]
theorem edist_toDual {X : Type u_1} [EDist X] (a b : X) :
edist (OrderDual.toDual a) (OrderDual.toDual b) = edist a b
source
@[simp]
theorem edist_ofDual {X : Type u_1} [EDist X] (a b : X ᵒᵈ) :
edist (OrderDual.ofDual a) (OrderDual.ofDual b) = edist a b
source
instance instPseudoEMetricSpaceOrderDual {X : Type u_1} [PseudoEMetricSpace X] :
PseudoEMetricSpace X ᵒᵈ
Equations

- instPseudoEMetricSpaceOrderDual = inst✝

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

- instEMetricSpaceOrderDual = inst✝