# mathlibdocumentation

topology.metric_space.basic

# Metric spaces #

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

## Main definitions #

• `has_dist α`: Endows a space `α` with a function `dist a b`.
• `pseudo_metric_space α`: A space endowed with a distance function, which can be zero even if the two elements are non-equal.
• `metric.ball x ε`: The set of all points `y` with `dist y x < ε`.
• `metric.bounded s`: Whether a subset of a `pseudo_metric_space` is bounded.
• `metric_space α`: A `pseudo_metric_space` with the guarantee `dist x y = 0 → x = y`.

• `nndist a b`: `dist` as a function to the non-negative reals.
• `metric.closed_ball x ε`: The set of all points `y` with `dist y x ≤ ε`.
• `metric.sphere x ε`: The set of all points `y` with `dist y x = ε`.
• `proper_space α`: A `pseudo_metric_space` where all closed balls are compact.
• `metric.diam s` : The `supr` of the distances of members of `s`. Defined in terms of `emetric.diam`, for better handling of the case when it should be infinite.

TODO (anyone): Add "Main results" section.

## Implementation notes #

Since a lot of elementary properties don't require `eq_of_dist_eq_zero` we start setting up the theory of `pseudo_metric_space`, where we don't require `dist x y = 0 → x = y` and we specialize to `metric_space` at the end.

## Tags #

metric, pseudo_metric, dist

def uniform_space_of_dist {α : Type u} (dist : α → α → ) (dist_self : ∀ (x : α), dist x x = 0) (dist_comm : ∀ (x y : α), dist x y = dist y x) (dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z) :

Construct a uniform structure from a distance function and metric space axioms

Equations
@[class]
structure has_dist (α : Type u_1) :
Type u_1
• dist : α → α →

The distance function (given an ambient metric space on `α`), which returns a nonnegative real number `dist x y` given `x y : α`.

Instances
@[class]
structure pseudo_metric_space (α : Type u) :
Type u

Metric space

Each metric 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 `metric_space` structure, the uniformity fields are not necessary, they will be filled in by default. In the same way, each metric space induces an emetric space structure. It is included in the structure, but filled in by default.

Instances
@[instance]
def metric_space.to_uniform_space' {α : Type u}  :
Equations
@[instance]
def pseudo_metric_space.to_has_edist {α : Type u}  :
Equations
@[simp]
theorem dist_self {α : Type u} (x : α) :
dist x x = 0
theorem dist_comm {α : Type u} (x y : α) :
dist x y = dist y x
theorem edist_dist {α : Type u} (x y : α) :
theorem dist_triangle {α : Type u} (x y z : α) :
dist x z dist x y + dist y z
theorem dist_triangle_left {α : Type u} (x y z : α) :
dist x y dist z x + dist z y
theorem dist_triangle_right {α : Type u} (x y z : α) :
dist x y dist x z + dist y z
theorem dist_triangle4 {α : Type u} (x y z w : α) :
dist x w dist x y + dist y z + dist z w
theorem dist_triangle4_left {α : Type u} (x₁ y₁ x₂ y₂ : α) :
dist x₂ y₂ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
theorem dist_triangle4_right {α : Type u} (x₁ y₁ x₂ y₂ : α) :
dist x₁ y₁ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
theorem dist_le_Ico_sum_dist {α : Type u} (f : → α) {m n : } (h : m n) :
dist (f m) (f n) ∑ (i : ) in n, dist (f i) (f (i + 1))

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

theorem dist_le_range_sum_dist {α : Type u} (f : → α) (n : ) :
dist (f 0) (f n) ∑ (i : ) in , dist (f i) (f (i + 1))

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

theorem dist_le_Ico_sum_of_dist_le {α : Type u} {f : → α} {m n : } (hmn : m n) {d : } (hd : ∀ {k : }, m kk < ndist (f k) (f (k + 1)) d k) :
dist (f m) (f n) ∑ (i : ) in n, d i

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

theorem dist_le_range_sum_of_dist_le {α : Type u} {f : → α} (n : ) {d : } (hd : ∀ {k : }, k < ndist (f k) (f (k + 1)) d k) :
dist (f 0) (f n) ∑ (i : ) in , d i

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

theorem swap_dist {α : Type u}  :
theorem abs_dist_sub_le {α : Type u} (x y z : α) :
abs (dist x z - dist y z) dist x y
theorem dist_nonneg {α : Type u} {x y : α} :
0 dist x y
@[simp]
theorem abs_dist {α : Type u} {a b : α} :
abs (dist a b) = dist a b
def nndist {α : Type u} (a b : α) :

Distance as a nonnegative real number.

Equations
theorem nndist_edist {α : Type u} (x y : α) :
y = (edist x y).to_nnreal

Express `nndist` in terms of `edist`

theorem edist_nndist {α : Type u} (x y : α) :
y = (nndist x y)

Express `edist` in terms of `nndist`

@[simp]
theorem ennreal_coe_nndist {α : Type u} (x y : α) :
(nndist x y) = y
@[simp]
theorem edist_lt_coe {α : Type u} {x y : α} {c : ℝ≥0} :
y < c y < c
@[simp]
theorem edist_le_coe {α : Type u} {x y : α} {c : ℝ≥0} :
y c y c
theorem edist_ne_top {α : Type u} (x y : α) :
y

In a pseudometric space, the extended distance is always finite

theorem edist_lt_top {α : Type u_1} (x y : α) :
y <

In a pseudometric space, the extended distance is always finite

@[simp]
theorem nndist_self {α : Type u} (a : α) :
a = 0

`nndist x x` vanishes

theorem dist_nndist {α : Type u} (x y : α) :
dist x y = (nndist x y)

Express `dist` in terms of `nndist`

@[simp]
theorem coe_nndist {α : Type u} (x y : α) :
(nndist x y) = dist x y
@[simp]
theorem dist_lt_coe {α : Type u} {x y : α} {c : ℝ≥0} :
dist x y < c y < c
@[simp]
theorem dist_le_coe {α : Type u} {x y : α} {c : ℝ≥0} :
dist x y c y c
theorem nndist_dist {α : Type u} (x y : α) :

Express `nndist` in terms of `dist`

theorem nndist_comm {α : Type u} (x y : α) :
y = x
theorem nndist_triangle {α : Type u} (x y z : α) :
z y + z

Triangle inequality for the nonnegative distance

theorem nndist_triangle_left {α : Type u} (x y z : α) :
y x + y
theorem nndist_triangle_right {α : Type u} (x y z : α) :
y z + z
theorem dist_edist {α : Type u} (x y : α) :
dist x y = (edist x y).to_real

Express `dist` in terms of `edist`

def metric.ball {α : Type u} (x : α) (ε : ) :
set α

`ball x ε` is the set of all points `y` with `dist y x < ε`

Equations
• ε = {y : α | dist y x < ε}
@[simp]
theorem metric.mem_ball {α : Type u} {x y : α} {ε : } :
y ε dist y x < ε
theorem metric.mem_ball' {α : Type u} {x y : α} {ε : } :
y ε dist x y < ε
@[simp]
theorem metric.nonempty_ball {α : Type u} {x : α} {ε : } (h : 0 < ε) :
theorem metric.ball_eq_ball {α : Type u} (ε : ) (x : α) :
{p : α × α | dist p.snd p.fst < ε} = ε
theorem metric.ball_eq_ball' {α : Type u} (ε : ) (x : α) :
{p : α × α | dist p.fst p.snd < ε} = ε
def metric.closed_ball {α : Type u} (x : α) (ε : ) :
set α

