mathlib documentation

topology.metric_space.emetric_space

Extended metric spaces #

This file is devoted to the definition and study of emetric_spaces, 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 emetric_space therefore extends uniform_space (and topological_space).

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

source
theorem uniformity_dist_of_mem_uniformity {α : Type u} {β : Type v} [linear_order β] {U : filter (α × α)} (z : β) (D : α → α → β) (H : ∀ (s : set (α × α)), s ∈ U ↔ ∃ (ε : β) (H : ε > z), ∀ {a b : α}, D a b < ε → (a, b) ∈ s) :
U = ⨅ (ε : β) (H : ε > z), 𝓟 {p : α × α | D p.fst p.snd < ε}

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

source
@[class]
structure has_edist (α : Type u_1) :
Type u_1

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

Instances
source
def uniform_space_of_edist {α : Type u} (edist : α → α → ℝ≥0∞) (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) :
uniform_space α

Creating a uniform space from an extended distance.

Equations
source
@[class]
structure pseudo_emetric_space (α : Type u) :
Type u

Extended (pseudo) metric spaces, with an extended distance edist possibly taking the value ∞

Each pseudo_emetric space induces a canonical uniform_space and hence a canonical topological_space. This is enforced in the type class definition, by extending the uniform_space structure. When instantiating a pseudo_emetric_space structure, the uniformity fields are not necessary, they will be filled in by default. There is a default value for the uniformity, that can be substituted in cases of interest, for instance when instantiating a pseudo_emetric_space structure on a product.

Continuity of edist is proved in topology.instances.ennreal

Instances
source
@[protected, instance]
def pseudo_emetric_space.to_uniform_space' {α : Type u} [pseudo_emetric_space α] :
uniform_space α
Equations
source
theorem edist_triangle_left {α : Type u} [pseudo_emetric_space α] (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} [pseudo_emetric_space α] (x y z : α) :
edist x y ≤ edist x z + edist y z
source
theorem edist_triangle4 {α : Type u} [pseudo_emetric_space α] (x y z t : α) :
edist x t ≤ edist x y + edist y z + edist z t
source
theorem edist_le_Ico_sum_edist {α : Type u} [pseudo_emetric_space α] (f : ℕ → α) {m n : ℕ} (h : m ≤ n) :
edist (f m) (f n) ≤ ∑ (i : ℕ) in finset.Ico m n, edist (f i) (f (i + 1))

The triangle (polygon) inequality for sequences of points; finset.Ico version.

source
theorem edist_le_range_sum_edist {α : Type u} [pseudo_emetric_space α] (f : ℕ → α) (n : ℕ) :
edist (f 0) (f n) ≤ ∑ (i : ℕ) in finset.range n, edist (f i) (f (i + 1))

The triangle (polygon) inequality for sequences of points; finset.range version.

source
theorem edist_le_Ico_sum_of_edist_le {α : Type u} [pseudo_emetric_space α] {f : ℕ → α} {m n : ℕ} (hmn : m ≤ n) {d : ℕ → ℝ≥0∞} (hd : ∀ {k : ℕ}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) :
edist (f m) (f n) ≤ ∑ (i : ℕ) in finset.Ico m n, d i

A version of edist_le_Ico_sum_edist with each intermediate distance replaced with an upper estimate.

source
theorem edist_le_range_sum_of_edist_le {α : Type u} [pseudo_emetric_space α] {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ≥0∞} (hd : ∀ {k : ℕ}, k < n → edist (f k) (f (k + 1)) ≤ d k) :
edist (f 0) (f n) ≤ ∑ (i : ℕ) in finset.range n, d i

A version of edist_le_range_sum_edist with each intermediate distance replaced with an upper estimate.

source
theorem uniformity_pseudoedist {α : Type u} [pseudo_emetric_space α] :
𝓤 α = ⨅ (ε : ℝ≥0∞) (H : ε > 0), 𝓟 {p : α × α | edist p.fst p.snd < ε}

Reformulation of the uniform structure in terms of the extended distance

source
theorem uniformity_basis_edist {α : Type u} [pseudo_emetric_space α] :
(𝓤 α).has_basis (λ (ε : ℝ≥0∞), 0 < ε) (λ (ε : ℝ≥0∞), {p : α × α | edist p.fst p.snd < ε})
source
theorem mem_uniformity_edist {α : Type u} [pseudo_emetric_space α] {s : set (α × α)} :
s ∈ 𝓤 α ↔ ∃ (ε : ℝ≥0∞) (H : ε > 0), ∀ {a b : α}, edist a b < ε → (a, b) ∈ s

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

source
@[protected]
theorem emetric.mk_uniformity_basis {α : Type u} [pseudo_emetric_space α] {β : Type u_1} {p : β → Prop} {f : β → ℝ≥0∞} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ℝ≥0∞), 0 < ε → (∃ (x : β) (hx : p x), f x ≤ ε)) :
(𝓤 α).has_basis p (λ (x : β), {p : α × α | edist p.fst p.snd < 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
@[protected]
theorem emetric.mk_uniformity_basis_le {α : Type u} [pseudo_emetric_space α] {β : Type u_1} {p : β → Prop} {f : β → ℝ≥0∞} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ℝ≥0∞), 0 < ε → (∃ (x : β) (hx : p x), f x ≤ ε)) :
(𝓤 α).has_basis p (λ (x : β), {p : α × α | edist p.fst p.snd ≤ 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} [pseudo_emetric_space α] :
(𝓤 α).has_basis (λ (ε : ℝ≥0∞), 0 < ε) (λ (ε : ℝ≥0∞), {p : α × α | edist p.fst p.snd ≤ ε})
source
theorem uniformity_basis_edist' {α : Type u} [pseudo_emetric_space α] (ε' : ℝ≥0∞) (hε' : 0 < ε') :
(𝓤 α).has_basis (λ (ε : ℝ≥0∞), ε ∈ set.Ioo 0 ε') (λ (ε : ℝ≥0∞), {p : α × α | edist p.fst p.snd < ε})
source
theorem uniformity_basis_edist_le' {α : Type u} [pseudo_emetric_space α] (ε' : ℝ≥0∞) (hε' : 0 < ε') :
(𝓤 α).has_basis (λ (ε : ℝ≥0∞), ε ∈ set.Ioo 0 ε') (λ (ε : ℝ≥0∞), {p : α × α | edist p.fst p.snd ≤ ε})
source
theorem uniformity_basis_edist_nnreal {α : Type u} [pseudo_emetric_space α] :
(𝓤 α).has_basis (λ (ε : ℝ≥0), 0 < ε) (λ (ε : ℝ≥0), {p : α × α | edist p.fst p.snd < ↑ε})
source
theorem uniformity_basis_edist_inv_nat {α : Type u} [pseudo_emetric_space α] :
(𝓤 α).has_basis (λ (_x : ℕ), true) (λ (n : ℕ), {p : α × α | edist p.fst p.snd < (↑n)⁻¹})
source
theorem uniformity_basis_edist_inv_two_pow {α : Type u} [pseudo_emetric_space α] :
(𝓤 α).has_basis (λ (_x : ℕ), true) (λ (n : ℕ), {p : α × α | edist p.fst p.snd < 2⁻¹ ^ n})
source
theorem edist_mem_uniformity {α : Type u} [pseudo_emetric_space α] {ε : ℝ≥0∞} (ε0 : 0 < ε) :
{p : α × α | edist p.fst p.snd < ε} ∈ 𝓤 α

Fixed size neighborhoods of the diagonal belong to the uniform structure

source
@[protected, instance]
def emetric.uniformity.filter.is_countably_generated {α : Type u} [pseudo_emetric_space α] :
(𝓤 α).is_countably_generated
source
theorem emetric.uniform_continuous_on_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : α → β} {s : set α} :
uniform_continuous_on f s ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (δ : ℝ≥0∞) (H : δ > 0), ∀ {a : α} {H : a ∈ s} {b : α} {H : b ∈ s}, edist a b < δ → edist (f a) (f b) < ε)

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

source
theorem emetric.uniform_continuous_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : α → β} :
uniform_continuous f ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (δ : ℝ≥0∞) (H : δ > 0), ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε)

ε-δ characterization of uniform continuity on pseudoemetric spaces

source
theorem emetric.uniform_embedding_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : α → β} :
uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧ ∀ (δ : ℝ≥0∞), δ > 0 → (∃ (ε : ℝ≥0∞) (H : ε > 0), ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ)