`closed_ball x ε` is the set of all points `y` with `dist y x ≤ ε`

Equations
@[simp]
theorem metric.mem_closed_ball {α : Type u} {x y : α} {ε : } :
y dist y x ε
def metric.sphere {α : Type u} (x : α) (ε : ) :
set α

`sphere x ε` is the set of all points `y` with `dist y x = ε`

Equations
@[simp]
theorem metric.mem_sphere {α : Type u} {x y : α} {ε : } :
y dist y x = ε
theorem metric.mem_closed_ball' {α : Type u} {x y : α} {ε : } :
y dist x y ε
theorem metric.nonempty_closed_ball {α : Type u} {x : α} {ε : } (h : 0 ε) :
theorem metric.ball_subset_closed_ball {α : Type u} {x : α} {ε : } :
ε
theorem metric.sphere_subset_closed_ball {α : Type u} {x : α} {ε : } :
theorem metric.sphere_disjoint_ball {α : Type u} {x : α} {ε : } :
disjoint ε) ε)
@[simp]
theorem metric.ball_union_sphere {α : Type u} {x : α} {ε : } :
ε =
@[simp]
theorem metric.sphere_union_ball {α : Type u} {x : α} {ε : } :
ε =
@[simp]
theorem metric.closed_ball_diff_sphere {α : Type u} {x : α} {ε : } :
\ = ε
@[simp]
theorem metric.closed_ball_diff_ball {α : Type u} {x : α} {ε : } :
\ ε =
theorem metric.pos_of_mem_ball {α : Type u} {x y : α} {ε : } (hy : y ε) :
0 < ε
theorem metric.mem_ball_self {α : Type u} {x : α} {ε : } (h : 0 < ε) :
x ε
theorem metric.mem_closed_ball_self {α : Type u} {x : α} {ε : } (h : 0 ε) :
x
theorem metric.mem_ball_comm {α : Type u} {x y : α} {ε : } :
x ε y ε
theorem metric.ball_subset_ball {α : Type u} {x : α} {ε₁ ε₂ : } (h : ε₁ ε₂) :
ε₁ ε₂
theorem metric.closed_ball_subset_closed_ball {α : Type u} {x : α} {ε₁ ε₂ : } (h : ε₁ ε₂) :
theorem metric.closed_ball_subset_ball {α : Type u} {x : α} {ε₁ ε₂ : } (h : ε₁ < ε₂) :
ε₂
theorem metric.ball_disjoint {α : Type u} {x y : α} {ε₁ ε₂ : } (h : ε₁ + ε₂ dist x y) :
ε₁ ε₂ =
theorem metric.ball_disjoint_same {α : Type u} {x y : α} {ε : } (h : ε dist x y / 2) :
ε ε =
theorem metric.ball_subset {α : Type u} {x y : α} {ε₁ ε₂ : } (h : dist x y ε₂ - ε₁) :
ε₁ ε₂
theorem metric.ball_half_subset {α : Type u} {x : α} {ε : } (y : α) (h : y / 2)) :
/ 2) ε
theorem metric.exists_ball_subset_ball {α : Type u} {x y : α} {ε : } (h : y ε) :
∃ (ε' : ) (H : ε' > 0), ε' ε
@[simp]
theorem metric.ball_eq_empty_iff_nonpos {α : Type u} {x : α} {ε : } :
ε = ε 0
@[simp]
theorem metric.closed_ball_eq_empty_iff_neg {α : Type u} {x : α} {ε : } :
ε < 0
@[simp]
theorem metric.ball_zero {α : Type u} {x : α} :
0 =
theorem metric.uniformity_basis_dist {α : Type u}  :
(𝓤 α).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), {p : α × α | dist p.fst p.snd < ε})
theorem metric.mk_uniformity_basis {α : Type u} {β : Type u_1} {p : β → Prop} {f : β → } (hf₀ : ∀ (i : β), p i0 < f i) (hf : ∀ ⦃ε : ⦄, 0 < ε(∃ (i : β) (hi : p i), f i ε)) :
(𝓤 α).has_basis p (λ (i : β), {p : α × α | dist p.fst p.snd < f i})

Given `f : β → ℝ`, 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_dist`, `uniformity_basis_dist_inv_nat_succ`, and `uniformity_basis_dist_inv_nat_pos`.

theorem metric.uniformity_basis_dist_inv_nat_succ {α : Type u}  :
(𝓤 α).has_basis (λ (_x : ), true) (λ (n : ), {p : α × α | dist p.fst p.snd < 1 / (n + 1)})
theorem metric.uniformity_basis_dist_inv_nat_pos {α : Type u}  :
(𝓤 α).has_basis (λ (n : ), 0 < n) (λ (n : ), {p : α × α | dist p.fst p.snd < 1 / n})
theorem metric.uniformity_basis_dist_pow {α : Type u} {r : } (h0 : 0 < r) (h1 : r < 1) :
(𝓤 α).has_basis (λ (n : ), true) (λ (n : ), {p : α × α | dist p.fst p.snd < r ^ n})
theorem metric.uniformity_basis_dist_lt {α : Type u} {R : } (hR : 0 < R) :
(𝓤 α).has_basis (λ (r : ), 0 < r r < R) (λ (r : ), {p : α × α | dist p.fst p.snd < r})
theorem metric.mk_uniformity_basis_le {α : Type u} {β : Type u_1} {p : β → Prop} {f : β → } (hf₀ : ∀ (x : β), p x0 < f x) (hf : ∀ (ε : ), 0 < ε(∃ (x : β) (hx : p x), f x ε)) :
(𝓤 α).has_basis p (λ (x : β), {p : α × α | dist p.fst p.snd f x})

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

Currently we have only one specific basis `uniformity_basis_dist_le` based on this constructor. More can be easily added if needed in the future.

theorem metric.uniformity_basis_dist_le {α : Type u}  :
(𝓤 α).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), {p : α × α | dist p.fst p.snd ε})

Contant size closed neighborhoods of the diagonal form a basis of the uniformity filter.

theorem metric.uniformity_basis_dist_le_pow {α : Type u} {r : } (h0 : 0 < r) (h1 : r < 1) :
(𝓤 α).has_basis (λ (n : ), true) (λ (n : ), {p : α × α | dist p.fst p.snd r ^ n})
theorem metric.mem_uniformity_dist {α : Type u} {s : set × α)} :
s 𝓤 α ∃ (ε : ) (H : ε > 0), ∀ {a b : α}, dist a b < ε(a, b) s
theorem metric.dist_mem_uniformity {α : Type u} {ε : } (ε0 : 0 < ε) :
{p : α × α | dist p.fst p.snd < ε} 𝓤 α

A constant size neighborhood of the diagonal is an entourage.

theorem metric.uniform_continuous_iff {α : Type u} {β : Type v} {f : α → β} :
∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {a b : α}, dist a b < δdist (f a) (f b) < ε)
theorem metric.uniform_continuous_on_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} :
∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (x y : α), x sy sdist x y < δdist (f x) (f y) < ε)
theorem metric.uniform_embedding_iff {α : Type u} {β : Type v} {f : α → β} :
∀ (δ : ), δ > 0(∃ (ε : ) (H : ε > 0), ∀ {a b : α}, dist (f a) (f b) < εdist a b < δ)
theorem metric.controlled_of_uniform_embedding {α : Type u} {β : Type v} {f : α → β} :
((∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {a b : α}, dist a b < δdist (f a) (f b) < ε)) ∀ (δ : ), δ > 0(∃ (ε : ) (H : ε > 0), ∀ {a b : α}, dist (f a) (f b) < εdist a b < δ))

If a map between pseudometric spaces is a uniform embedding then the distance between `f x` and `f y` is controlled in terms of the distance between `x` and `y`.

theorem metric.totally_bounded_iff {α : Type u} {s : set α} :
∀ (ε : ), ε > 0(∃ (t : set α), t.finite s ⋃ (y : α) (H : y t), ε)
theorem metric.totally_bounded_of_finite_discretization {α : Type u} {s : set α} (H : ∀ (ε : ), ε > 0(∃ (β : Type u) [_inst_2 : fintype β] (F : s → β), ∀ (x y : s), F x = F y y < ε)) :

A pseudometric space space is totally bounded if one can reconstruct up to any ε>0 any element of the space from finitely many data.

theorem metric.finite_approx_of_totally_bounded {α : Type u} {s : set α} (hs : totally_bounded s) (ε : ) (H : ε > 0) :
∃ (t : set α) (H : t s), t.finite s ⋃ (y : α) (H : y t), ε
theorem metric.tendsto_locally_uniformly_on_iff {α : Type u} {β : Type v} {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :
s ∀ (ε : ), ε > 0∀ (x : β), x s(∃ (t : set β) (H : t 𝓝[s] x), ∀ᶠ (n : ι) in p, ∀ (y : β), y tdist (f y) (F n y) < ε)

Expressing locally uniform convergence on a set using `dist`.

theorem metric.tendsto_uniformly_on_iff {α : Type u} {β : Type v} {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :
p s ∀ (ε : ), ε > 0(∀ᶠ (n : ι) in p, ∀ (x : β), x sdist (f x) (F n x) < ε)

Expressing uniform convergence on a set using `dist`.

theorem metric.tendsto_locally_uniformly_iff {α : Type u} {β : Type v} {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} :
∀ (ε : ), ε > 0∀ (x : β), ∃ (t : set β) (H : t 𝓝 x), ∀ᶠ (n : ι) in p, ∀ (y : β), y tdist (f y) (F n y) < ε

Expressing locally uniform convergence using `dist`.

theorem metric.tendsto_uniformly_iff {α : Type u} {β : Type v} {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} :
p ∀ (ε : ), ε > 0(∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε)

Expressing uniform convergence using `dist`.

theorem metric.cauchy_iff {α : Type u} {f : filter α} :
f.ne_bot ∀ (ε : ), ε > 0(∃ (t : set α) (H : t f), ∀ (x y : α), x ty tdist x y < ε)
theorem metric.nhds_basis_ball {α : Type u} {x : α} :
(𝓝 x).has_basis (λ (ε : ), 0 < ε) (metric.ball x)
theorem metric.mem_nhds_iff {α : Type u} {x : α} {s : set α} :
s 𝓝 x ∃ (ε : ) (H : ε > 0), ε s
theorem metric.eventually_nhds_iff {α : Type u} {x : α} {p : α → Prop} :
(∀ᶠ (y : α) in 𝓝 x, p y) ∃ (ε : ) (H : ε > 0), ∀ ⦃y : α⦄, dist y x < εp y
theorem metric.eventually_nhds_iff_ball {α : Type u} {x : α} {p : α → Prop} :
(∀ᶠ (y : α) in 𝓝 x, p y) ∃ (ε : ) (H : ε > 0), ∀ (y : α), y εp y
theorem metric.nhds_basis_closed_ball {α : Type u} {x : α} :
(𝓝 x).has_basis (λ (ε : ), 0 < ε)
theorem metric.nhds_basis_ball_inv_nat_succ {α : Type u} {x : α} :
(𝓝 x).has_basis (λ (_x : ), true) (λ (n : ), (1 / (n + 1)))
theorem metric.nhds_basis_ball_inv_nat_pos {α : Type u} {x : α} :
(𝓝 x).has_basis (λ (n : ), 0 < n) (λ (n : ), (1 / n))
theorem metric.nhds_basis_ball_pow {α : Type u} {x : α} {r : } (h0 : 0 < r) (h1 : r < 1) :
(𝓝 x).has_basis (λ (n : ), true) (λ (n : ), (r ^ n))
theorem metric.nhds_basis_closed_ball_pow {α : Type u} {x : α} {r : } (h0 : 0 < r) (h1 : r < 1) :
(𝓝 x).has_basis (λ (n : ), true) (λ (n : ), (r ^ n))
theorem metric.is_open_iff {α : Type u} {s : set α} :
∀ (x : α), x s(∃ (ε : ) (H : ε > 0), ε s)
theorem metric.is_open_ball {α : Type u} {x : α} {ε : } :
theorem metric.ball_mem_nhds {α : Type u} (x : α) {ε : } (ε0 : 0 < ε) :
ε 𝓝 x
theorem metric.closed_ball_mem_nhds {α : Type u} (x : α) {ε : } (ε0 : 0 < ε) :
theorem metric.nhds_within_basis_ball {α : Type u} {x : α} {s : set α} :
(𝓝[s] x).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), ε s)
theorem metric.mem_nhds_within_iff {α : Type u} {x : α} {s t : set α} :
s 𝓝[t] x ∃ (ε : ) (H : ε > 0), ε t s
theorem metric.tendsto_nhds_within_nhds_within {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} {a : α} {b : β} :
(𝓝[s] a) (𝓝[t] b) ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {x : α}, x sdist x a < δf x t dist (f x) b < ε)
theorem metric.tendsto_nhds_within_nhds {α : Type u} {β : Type v} {s : set α} {f : α → β} {a : α} {b : β} :
(𝓝[s] a) (𝓝 b) ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {x : α}, x sdist x a < δdist (f x) b < ε)
theorem metric.tendsto_nhds_nhds {α : Type u} {β : Type v} {f : α → β} {a : α} {b : β} :
(𝓝 a) (𝓝 b) ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {x : α}, dist x a < δdist (f x) b < ε)
theorem metric.continuous_at_iff {α : Type u} {β : Type v} {f : α → β} {a : α} :
∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {x : α}, dist x a < δdist (f x) (f a) < ε)
theorem metric.continuous_within_at_iff {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} :
a ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {x : α}, x sdist x a < δdist (f x) (f a) < ε)
theorem metric.continuous_on_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} :
∀ (b : α), b s∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (a : α), a sdist a b < δdist (f a) (f b) < ε)
theorem metric.continuous_iff {α : Type u} {β : Type v} {f : α → β} :
∀ (b : α) (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (a : α), dist a b < δdist (f a) (f b) < ε)
theorem metric.tendsto_nhds {α : Type u} {β : Type v} {f : filter β} {u : β → α} {a : α} :
(𝓝 a) ∀ (ε : ), ε > 0(∀ᶠ (x : β) in f, dist (u x) a < ε)
theorem metric.continuous_at_iff' {α : Type u} {β : Type v} {f : β → α} {b : β} :
∀ (ε : ), ε > 0(∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε)
theorem metric.continuous_within_at_iff' {α : Type u} {β : Type v} {f : β → α} {b : β} {s : set β} :
b ∀ (ε : ), ε > 0(∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε)
theorem metric.continuous_on_iff' {α : Type u} {β : Type v} {f : β → α} {s : set β} :
∀ (b : β), b s∀ (ε : ), ε > 0(∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε)
theorem metric.continuous_iff' {α : Type u} {β : Type v} {f : β → α} :
∀ (a : β) (ε : ), ε > 0(∀ᶠ (x : β) in 𝓝 a, dist (f x) (f a) < ε)
theorem metric.tendsto_at_top {α : Type u} {β : Type v} [nonempty β] {u : β → α} {a : α} :
(𝓝 a) ∀ (ε : ), ε > 0(∃ (N : β), ∀ (n : β), n Ndist (u n) a < ε)
theorem metric.tendsto_at_top' {α : Type u} {β : Type v} [nonempty β] [no_top_order β] {u : β → α} {a : α} :
(𝓝 a) ∀ (ε : ), ε > 0(∃ (N : β), ∀ (n : β), n > Ndist (u n) a < ε)

A variant of `tendsto_at_top` that uses `∃ N, ∀ n > N, ...` rather than `∃ N, ∀ n ≥ N, ...`

theorem metric.is_open_singleton_iff {X : Type u_1} {x : X} :
is_open {x} ∃ (ε : ) (H : ε > 0), ∀ (y : X), dist y x < εy = x
theorem metric.exists_ball_inter_eq_singleton_of_mem_discrete {α : Type u} {s : set α} {x : α} (hx : x s) :
∃ (ε : ) (H : ε > 0), ε s = {x}

Given a point `x` in a discrete subset `s` of a pseudometric space, there is an open ball centered at `x` and intersecting `s` only at `x`.

theorem metric.exists_closed_ball_inter_eq_singleton_of_discrete {α : Type u} {s : set α} {x : α} (hx : x s) :
∃ (ε : ) (H : ε > 0), s = {x}

Given a point `x` in a discrete subset `s` of a pseudometric space, there is a closed ball of positive radius centered at `x` and intersecting `s` only at `x`.

theorem pseudo_metric.uniformity_basis_edist {α : Type u}  :
(𝓤 α).has_basis (λ (ε : ℝ≥0∞), 0 < ε) (λ (ε : ℝ≥0∞), {p : α × α | edist p.fst p.snd < ε})

Expressing the uniformity in terms of `edist`

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

A pseudometric space induces a pseudoemetric space

Equations
theorem metric.emetric_ball {α : Type u} {x : α} {ε : } :
= ε

Balls defined using the distance or the edistance coincide

theorem metric.emetric_ball_nnreal {α : Type u} {x : α} {ε : ℝ≥0} :
= ε

Balls defined using the distance or the edistance coincide

theorem metric.emetric_closed_ball {α : Type u} {x : α} {ε : } (h : 0 ε) :

Closed balls defined using the distance or the edistance coincide

theorem metric.emetric_closed_ball_nnreal {α : Type u} {x : α} {ε : ℝ≥0} :

Closed balls defined using the distance or the edistance coincide

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

Build a new pseudometric space from an old one where the bundled uniform structure is provably (but typically non-definitionaly) equal to some given uniform structure. See Note [forgetful inheritance].

Equations
def pseudo_emetric_space.to_pseudo_metric_space_of_dist {α : Type u} [e : pseudo_emetric_space α] (dist : α → α → ) (edist_ne_top : ∀ (x y : α), y ) (h : ∀ (x y : α), dist x y = (edist x y).to_real) :

One gets a pseudometric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the pseudometric space and the pseudoemetric space. In this definition, the distance is given separately, to be able to prescribe some expression which is not defeq to the push-forward of the edistance to reals.

Equations
def pseudo_emetric_space.to_pseudo_metric_space {α : Type u} [e : emetric_space α] (h : ∀ (x y : α), y ) :

One gets a pseudometric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the pseudometric space and the emetric space.

Equations
theorem metric.complete_of_convergent_controlled_sequences {α : Type u} (B : ) (hB : ∀ (n : ), 0 < B n) (H : ∀ (u : → α), (∀ (N n m : ), N nN mdist (u n) (u m) < B N)(∃ (x : α), (𝓝 x))) :

A very useful criterion to show that a space is complete is to show that all sequences which satisfy a bound of the form `dist (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.

theorem metric.complete_of_cauchy_seq_tendsto {α : Type u}  :
(∀ (u : → α), (∃ (a : α), (𝓝 a)))
@[instance]

Instantiate the reals as a pseudometric space.

Equations
theorem real.dist_eq (x y : ) :
dist x y = abs (x - y)
theorem real.dist_0_eq_abs (x : ) :
dist x 0 = abs x
theorem real.dist_left_le_of_mem_interval {x y z : } (h : y z) :
dist x y dist x z
theorem real.dist_right_le_of_mem_interval {x y z : } (h : y z) :
dist y z dist x z
theorem real.dist_le_of_mem_interval {x y x' y' : } (hx : x y') (hy : y y') :
dist x y dist x' y'
theorem real.dist_le_of_mem_Icc {x y x' y' : } (hx : x set.Icc x' y') (hy : y set.Icc x' y') :
dist x y dist x' y'
theorem real.dist_le_of_mem_Icc_01 {x y : } (hx : x 1) (hy : y 1) :
dist x y 1
@[instance]
theorem closed_ball_Icc {x r : } :
= set.Icc (x - r) (x + r)
theorem totally_bounded_Icc {α : Type u} (a b : α) :
theorem totally_bounded_Ico {α : Type u} (a b : α) :
theorem totally_bounded_Ioc {α : Type u} (a b : α) :
theorem totally_bounded_Ioo {α : Type u} (a b : α) :
theorem squeeze_zero' {α : Type u_1} {f g : α → } {t₀ : filter α} (hf : ∀ᶠ (t : α) in t₀, 0 f t) (hft : ∀ᶠ (t : α) in t₀, f t g t) (g0 : t₀ (𝓝 0)) :
t₀ (𝓝 0)

Special case of the sandwich theorem; see `tendsto_of_tendsto_of_tendsto_of_le_of_le'` for the general case.

theorem squeeze_zero {α : Type u_1} {f g : α → } {t₀ : filter α} (hf : ∀ (t : α), 0 f t) (hft : ∀ (t : α), f t g t) (g0 : t₀ (𝓝 0)) :
t₀ (𝓝 0)

Special case of the sandwich theorem; see `tendsto_of_tendsto_of_tendsto_of_le_of_le` and `tendsto_of_tendsto_of_tendsto_of_le_of_le'` for the general case.

theorem metric.uniformity_eq_comap_nhds_zero {α : Type u}  :
𝓤 α = filter.comap (λ (p : α × α), dist p.fst p.snd) (𝓝 0)
theorem cauchy_seq_iff_tendsto_dist_at_top_0 {α : Type u} {β : Type v} [nonempty β] {u : β → α} :
filter.tendsto (λ (n : β × β), dist (u n.fst) (u n.snd)) filter.at_top (𝓝 0)
theorem tendsto_uniformity_iff_dist_tendsto_zero {α : Type u} {ι : Type u_1} {f : ι → α × α} {p : filter ι} :
(𝓤 α) filter.tendsto (λ (x : ι), dist (f x).fst (f x).snd) p (𝓝 0)
theorem filter.tendsto.congr_dist {α : Type u} {ι : Type u_1} {f₁ f₂ : ι → α} {p : filter ι} {a : α} (h₁ : p (𝓝 a)) (h : filter.tendsto (λ (x : ι), dist (f₁ x) (f₂ x)) p (𝓝 0)) :
p (𝓝 a)
theorem tendsto_of_tendsto_of_dist {α : Type u} {ι : Type u_1} {f₁ f₂ : ι → α} {p : filter ι} {a : α} (h₁ : p (𝓝 a)) (h : filter.tendsto (λ (x : ι), dist (f₁ x) (f₂ x)) p (𝓝 0)) :
p (𝓝 a)

Alias of `filter.tendsto.congr_dist`.

theorem tendsto_iff_of_dist {α : Type u} {ι : Type u_1} {f₁ f₂ : ι → α} {p : filter ι} {a : α} (h : filter.tendsto (λ (x : ι), dist (f₁ x) (f₂ x)) p (𝓝 0)) :
p (𝓝 a) p (𝓝 a)
@[nolint]
theorem metric.cauchy_seq_iff {α : Type u} {β : Type v} [nonempty β] {u : β → α} :
∀ (ε : ), ε > 0(∃ (N : β), ∀ (m n : β), m Nn Ndist (u m) (u n) < ε)

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

theorem metric.cauchy_seq_iff' {α : Type u} {β : Type v} [nonempty β] {u : β → α} :
∀ (ε : ), ε > 0(∃ (N : β), ∀ (n : β), n Ndist (u n) (u N) < ε)

A variation around the pseudometric characterization of Cauchy sequences

theorem cauchy_seq_of_le_tendsto_0 {α : Type u} {β : Type v} [nonempty β] {s : β → α} (b : β → ) (h : ∀ (n m N : β), N nN mdist (s n) (s m) b N) (h₀ : (𝓝 0)) :

If the distance between `s n` and `s m`, `n, m ≥ N` is bounded above by `b N` and `b` converges to zero, then `s` is a Cauchy sequence.

theorem cauchy_seq_bdd {α : Type u} {u : → α} (hu : cauchy_seq u) :
∃ (R : ) (H : R > 0), ∀ (m n : ), dist (u m) (u n) < R

A Cauchy sequence on the natural numbers is bounded.

theorem cauchy_seq_iff_le_tendsto_0 {α : Type u} {s : → α} :
∃ (b : ), (∀ (n : ), 0 b n) (∀ (n m N : ), N nN mdist (s n) (s m) b N) (𝓝 0)

Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.

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

Pseudometric space structure pulled back by a function.

Equations
@[instance]
def subtype.psudo_metric_space {α : Type u_1} {p : α → Prop} [t : pseudo_metric_space α] :
Equations
theorem subtype.pseudo_dist_eq {α : Type u} {p : α → Prop} (x y : subtype p) :
dist x y = y
@[instance]
Equations
theorem nnreal.dist_eq (a b : ℝ≥0) :
dist a b = abs (a - b)
theorem nnreal.nndist_eq (a b : ℝ≥0) :
b = max (a - b) (b - a)
@[instance]
def prod.pseudo_metric_space_max {α : Type u} {β : Type v}  :
Equations
theorem prod.dist_eq {α : Type u} {β : Type v} {x y : α × β} :
dist x y = max (dist x.fst y.fst) (dist x.snd y.snd)
theorem ball_prod_same {α : Type u} {β : Type v} (x : α) (y : β) (r : ) :
r).prod r) = metric.ball (x, y) r
theorem closed_ball_prod_same {α : Type u} {β : Type v} (x : α) (y : β) (r : ) :
r).prod r) = metric.closed_ball (x, y) r
theorem uniform_continuous_dist {α : Type u}  :
uniform_continuous (λ (p : α × α), dist p.fst p.snd)
theorem uniform_continuous.dist {α : Type u} {β : Type v} {f g : β → α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (b : β), dist (f b) (g b))
theorem continuous_dist {α : Type u}  :
continuous (λ (p : α × α), dist p.fst p.snd)
theorem continuous.dist {α : Type u} {β : Type v} {f g : β → α} (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), dist (f b) (g b))
theorem filter.tendsto.dist {α : Type u} {β : Type v} {f g : β → α} {x : filter β} {a b : α} (hf : (𝓝 a)) (hg : (𝓝 b)) :
filter.tendsto (λ (x : β), dist (f x) (g x)) x (𝓝 (dist a b))
theorem nhds_comap_dist {α : Type u} (a : α) :
filter.comap (λ (a' : α), dist a' a) (𝓝 0) = 𝓝 a
theorem tendsto_iff_dist_tendsto_zero {α : Type u} {β : Type v} {f : β → α} {x : filter β} {a : α} :
(𝓝 a) filter.tendsto (λ (b : β), dist (f b) a) x (𝓝 0)
theorem uniform_continuous_nndist {α : Type u}  :
uniform_continuous (λ (p : α × α), p.snd)
theorem uniform_continuous.nndist {α : Type u} {β : Type v} {f g : β → α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (b : β), nndist (f b) (g b))
theorem continuous_nndist {α : Type u}  :
continuous (λ (p : α × α), p.snd)
theorem continuous.nndist {α : Type u} {β : Type v} {f g : β → α} (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), nndist (f b) (g b))
theorem filter.tendsto.nndist {α : Type u} {β : Type v} {f g : β → α} {x : filter β} {a b : α} (hf : (𝓝 a)) (hg : (𝓝 b)) :
filter.tendsto (λ (x : β), nndist (f x) (g x)) x (𝓝 (nndist a b))
theorem metric.is_closed_ball {α : Type u} {x : α} {ε : } :
theorem metric.is_closed_sphere {α : Type u} {x : α} {ε : } :
@[simp]
theorem metric.closure_closed_ball {α : Type u} {x : α} {ε : } :
=
theorem metric.closure_ball_subset_closed_ball {α : Type u} {x : α} {ε : } :
theorem metric.frontier_ball_subset_sphere {α : Type u} {x : α} {ε : } :
theorem metric.frontier_closed_ball_subset_sphere {α : Type u} {x : α} {ε : } :
theorem metric.ball_subset_interior_closed_ball {α : Type u} {x : α} {ε : } :
ε
theorem metric.mem_closure_iff {α : Type u} {s : set α} {a : α} :
a ∀ (ε : ), ε > 0(∃ (b : α) (H : b s), dist a b < ε)