ε-δ characterization of uniform embeddings on pseudoemetric spaces

source
theorem emetric.controlled_of_uniform_embedding {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : α → β} :
uniform_embedding f → ((∀ (ε : ℝ≥0∞), ε > 0 → (∃ (δ : ℝ≥0∞) (H : δ > 0), ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε)) ∧ ∀ (δ : ℝ≥0∞), δ > 0 → (∃ (ε : ℝ≥0∞) (H : ε > 0), ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ))

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.

source
@[protected]
theorem emetric.cauchy_iff {α : Type u} [pseudo_emetric_space α] {f : filter α} :
cauchy f ↔ f ≠ ⊥ ∧ ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (t : set α) (H : t ∈ f), ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → edist x y < ε)

ε-δ characterization of Cauchy sequences on pseudoemetric spaces

source
theorem emetric.complete_of_convergent_controlled_sequences {α : Type u} [pseudo_emetric_space α] (B : ℕ → ℝ≥0∞) (hB : ∀ (n : ℕ), 0 < B n) (H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (u n) (u m) < B N) → (∃ (x : α), filter.tendsto u filter.at_top (𝓝 x))) :
complete_space α

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.

source
theorem emetric.complete_of_cauchy_seq_tendsto {α : Type u} [pseudo_emetric_space α] :
(∀ (u : ℕ → α), cauchy_seq u → (∃ (a : α), filter.tendsto u filter.at_top (𝓝 a))) → complete_space α

A sequentially complete pseudoemetric space is complete.

source
theorem emetric.tendsto_locally_uniformly_on_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] {ι : Type u_1} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :
tendsto_locally_uniformly_on F f p s ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∀ (x : β), x ∈ s → (∃ (t : set β) (H : t ∈ 𝓝[s] x), ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → edist (f y) (F n y) < ε)

Expressing locally uniform convergence on a set using edist.

source
theorem emetric.tendsto_uniformly_on_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :
tendsto_uniformly_on F f p s ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∀ᶠ (n : ι) in p, ∀ (x : β), x ∈ s → edist (f x) (F n x) < ε)

Expressing uniform convergence on a set using edist.

source
theorem emetric.tendsto_locally_uniformly_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] {ι : Type u_1} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} :
tendsto_locally_uniformly F f p ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∀ (x : β), ∃ (t : set β) (H : t ∈ 𝓝 x), ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → edist (f y) (F n y) < ε

Expressing locally uniform convergence using edist.

source
theorem emetric.tendsto_uniformly_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} :
tendsto_uniformly F f p ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε)

Expressing uniform convergence using edist.

source
def pseudo_emetric_space.replace_uniformity {α : Type u_1} [U : uniform_space α] (m : pseudo_emetric_space α) (H : 𝓤 α = 𝓤 α) :
pseudo_emetric_space α

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.

Equations
source
def pseudo_emetric_space.induced {α : Type u_1} {β : Type u_2} (f : α → β) (m : pseudo_emetric_space β) :
pseudo_emetric_space α

The extended pseudometric induced by a function taking values in a pseudoemetric space.

Equations
source
@[protected, instance]
def subtype.pseudo_emetric_space {α : Type u_1} {p : α → Prop} [pseudo_emetric_space α] :
pseudo_emetric_space (subtype p)

Pseudoemetric space instance on subsets of pseudoemetric spaces

Equations
source
theorem subtype.edist_eq {α : Type u} [pseudo_emetric_space α] {p : α → Prop} (x y : subtype p) :
edist x y = edist ↑x ↑y

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

source
@[protected, instance]
def add_opposite.pseudo_emetric_space {α : Type u_1} [pseudo_emetric_space α] :
pseudo_emetric_space αᵃᵒᵖ

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

Equations
source
@[protected, instance]
def mul_opposite.pseudo_emetric_space {α : Type u_1} [pseudo_emetric_space α] :
pseudo_emetric_space αᵐᵒᵖ

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