ε-characterization of the closure in pseudometric spaces

theorem metric.mem_closure_range_iff {β : Type v} {α : Type u} {e : β → α} {a : α} :
a closure (set.range e) ∀ (ε : ), ε > 0(∃ (k : β), dist a (e k) < ε)
theorem metric.mem_closure_range_iff_nat {β : Type v} {α : Type u} {e : β → α} {a : α} :
a closure (set.range e) ∀ (n : ), ∃ (k : β), dist a (e k) < 1 / (n + 1)
theorem metric.mem_of_closed' {α : Type u} {s : set α} (hs : is_closed s) {a : α} :
a s ∀ (ε : ), ε > 0(∃ (b : α) (H : b s), dist a b < ε)
@[instance]
def pseudo_metric_space_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] :
pseudo_metric_space (Π (b : β), «π» b)

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

Equations
theorem nndist_pi_def {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] (f g : Π (b : β), «π» b) :
g = finset.univ.sup (λ (b : β), nndist (f b) (g b))
theorem dist_pi_def {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] (f g : Π (b : β), «π» b) :
dist f g = (finset.univ.sup (λ (b : β), nndist (f b) (g b)))
@[simp]
theorem dist_pi_const {α : Type u} {β : Type v} [fintype β] [nonempty β] (a b : α) :
dist (λ (x : β), a) (λ (_x : β), b) = dist a b
@[simp]
theorem nndist_pi_const {α : Type u} {β : Type v} [fintype β] [nonempty β] (a b : α) :
nndist (λ (x : β), a) (λ (_x : β), b) = b
theorem dist_pi_lt_iff {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] {f g : Π (b : β), «π» b} {r : } (hr : 0 < r) :
dist f g < r ∀ (b : β), dist (f b) (g b) < r
theorem dist_pi_le_iff {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] {f g : Π (b : β), «π» b} {r : } (hr : 0 r) :
dist f g r ∀ (b : β), dist (f b) (g b) r
theorem nndist_le_pi_nndist {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] (f g : Π (b : β), «π» b) (b : β) :
nndist (f b) (g b) g
theorem dist_le_pi_dist {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] (f g : Π (b : β), «π» b) (b : β) :
dist (f b) (g b) dist f g
theorem ball_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] (x : Π (b : β), «π» b) {r : } (hr : 0 < r) :
r = {y : Π (b : β), «π» b | ∀ (b : β), y b metric.ball (x b) r}