Equations
source
theorem mul_opposite.edist_unop {α : Type u} [pseudo_emetric_space α] (x y : αᵐᵒᵖ) :
edist (mul_opposite.unop x) (mul_opposite.unop y) = edist x y
source
theorem add_opposite.edist_unop {α : Type u} [pseudo_emetric_space α] (x y : αᵃᵒᵖ) :
edist (add_opposite.unop x) (add_opposite.unop y) = edist x y
source
theorem add_opposite.edist_op {α : Type u} [pseudo_emetric_space α] (x y : α) :
edist (add_opposite.op x) (add_opposite.op y) = edist x y
source
theorem mul_opposite.edist_op {α : Type u} [pseudo_emetric_space α] (x y : α) :
edist (mul_opposite.op x) (mul_opposite.op y) = edist x y
source
@[protected, instance]
noncomputable def prod.pseudo_emetric_space_max {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] :
pseudo_emetric_space (α × β)

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
source
theorem prod.edist_eq {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (x y : α × β) :
edist x y = max (edist x.fst y.fst) (edist x.snd y.snd)
source
@[protected, instance]
noncomputable def pseudo_emetric_space_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_emetric_space (π b)] :
pseudo_emetric_space (Π (b : β), π b)

The product of a finite number of pseudoemetric spaces, with the max distance, is still a pseudoemetric space. This construction would also work for infinite products, but it would not give rise to the product topology. Hence, we only formalize it in the good situation of finitely many spaces.

Equations
source
theorem edist_pi_def {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_emetric_space (π b)] (f g : Π (b : β), π b) :
edist f g = finset.univ.sup (λ (b : β), edist (f b) (g b))
source
@[simp]
theorem edist_pi_const {α : Type u} {β : Type v} [pseudo_emetric_space α] [fintype β] [nonempty β] (a b : α) :
edist (λ (x : β), a) (λ (_x : β), b) = edist a b
source
theorem edist_le_pi_edist {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_emetric_space (π b)] (f g : Π (b : β), π b) (b : β) :
edist (f b) (g b) ≤ edist f g
source
theorem edist_pi_le_iff {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_emetric_space (π b)] {f g : Π (b : β), π b} {d : ℝ≥0∞} :
edist f g ≤ d ↔ ∀ (b : β), edist (f b) (g b) ≤ d
source
def emetric.ball {α : Type u} [pseudo_emetric_space α] (x : α) (ε : ℝ≥0∞) :
set α

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

Equations
source
@[simp]
theorem emetric.mem_ball {α : Type u} [pseudo_emetric_space α] {x y : α} {ε : ℝ≥0∞} :
y ∈ emetric.ball x ε ↔ edist y x < ε
source
theorem emetric.mem_ball' {α : Type u} [pseudo_emetric_space α] {x y : α} {ε : ℝ≥0∞} :
y ∈ emetric.ball x ε ↔ edist x y < ε
source
def emetric.closed_ball {α : Type u} [pseudo_emetric_space α] (x : α) (ε : ℝ≥0∞) :
set α

emetric.closed_ball x ε is the set of all points y with edist y x ≤ ε

Equations
source
@[simp]
theorem emetric.mem_closed_ball {α : Type u} [pseudo_emetric_space α] {x y : α} {ε : ℝ≥0∞} :
y ∈ emetric.closed_ball x ε ↔ edist y x ≤ ε
source
@[simp]
theorem emetric.closed_ball_top {α : Type u} [pseudo_emetric_space α] (x : α) :
emetric.closed_ball x ⊤ = set.univ
source
theorem emetric.ball_subset_closed_ball {α : Type u} [pseudo_emetric_space α] {x : α} {ε : ℝ≥0∞} :
emetric.ball x ε ⊆ emetric.closed_ball x ε
source
theorem emetric.pos_of_mem_ball {α : Type u} [pseudo_emetric_space α] {x y : α} {ε : ℝ≥0∞} (hy : y ∈ emetric.ball x ε) :
0 < ε
source
theorem emetric.mem_ball_self {α : Type u} [pseudo_emetric_space α] {x : α} {ε : ℝ≥0∞} (h : 0 < ε) :
x ∈ emetric.ball x ε
source
theorem emetric.mem_closed_ball_self {α : Type u} [pseudo_emetric_space α] {x : α} {ε : ℝ≥0∞} :
x ∈ emetric.closed_ball x ε
source
theorem emetric.mem_ball_comm {α : Type u} [pseudo_emetric_space α] {x y : α} {ε : ℝ≥0∞} :
x ∈ emetric.ball y ε ↔ y ∈ emetric.ball x ε
source
theorem emetric.ball_subset_ball {α : Type u} [pseudo_emetric_space α] {x : α} {ε₁ ε₂ : ℝ≥0∞} (h : ε₁ ≤ ε₂) :
emetric.ball x ε₁ ⊆ emetric.ball x ε₂
source
theorem emetric.closed_ball_subset_closed_ball {α : Type u} [pseudo_emetric_space α] {x : α} {ε₁ ε₂ : ℝ≥0∞} (h : ε₁ ≤ ε₂) :
emetric.closed_ball x ε₁ ⊆ emetric.closed_ball x ε₂
source
theorem emetric.ball_disjoint {α : Type u} [pseudo_emetric_space α] {x y : α} {ε₁ ε₂ : ℝ≥0∞} (h : ε₁ + ε₂ ≤ edist x y) :
emetric.ball x ε₁ ∩ emetric.ball y ε₂ = ∅
source
theorem emetric.ball_subset {α : Type u} [pseudo_emetric_space α] {x y : α} {ε₁ ε₂ : ℝ≥0∞} (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y ≠ ⊤) :
emetric.ball x ε₁ ⊆ emetric.ball y ε₂
source
theorem emetric.exists_ball_subset_ball {α : Type u} [pseudo_emetric_space α] {x y : α} {ε : ℝ≥0∞} (h : y ∈ emetric.ball x ε) :
∃ (ε' : ℝ≥0∞) (H : ε' > 0), emetric.ball y ε' ⊆ emetric.ball x ε
source
theorem emetric.ball_eq_empty_iff {α : Type u} [pseudo_emetric_space α] {x : α} {ε : ℝ≥0∞} :
emetric.ball x ε = ∅ ↔ ε = 0
source
def emetric.edist_lt_top_setoid {α : Type u} [pseudo_emetric_space α] :
setoid α

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

Equations
source
@[simp]
theorem emetric.ball_zero {α : Type u} [pseudo_emetric_space α] {x : α} :
emetric.ball x 0 = ∅
source
theorem emetric.nhds_basis_eball {α : Type u} [pseudo_emetric_space α] {x : α} :
(𝓝 x).has_basis (λ (ε : ℝ≥0∞), 0 < ε) (emetric.ball x)
source
theorem emetric.nhds_basis_closed_eball {α : Type u} [pseudo_emetric_space α] {x : α} :
(𝓝 x).has_basis (λ (ε : ℝ≥0∞), 0 < ε) (emetric.closed_ball x)
source
theorem emetric.nhds_eq {α : Type u} [pseudo_emetric_space α] {x : α} :
𝓝 x = ⨅ (ε : ℝ≥0∞) (H : ε > 0), 𝓟 (emetric.ball x ε)
source
theorem emetric.mem_nhds_iff {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} :
s ∈ 𝓝 x ↔ ∃ (ε : ℝ≥0∞) (H : ε > 0), emetric.ball x ε ⊆ s
source
theorem emetric.is_open_iff {α : Type u} [pseudo_emetric_space α] {s : set α} :
is_open s ↔ ∀ (x : α), x ∈ s → (∃ (ε : ℝ≥0∞) (H : ε > 0), emetric.ball x ε ⊆ s)
source
theorem emetric.is_open_ball {α : Type u} [pseudo_emetric_space α] {x : α} {ε : ℝ≥0∞} :
is_open (emetric.ball x ε)
source
theorem emetric.is_closed_ball_top {α : Type u} [pseudo_emetric_space α] {x : α} :
is_closed (emetric.ball x ⊤)
source
theorem emetric.ball_mem_nhds {α : Type u} [pseudo_emetric_space α] (x : α) {ε : ℝ≥0∞} (ε0 : 0 < ε) :
emetric.ball x ε ∈ 𝓝 x
source
theorem emetric.closed_ball_mem_nhds {α : Type u} [pseudo_emetric_space α] (x : α) {ε : ℝ≥0∞} (ε0 : 0 < ε) :
emetric.closed_ball x ε ∈ 𝓝 x
source
theorem emetric.ball_prod_same {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (x : α) (y : β) (r : ℝ≥0∞) :
emetric.ball x r ×ˢ emetric.ball y r = emetric.ball (x, y) r
source
theorem emetric.closed_ball_prod_same {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] (x : α) (y : β) (r : ℝ≥0∞) :
emetric.closed_ball x r ×ˢ emetric.closed_ball y r = emetric.closed_ball (x, y) r
source
theorem emetric.mem_closure_iff {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} :
x ∈ closure s ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (y : α) (H : y ∈ s), edist x y < ε)