An open ball in a product space is a product of open balls. The assumption `0 < r` is necessary for the case of the empty product.

theorem closed_ball_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] (x : Π (b : β), «π» b) {r : } (hr : 0 r) :
= {y : Π (b : β), «π» b | ∀ (b : β), y b metric.closed_ball (x b) r}

A closed ball in a product space is a product of closed balls. The assumption `0 ≤ r` is necessary for the case of the empty product.

theorem finite_cover_balls_of_compact {α : Type u} {s : set α} (hs : is_compact s) {e : } (he : 0 < e) :
∃ (t : set α) (H : t s), t.finite s ⋃ (x : α) (H : x t), e

Any compact set in a pseudometric space can be covered by finitely many balls of a given positive radius

theorem is_compact.finite_cover_balls {α : Type u} {s : set α} (hs : is_compact s) {e : } (he : 0 < e) :
∃ (t : set α) (H : t s), t.finite s ⋃ (x : α) (H : x t), e

Alias of `finite_cover_balls_of_compact`.

@[class]
structure proper_space (α : Type u)  :
Prop
• compact_ball : ∀ (x : α) (r : ),

A pseudometric space is proper if all closed balls are compact.

Instances
@[instance]
def second_countable_of_proper {α : Type u} [proper_space α] :

A proper pseudo metric space is sigma compact, and therefore second countable.