ε-characterization of the closure in pseudoemetric spaces

source
theorem emetric.tendsto_nhds {α : Type u} {β : Type v} [pseudo_emetric_space α] {f : filter β} {u : β → α} {a : α} :
filter.tendsto u f (𝓝 a) ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∀ᶠ (x : β) in f, edist (u x) a < ε)
source
theorem emetric.tendsto_at_top {α : Type u} {β : Type v} [pseudo_emetric_space α] [nonempty β] [semilattice_sup β] {u : β → α} {a : α} :
filter.tendsto u filter.at_top (𝓝 a) ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (N : β), ∀ (n : β), n ≥ N → edist (u n) a < ε)
source
@[nolint]
theorem emetric.cauchy_seq_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :
cauchy_seq u ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (N : β), ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → edist (u m) (u n) < ε)

In a pseudoemetric space, Cauchy sequences are characterized by the fact that, eventually, the pseudoedistance between its elements is arbitrarily small

source
theorem emetric.cauchy_seq_iff' {α : Type u} {β : Type v} [pseudo_emetric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :
cauchy_seq u ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (N : β), ∀ (n : β), n ≥ N → edist (u n) (u N) < ε)

A variation around the emetric characterization of Cauchy sequences

source
theorem emetric.cauchy_seq_iff_nnreal {α : Type u} {β : Type v} [pseudo_emetric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :
cauchy_seq u ↔ ∀ (ε : ℝ≥0), 0 < ε → (∃ (N : β), ∀ (n : β), N ≤ n → edist (u n) (u N) < ↑ε)

A variation of the emetric characterization of Cauchy sequences that deals with ℝ≥0 upper bounds.

source
theorem emetric.totally_bounded_iff {α : Type u} [pseudo_emetric_space α] {s : set α} :
totally_bounded s ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (t : set α), t.finite ∧ s ⊆ ⋃ (y : α) (H : y ∈ t), emetric.ball y ε)
source
theorem emetric.totally_bounded_iff' {α : Type u} [pseudo_emetric_space α] {s : set α} :
totally_bounded s ↔ ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (t : set α) (H : t ⊆ s), t.finite ∧ s ⊆ ⋃ (y : α) (H : y ∈ t), emetric.ball y ε)
source
theorem emetric.subset_countable_closure_of_almost_dense_set {α : Type u} [pseudo_emetric_space α] (s : set α) (hs : ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (t : set α), t.countable ∧ s ⊆ ⋃ (x : α) (H : x ∈ t), emetric.closed_ball x ε)) :
∃ (t : set α) (H : 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
theorem emetric.subset_countable_closure_of_compact {α : Type u} [pseudo_emetric_space α] {s : set α} (hs : is_compact s) :
∃ (t : set α) (H : t ⊆ s), t.countable ∧ s ⊆ closure t

A compact set in a pseudo emetric space is separable, i.e., it is a subset of the closure of a countable set.

source
theorem emetric.second_countable_of_sigma_compact (α : Type u) [pseudo_emetric_space α] [sigma_compact_space α] :
topological_space.second_countable_topology α

A sigma compact pseudo emetric space has second countable topology. This is not an instance to avoid a loop with sigma_compact_space_of_locally_compact_second_countable.

source
theorem emetric.second_countable_of_almost_dense_set {α : Type u} [pseudo_emetric_space α] (hs : ∀ (ε : ℝ≥0∞), ε > 0 → (∃ (t : set α), t.countable ∧ (⋃ (x : α) (H : x ∈ t), emetric.closed_ball x ε) = set.univ)) :
topological_space.second_countable_topology α
source
noncomputable def emetric.diam {α : Type u} [pseudo_emetric_space α] (s : set α) :
ℝ≥0∞

The diameter of a set in a pseudoemetric space, named emetric.diam

Equations
source
theorem emetric.diam_le_iff {α : Type u} [pseudo_emetric_space α] {s : set α} {d : ℝ≥0∞} :
emetric.diam s ≤ d ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → edist x y ≤ d
source
theorem emetric.diam_image_le_iff {α : Type u} {β : Type v} [pseudo_emetric_space α] {d : ℝ≥0∞} {f : β → α} {s : set β} :
emetric.diam (f '' s) ≤ d ↔ ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → edist (f x) (f y) ≤ d
source
theorem emetric.edist_le_of_diam_le {α : Type u} [pseudo_emetric_space α] {x y : α} {s : set α} {d : ℝ≥0∞} (hx : x ∈ s) (hy : y ∈ s) (hd : emetric.diam s ≤ d) :
edist x y ≤ d
source
theorem emetric.edist_le_diam_of_mem {α : Type u} [pseudo_emetric_space α] {x y : α} {s : set α} (hx : x ∈ s) (hy : y ∈ s) :
edist x y ≤ emetric.diam s

If two points belong to some set, their edistance is bounded by the diameter of the set

source
theorem emetric.diam_le {α : Type u} [pseudo_emetric_space α] {s : set α} {d : ℝ≥0∞} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → edist x y ≤ d) :
emetric.diam s ≤ d