theorem tendsto_dist_right_cocompact_at_top {α : Type u} [proper_space α] (x : α) :
filter.tendsto (λ (y : α), dist y x) filter.at_top
theorem tendsto_dist_left_cocompact_at_top {α : Type u} [proper_space α] (x : α) :
theorem proper_space_of_compact_closed_ball_of_le {α : Type u} (R : ) (h : ∀ (x : α) (r : ), R r) :

If all closed balls of large enough radius are compact, then the space is proper. Especially useful when the lower bound for the radius is 0.

@[instance]
def proper_of_compact {α : Type u}  :
@[instance]
def locally_compact_of_proper {α : Type u} [proper_space α] :

A proper space is locally compact

@[instance]
def complete_of_proper {α : Type u} [proper_space α] :

A proper space is complete

@[instance]
def pi_proper_space {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space («π» b)] [h : ∀ (b : β), proper_space («π» b)] :
proper_space (Π (b : β), «π» b)

A finite product of proper spaces is proper.

theorem exists_pos_lt_subset_ball {α : Type u} [proper_space α] {x : α} {r : } {s : set α} (hr : 0 < r) (hs : is_closed s) (h : s r) :
∃ (r' : ) (H : r' r), s r'

If a nonempty ball in a proper space includes a closed set `s`, then there exists a nonempty ball with the same center and a strictly smaller radius that includes `s`.

theorem exists_lt_subset_ball {α : Type u} [proper_space α] {x : α} {r : } {s : set α} (hs : is_closed s) (h : s r) :
∃ (r' : ) (H : r' < r), s r'

If a ball in a proper space includes a closed set `s`, then there exists a ball with the same center and a strictly smaller radius that includes `s`.

theorem metric.second_countable_of_almost_dense_set {α : Type u} (H : ∀ (ε : ), ε > 0(∃ (s : set α), s.countable ∀ (x : α), ∃ (y : α) (H : y s), dist x y ε)) :

A pseudometric space is second countable if, for every `ε > 0`, there is a countable set which is `ε`-dense.

theorem lebesgue_number_lemma_of_metric {α : Type u} {s : set α} {ι : Sort u_1} {c : ι → set α} (hs : is_compact s) (hc₁ : ∀ (i : ι), is_open (c i)) (hc₂ : s ⋃ (i : ι), c i) :
∃ (δ : ) (H : δ > 0), ∀ (x : α), x s(∃ (i : ι), δ c i)
theorem lebesgue_number_lemma_of_metric_sUnion {α : Type u} {s : set α} {c : set (set α)} (hs : is_compact s) (hc₁ : ∀ (t : set α), t c) (hc₂ : s ⋃₀c) :
∃ (δ : ) (H : δ > 0), ∀ (x : α), x s(∃ (t : set α) (H : t c), δ t)
def metric.bounded {α : Type u} (s : set α) :
Prop

Boundedness of a subset of a pseudometric space. We formulate the definition to work even in the empty space.

Equations
@[simp]
theorem metric.bounded_empty {α : Type u}  :
theorem metric.bounded_iff_mem_bounded {α : Type u} {s : set α} :
∀ (x : α), x s
theorem metric.bounded.subset {α : Type u} {s t : set α} (incl : s t) :

Subsets of a bounded set are also bounded

theorem metric.bounded_closed_ball {α : Type u} {x : α} {r : } :

Closed balls are bounded

theorem metric.bounded_ball {α : Type u} {x : α} {r : } :

Open balls are bounded

theorem metric.bounded_iff_subset_ball {α : Type u} {s : set α} (c : α) :
∃ (r : ), s

Given a point, a bounded subset is included in some ball around this point

theorem metric.bounded_closure_of_bounded {α : Type u} {s : set α} (h : metric.bounded s) :
theorem metric.bounded.closure {α : Type u} {s : set α} (h : metric.bounded s) :

Alias of `bounded_closure_of_bounded`.

@[simp]
theorem metric.bounded_closure_iff {α : Type u} {s : set α} :
@[simp]
theorem metric.bounded_union {α : Type u} {s t : set α} :

The union of two bounded sets is bounded iff each of the sets is bounded

theorem metric.bounded_bUnion {α : Type u} {β : Type v} {I : set β} {s : β → set α} (H : I.finite) :
metric.bounded (⋃ (i : β) (H : i I), s i) ∀ (i : β), i Imetric.bounded (s i)

A finite union of bounded sets is bounded

theorem metric.bounded_of_compact {α : Type u} {s : set α} (h : is_compact s) :

A compact set is bounded

theorem is_compact.bounded {α : Type u} {s : set α} (h : is_compact s) :

Alias of `bounded_of_compact`.

theorem metric.bounded_of_finite {α : Type u} {s : set α} (h : s.finite) :

A finite set is bounded

theorem set.finite.bounded {α : Type u} {s : set α} (h : s.finite) :

Alias of `bounded_of_finite`.

theorem metric.bounded_singleton {α : Type u} {x : α} :

A singleton is bounded

theorem metric.bounded_range_iff {α : Type u} {β : Type v} {f : β → α} :
∃ (C : ), ∀ (x y : β), dist (f x) (f y) C

Characterization of the boundedness of the range of a function

theorem metric.bounded_of_compact_space {α : Type u} {s : set α}  :

In a compact space, all sets are bounded

theorem metric.compact_iff_closed_bounded {α : Type u} {s : set α} [t2_space α] [proper_space α] :

The Heine–Borel theorem: In a proper space, a set is compact if and only if it is closed and bounded

def metric.diam {α : Type u} (s : set α) :

The diameter of a set in a metric space. To get controllable behavior even when the diameter should be infinite, we express it in terms of the emetric.diameter

Equations
theorem metric.diam_nonneg {α : Type u} {s : set α} :
0

The diameter of a set is always nonnegative

theorem metric.diam_subsingleton {α : Type u} {s : set α} (hs : s.subsingleton) :
= 0
@[simp]
theorem metric.diam_empty {α : Type u}  :

The empty set has zero diameter

@[simp]
theorem metric.diam_singleton {α : Type u} {x : α} :

A singleton has zero diameter

theorem metric.diam_pair {α : Type u} {x y : α} :
metric.diam {x, y} = dist x y
theorem metric.diam_triple {α : Type u} {x y z : α} :
metric.diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)
theorem metric.ediam_le_of_forall_dist_le {α : Type u} {s : set α} {C : } (h : ∀ (x : α), x s∀ (y : α), y sdist x y C) :

If the distance between any two points in a set is bounded by some constant `C`, then `ennreal.of_real C` bounds the emetric diameter of this set.

theorem metric.diam_le_of_forall_dist_le {α : Type u} {s : set α} {C : } (h₀ : 0 C) (h : ∀ (x : α), x s∀ (y : α), y sdist x y C) :
C

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

theorem metric.diam_le_of_forall_dist_le_of_nonempty {α : Type u} {s : set α} (hs : s.nonempty) {C : } (h : ∀ (x : α), x s∀ (y : α), y sdist x y C) :
C

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

theorem metric.dist_le_diam_of_mem' {α : Type u} {s : set α} {x y : α} (h : ) (hx : x s) (hy : y s) :
dist x y

The distance between two points in a set is controlled by the diameter of the set.

theorem metric.bounded_iff_ediam_ne_top {α : Type u} {s : set α} :

Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.

theorem metric.bounded.ediam_ne_top {α : Type u} {s : set α} (h : metric.bounded s) :
theorem metric.dist_le_diam_of_mem {α : Type u} {s : set α} {x y : α} (h : metric.bounded s) (hx : x s) (hy : y s) :
dist x y

The distance between two points in a set is controlled by the diameter of the set.

theorem metric.diam_eq_zero_of_unbounded {α : Type u} {s : set α} (h : ¬) :
= 0

An unbounded set has zero diameter. If you would prefer to get the value ∞, use `emetric.diam`. This lemma makes it possible to avoid side conditions in some situations

theorem metric.diam_mono {α : Type u} {s t : set α} (h : s t) (ht : metric.bounded t) :

If `s ⊆ t`, then the diameter of `s` is bounded by that of `t`, provided `t` is bounded.

theorem metric.diam_union {α : Type u} {s : set α} {x y : α} {t : set α} (xs : x s) (yt : y t) :
metric.diam (s t) + dist x y +

The diameter of a union is controlled by the sum of the diameters, and the distance between any two points in each of the sets. This lemma is true without any side condition, since it is obviously true if `s ∪ t` is unbounded.

theorem metric.diam_union' {α : Type u} {s t : set α} (h : (s t).nonempty) :

If two sets intersect, the diameter of the union is bounded by the sum of the diameters.

theorem metric.diam_closed_ball {α : Type u} {x : α} {r : } (h : 0 r) :
2 * r

The diameter of a closed ball of radius `r` is at most `2 r`.

theorem metric.diam_ball {α : Type u} {x : α} {r : } (h : 0 r) :

The diameter of a ball of radius `r` is at most `2 r`.

Under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite.

@[class]
structure metric_space (α : Type u) :
Type u
• to_pseudo_metric_space :
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y

We now define `metric_space`, extending `pseudo_metric_space`.

Instances
theorem eq_of_dist_eq_zero {γ : Type w} [metric_space γ] {x y : γ} :
dist x y = 0x = y
@[simp]
theorem dist_eq_zero {γ : Type w} [metric_space γ] {x y : γ} :
dist x y = 0 x = y
@[simp]
theorem zero_eq_dist {γ : Type w} [metric_space γ] {x y : γ} :
0 = dist x y x = y
@[simp]
theorem dist_le_zero {γ : Type w} [metric_space γ] {x y : γ} :
dist x y 0 x = y
@[simp]
theorem dist_pos {γ : Type w} [metric_space γ] {x y : γ} :
0 < dist x y x y
theorem eq_of_forall_dist_le {γ : Type w} [metric_space γ] {x y : γ} (h : ∀ (ε : ), ε > 0dist x y ε) :
x = y
theorem eq_of_nndist_eq_zero {γ : Type w} [metric_space γ] {x y : γ} :
y = 0x = y

Deduce the equality of points with the vanishing of the nonnegative distance

@[simp]
theorem nndist_eq_zero {γ : Type w} [metric_space γ] {x y : γ} :
y = 0 x = y

Characterize the equality of points with the vanishing of the nonnegative distance

@[simp]
theorem zero_eq_nndist {γ : Type w} [metric_space γ] {x y : γ} :
0 = y x = y
@[simp]
theorem metric.closed_ball_zero {γ : Type w} [metric_space γ] {x : γ} :
= {x}
theorem metric.uniform_embedding_iff' {β : Type v} {γ : Type w} [metric_space γ] [metric_space β] {f : γ → β} :
(∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {a b : γ}, dist a b < δdist (f a) (f b) < ε)) ∀ (δ : ), δ > 0(∃ (ε : ) (H : ε > 0), ∀ {a b : γ}, dist (f a) (f b) < εdist a b < δ)

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

@[instance]
def metric.of_t2_pseudo_metric_space {α : Type u_1} (h : separated_space α) :

If a `pseudo_metric_space` is separated, then it is a `metric_space`.

Equations
@[instance]

A metric space induces an emetric space

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