If the distance between any two points in a set is bounded by some constant, this constant bounds the diameter.

source
theorem emetric.diam_subsingleton {α : Type u} [pseudo_emetric_space α] {s : set α} (hs : s.subsingleton) :
emetric.diam s = 0

The diameter of a subsingleton vanishes.

source
@[simp]
theorem emetric.diam_empty {α : Type u} [pseudo_emetric_space α] :
emetric.diam ∅ = 0

The diameter of the empty set vanishes

source
@[simp]
theorem emetric.diam_singleton {α : Type u} [pseudo_emetric_space α] {x : α} :
emetric.diam {x} = 0

The diameter of a singleton vanishes

source
theorem emetric.diam_Union_mem_option {α : Type u} [pseudo_emetric_space α] {ι : Type u_1} (o : option ι) (s : ι → set α) :
emetric.diam (⋃ (i : ι) (H : i ∈ o), s i) = ⨆ (i : ι) (H : i ∈ o), emetric.diam (s i)
source
theorem emetric.diam_insert {α : Type u} [pseudo_emetric_space α] {x : α} {s : set α} :
emetric.diam (insert x s) = max (⨆ (y : α) (H : y ∈ s), edist x y) (emetric.diam s)
source
theorem emetric.diam_pair {α : Type u} [pseudo_emetric_space α] {x y : α} :
emetric.diam {x, y} = edist x y
source
theorem emetric.diam_triple {α : Type u} [pseudo_emetric_space α] {x y z : α} :
emetric.diam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)
source
theorem emetric.diam_mono {α : Type u} [pseudo_emetric_space α] {s t : set α} (h : s ⊆ t) :
emetric.diam s ≤ emetric.diam t

The diameter is monotonous with respect to inclusion

source
theorem emetric.diam_union {α : Type u} [pseudo_emetric_space α] {x y : α} {s t : set α} (xs : x ∈ s) (yt : y ∈ t) :
emetric.diam (s ∪ t) ≤ emetric.diam s + edist x y + emetric.diam t

The diameter of a union is controlled by the diameter of the sets, and the edistance between two points in the sets.

source
theorem emetric.diam_union' {α : Type u} [pseudo_emetric_space α] {s t : set α} (h : (s ∩ t).nonempty) :
emetric.diam (s ∪ t) ≤ emetric.diam s + emetric.diam t
source
theorem emetric.diam_closed_ball {α : Type u} [pseudo_emetric_space α] {x : α} {r : ℝ≥0∞} :
emetric.diam (emetric.closed_ball x r) ≤ 2 * r
source
theorem emetric.diam_ball {α : Type u} [pseudo_emetric_space α] {x : α} {r : ℝ≥0∞} :
emetric.diam (emetric.ball x r) ≤ 2 * r
source
theorem emetric.diam_pi_le_of_le {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_emetric_space (π b)] {s : Π (b : β), set (π b)} {c : ℝ≥0∞} (h : ∀ (b : β), emetric.diam (s b) ≤ c) :
emetric.diam (set.univ.pi s) ≤ c
source
@[class]
structure emetric_space (α : Type u) :
Type u

We now define emetric_space, extending pseudo_emetric_space.