Build a new metric space from an old one where the bundled uniform structure is provably (but typically non-definitionaly) equal to some given uniform structure. See Note [forgetful inheritance].

Equations
def emetric_space.to_metric_space_of_dist {α : Type u} [e : emetric_space α] (dist : α → α → ) (edist_ne_top : ∀ (x y : α), y ) (h : ∀ (x y : α), dist x y = (edist x y).to_real) :

One gets a metric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the metric space and the emetric space. In this definition, the distance is given separately, to be able to prescribe some expression which is not defeq to the push-forward of the edistance to reals.

Equations
def emetric_space.to_metric_space {α : Type u} [e : emetric_space α] (h : ∀ (x y : α), y ) :

One gets a metric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the metric space and the emetric space.

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

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

Equations
@[instance]
def subtype.metric_space {α : Type u_1} {p : α → Prop} [t : metric_space α] :
Equations
theorem subtype.dist_eq {α : Type u} {p : α → Prop} (x y : subtype p) :
dist x y = y
@[instance]

Instantiate the reals as a metric space.

Equations
@[instance]
Equations
@[instance]
def prod.metric_space_max {β : Type v} {γ : Type w} [metric_space γ] [metric_space β] :
Equations
@[instance]
def metric_space_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space («π» b)] :
metric_space (Π (b : β), «π» b)

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

Equations
theorem exists_subset_Union_ball_radius_lt {γ : Type w} [metric_space γ] {ι : Type u_1} {c : ι → γ} [proper_space γ] {s : set γ} {r : ι → } (hs : is_closed s) (uf : ∀ (x : γ), x s{i : ι | x metric.ball (c i) (r i)}.finite) (us : s ⋃ (i : ι), metric.ball (c i) (r i)) :
∃ (r' : ι → ), (s ⋃ (i : ι), metric.ball (c i) (r' i)) ∀ (i : ι), r' i < r i

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a closed subset of a proper metric space by open balls can be shrunk to a new cover by open balls so that each of the new balls has strictly smaller radius than the old one. This version assumes that `λ x, ball (c i) (r i)` is a locally finite covering and provides a covering indexed by the same type.

theorem exists_Union_ball_eq_radius_lt {γ : Type w} [metric_space γ] {ι : Type u_1} {c : ι → γ} [proper_space γ] {r : ι → } (uf : ∀ (x : γ), {i : ι | x metric.ball (c i) (r i)}.finite) (uU : (⋃ (i : ι), metric.ball (c i) (r i)) = set.univ) :
∃ (r' : ι → ), (⋃ (i : ι), metric.ball (c i) (r' i)) = set.univ ∀ (i : ι), r' i < r i

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a proper metric space by open balls can be shrunk to a new cover by open balls so that each of the new balls has strictly smaller radius than the old one.

theorem exists_subset_Union_ball_radius_pos_lt {γ : Type w} [metric_space γ] {ι : Type u_1} {c : ι → γ} [proper_space γ] {s : set γ} {r : ι → } (hr : ∀ (i : ι), 0 < r i) (hs : is_closed s) (uf : ∀ (x : γ), x s{i : ι | x metric.ball (c i) (r i)}.finite) (us : s ⋃ (i : ι), metric.ball (c i) (r i)) :
∃ (r' : ι → ), (s ⋃ (i : ι), metric.ball (c i) (r' i)) ∀ (i : ι), r' i (r i)

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a closed subset of a proper metric space by nonempty open balls can be shrunk to a new cover by nonempty open balls so that each of the new balls has strictly smaller radius than the old one.

theorem exists_Union_ball_eq_radius_pos_lt {γ : Type w} [metric_space γ] {ι : Type u_1} {c : ι → γ} [proper_space γ] {r : ι → } (hr : ∀ (i : ι), 0 < r i) (uf : ∀ (x : γ), {i : ι | x metric.ball (c i) (r i)}.finite) (uU : (⋃ (i : ι), metric.ball (c i) (r i)) = set.univ) :
∃ (r' : ι → ), (⋃ (i : ι), metric.ball (c i) (r' i)) = set.univ ∀ (i : ι), r' i (r i)

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a proper metric space by nonempty open balls can be shrunk to a new cover by nonempty open balls so that each of the new balls has strictly smaller radius than the old one.

theorem exists_locally_finite_subset_Union_ball_radius_lt {γ : Type w} [metric_space γ] [proper_space γ] {s : set γ} (hs : is_closed s) {R : γ → } (hR : ∀ (x : γ), x s0 < R x) :
∃ (ι : Type w) (c : ι → γ) (r r' : ι → ), (∀ (i : ι), c i s 0 < r i r i < r' i r' i < R (c i)) locally_finite (λ (i : ι), metric.ball (c i) (r' i)) s ⋃ (i : ι), metric.ball (c i) (r i)

Let `R : γ → ℝ` be a (possibly discontinuous) function on a proper metric space. Let `s` be a closed set in `α` such that `R` is positive on `s`. Then there exists a collection of pairs of balls `metric.ball (c i) (r i)`, `metric.ball (c i) (r' i)` such that

• all centers belong to `s`;
• for all `i` we have `0 < r i < r' i < R (c i)`;
• the family of balls `metric.ball (c i) (r' i)` is locally finite;
• the balls `metric.ball (c i) (r i)` cover `s`.

This is a simple corollary of `refinement_of_locally_compact_sigma_compact_of_nhds_basis_set` and `exists_subset_Union_ball_radius_pos_lt`.

theorem exists_locally_finite_Union_eq_ball_radius_lt {γ : Type w} [metric_space γ] [proper_space γ] {R : γ → } (hR : ∀ (x : γ), 0 < R x) :
∃ (ι : Type w) (c : ι → γ) (r r' : ι → ), (∀ (i : ι), 0 < r i r i < r' i r' i < R (c i)) locally_finite (λ (i : ι), metric.ball (c i) (r' i)) (⋃ (i : ι), metric.ball (c i) (r i)) = set.univ

Let `R : γ → ℝ` be a (possibly discontinuous) positive function on a proper metric space. Then there exists a collection of pairs of balls `metric.ball (c i) (r i)`, `metric.ball (c i) (r' i)` such that

• for all `i` we have `0 < r i < r' i < R (c i)`;
• the family of balls `metric.ball (c i) (r' i)` is locally finite;
• the balls `metric.ball (c i) (r i)` cover the whole space.

This is a simple corollary of `refinement_of_locally_compact_sigma_compact_of_nhds_basis` and `exists_Union_ball_eq_radius_pos_lt` or `exists_locally_finite_subset_Union_ball_radius_lt`.

theorem metric.second_countable_of_countable_discretization {α : Type u} [metric_space α] (H : ∀ (ε : ), ε > 0(∃ (β : Type u_1) [_inst_4 : (F : α → β), ∀ (x y : α), F x = F ydist x y ε)) :

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

def pseudo_metric.dist_setoid (α : Type u)  :

The canonical equivalence relation on a pseudometric space.

Equations
def pseudo_metric_quot (α : Type u)  :
Type u

The canonical quotient of a pseudometric space, identifying points at distance `0`.

Equations
@[instance]
def has_dist_metric_quot {α : Type u}  :
Equations
theorem pseudo_metric_quot_dist_eq {α : Type u} (p q : α) :
q = dist p q
@[instance]
def metric_space_quot {α : Type u}  :
Equations