Instances
source
@[protected, instance]
def emetric_space.to_uniform_space' {γ : Type w} [emetric_space γ] :
uniform_space γ
Equations
source
@[simp]
theorem edist_eq_zero {γ : Type w} [emetric_space γ] {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} [emetric_space γ] {x y : γ} :
0 = edist x y ↔ x = y
source
theorem edist_le_zero {γ : Type w} [emetric_space γ] {x y : γ} :
edist x y ≤ 0 ↔ x = y
source
@[simp]
theorem edist_pos {γ : Type w} [emetric_space γ] {x y : γ} :
0 < edist x y ↔ x ≠ y
source
theorem eq_of_forall_edist_le {γ : Type w} [emetric_space γ] {x y : γ} (h : ∀ (ε : ℝ≥0∞), ε > 0 → edist x y ≤ ε) :
x = y

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

source
theorem uniform_embedding_iff' {β : Type v} {γ : Type w} [emetric_space γ] [emetric_space β] {f : γ → β} :
uniform_embedding f ↔ (∀ (ε : ℝ≥0∞), ε > 0 → (∃ (δ : ℝ≥0∞) (H : δ > 0), ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε)) ∧ ∀ (δ : ℝ≥0∞), δ > 0 → (∃ (ε : ℝ≥0∞) (H : ε > 0), ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ)

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.

source
@[protected, instance]
def to_separated {γ : Type w} [emetric_space γ] :
separated_space γ

An emetric space is separated

source
def emetric_of_t2_pseudo_emetric_space {α : Type u_1} [pseudo_emetric_space α] (h : separated_space α) :
emetric_space α

If a pseudo_emetric_space is separated, then it is an emetric_space.

Equations
source
def emetric_space.replace_uniformity {γ : Type u_1} [U : uniform_space γ] (m : emetric_space γ) (H : 𝓤 γ = 𝓤 γ) :
emetric_space γ

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.

Equations
source
def emetric_space.induced {γ : Type u_1} {β : Type u_2} (f : γ → β) (hf : function.injective f) (m : emetric_space β) :
emetric_space γ

The extended metric induced by an injective function taking values in a emetric space.

Equations
source
@[protected, instance]
def subtype.emetric_space {α : Type u_1} {p : α → Prop} [emetric_space α] :
emetric_space (subtype p)

Emetric space instance on subsets of emetric spaces

Equations
source
@[protected, instance]
def mul_opposite.emetric_space {α : Type u_1} [emetric_space α] :
emetric_space αᵐᵒᵖ

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

Equations
source
@[protected, instance]
def add_opposite.emetric_space {α : Type u_1} [emetric_space α] :
emetric_space αᵃᵒᵖ

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

Equations
source
@[protected, instance]
noncomputable def prod.emetric_space_max {β : Type v} {γ : Type w} [emetric_space γ] [emetric_space β] :
emetric_space (γ × β)

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
source
theorem uniformity_edist {γ : Type w} [emetric_space γ] :
𝓤 γ = ⨅ (ε : ℝ≥0∞) (H : ε > 0), 𝓟 {p : γ × γ | edist p.fst p.snd < ε}

Reformulation of the uniform structure in terms of the extended distance

source
@[protected, instance]
noncomputable def emetric_space_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), emetric_space (π b)] :
emetric_space (Π (b : β), π b)

The product of a finite number of emetric spaces, with the max distance, is still an emetric space. This construction would also work for infinite products, but it would not give rise to the product topology. Hence, we only formalize it in the good situation of finitely many spaces.

Equations
source
theorem emetric.countable_closure_of_compact {γ : Type w} [emetric_space γ] {s : set γ} (hs : is_compact s) :
∃ (t : set γ) (H : t ⊆ s), t.countable ∧ s = closure t

A compact set in an emetric space is separable, i.e., it is the closure of a countable set.

source
theorem emetric.diam_eq_zero_iff {γ : Type w} [emetric_space γ] {s : set γ} :
emetric.diam s = 0 ↔ s.subsingleton
source
theorem emetric.diam_pos_iff {γ : Type w} [emetric_space γ] {s : set γ} :
0 < emetric.diam s ↔ ∃ (x : γ) (H : x ∈ s) (y : γ) (H : y ∈ s), x ≠ y