mathlib documentation

topology.metric_space.basic

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

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

Equations
@[class]
structure has_dist  :
Type u_1Type 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 metric_space  :
Type uType 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_has_edist {α : Type u} [metric_space α] :

Equations
@[simp]
theorem dist_self {α : Type u} [metric_space α] (x : α) :
dist x x = 0

theorem eq_of_dist_eq_zero {α : Type u} [metric_space α] {x y : α} :
dist x y = 0x = y

theorem dist_comm {α : Type u} [metric_space α] (x y : α) :
dist x y = dist y x

theorem edist_dist {α : Type u} [metric_space α] (x y : α) :

@[simp]
theorem dist_eq_zero {α : Type u} [metric_space α] {x y : α} :
dist x y = 0 x = y

@[simp]
theorem zero_eq_dist {α : Type u} [metric_space α] {x y : α} :
0 = dist x y x = y

theorem dist_triangle {α : Type u} [metric_space α] (x y z : α) :
dist x z dist x y + dist y z

theorem dist_triangle_left {α : Type u} [metric_space α] (x y z : α) :
dist x y dist z x + dist z y

theorem dist_triangle_right {α : Type u} [metric_space α] (x y z : α) :
dist x y dist x z + dist y z

theorem dist_triangle4 {α : Type u} [metric_space α] (x y z w : α) :
dist x w dist x y + dist y z + dist z w

theorem dist_triangle4_left {α : Type u} [metric_space α] (x₁ y₁ x₂ y₂ : α) :
dist x₂ y₂ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)

theorem dist_triangle4_right {α : Type u} [metric_space α] (x₁ y₁ x₂ y₂ : α) :
dist x₁ y₁ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂

theorem dist_le_Ico_sum_dist {α : Type u} [metric_space α] (f : → α) {m n : } :
m ndist (f m) (f n) ∑ (i : ) in finset.Ico m 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} [metric_space α] (f : → α) (n : ) :
dist (f 0) (f n) ∑ (i : ) in finset.range n, 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} [metric_space α] {f : → α} {m n : } (hmn : m n) {d : } :
(∀ {k : }, m kk < ndist (f k) (f (k + 1)) d k)dist (f m) (f n) ∑ (i : ) in finset.Ico m 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} [metric_space α] {f : → α} (n : ) {d : } :
(∀ {k : }, k < ndist (f k) (f (k + 1)) d k)dist (f 0) (f n) ∑ (i : ) in finset.range n, d i

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

theorem swap_dist {α : Type u} [metric_space α] :

theorem abs_dist_sub_le {α : Type u} [metric_space α] (x y z : α) :
abs (dist x z - dist y z) dist x y

theorem dist_nonneg {α : Type u} [metric_space α] {x y : α} :
0 dist x y

@[simp]
theorem dist_le_zero {α : Type u} [metric_space α] {x y : α} :
dist x y 0 x = y

@[simp]
theorem dist_pos {α : Type u} [metric_space α] {x y : α} :
0 < dist x y x y

@[simp]
theorem abs_dist {α : Type u} [metric_space α] {a b : α} :
abs (dist a b) = dist a b

theorem eq_of_forall_dist_le {α : Type u} [metric_space α] {x y : α} :
(∀ (ε : ), ε > 0dist x y ε)x = y

def nndist {α : Type u} [metric_space α] :
α → α → ℝ≥0

Distance as a nonnegative real number.

Equations
theorem nndist_edist {α : Type u} [metric_space α] (x y : α) :

Express nndist in terms of edist

theorem edist_nndist {α : Type u} [metric_space α] (x y : α) :
edist x y = (nndist x y)

Express edist in terms of nndist

theorem edist_ne_top {α : Type u} [metric_space α] (x y : α) :

In a metric space, the extended distance is always finite

theorem edist_lt_top {α : Type u_1} [metric_space α] (x y : α) :
edist x y <

In a metric space, the extended distance is always finite

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

nndist x x vanishes

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

Express dist in terms of nndist

theorem nndist_dist {α : Type u} [metric_space α] (x y : α) :

Express nndist in terms of dist

theorem eq_of_nndist_eq_zero {α : Type u} [metric_space α] {x y : α} :
nndist x y = 0x = y

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

theorem nndist_comm {α : Type u} [metric_space α] (x y : α) :
nndist x y = nndist y x

@[simp]
theorem nndist_eq_zero {α : Type u} [metric_space α] {x y : α} :
nndist x y = 0 x = y

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

@[simp]
theorem zero_eq_nndist {α : Type u} [metric_space α] {x y : α} :
0 = nndist x y x = y

theorem nndist_triangle {α : Type u} [metric_space α] (x y z : α) :
nndist x z nndist x y + nndist y z

Triangle inequality for the nonnegative distance

theorem nndist_triangle_left {α : Type u} [metric_space α] (x y z : α) :
nndist x y nndist z x + nndist z y

theorem nndist_triangle_right {α : Type u} [metric_space α] (x y z : α) :
nndist x y nndist x z + nndist y z

theorem dist_edist {α : Type u} [metric_space α] (x y : α) :
dist x y = (edist x y).to_real

Express dist in terms of edist

def metric.ball {α : Type u} [metric_space α] :
α → set α

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

Equations
@[simp]
theorem metric.mem_ball {α : Type u} [metric_space α] {x y : α} {ε : } :
y metric.ball x ε dist y x < ε

theorem metric.mem_ball' {α : Type u} [metric_space α] {x y : α} {ε : } :
y metric.ball x ε dist x y < ε

@[simp]
theorem metric.nonempty_ball {α : Type u} [metric_space α] {x : α} {ε : } :
0 < ε(metric.ball x ε).nonempty

theorem metric.ball_eq_ball {α : Type u} [metric_space α] (ε : ) (x : α) :
uniform_space.ball x {p : α × α | dist p.snd p.fst < ε} = metric.ball x ε

theorem metric.ball_eq_ball' {α : Type u} [metric_space α] (ε : ) (x : α) :
uniform_space.ball x {p : α × α | dist p.fst p.snd < ε} = metric.ball x ε

def metric.closed_ball {α : Type u} [metric_space α] :
α → set α

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

Equations
def metric.sphere {α : Type u} [metric_space α] :
α → set α

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

Equations
@[simp]
theorem metric.mem_closed_ball {α : Type u} [metric_space α] {x y : α} {ε : } :

theorem metric.nonempty_closed_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.ball_subset_closed_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.sphere_subset_closed_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.sphere_disjoint_ball {α : Type u} [metric_space α] {x : α} {ε : } :

@[simp]
theorem metric.ball_union_sphere {α : Type u} [metric_space α] {x : α} {ε : } :

@[simp]
theorem metric.sphere_union_ball {α : Type u} [metric_space α] {x : α} {ε : } :

@[simp]
theorem metric.closed_ball_diff_sphere {α : Type u} [metric_space α] {x : α} {ε : } :

@[simp]
theorem metric.closed_ball_diff_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.pos_of_mem_ball {α : Type u} [metric_space α] {x y : α} {ε : } :
y metric.ball x ε0 < ε

theorem metric.mem_ball_self {α : Type u} [metric_space α] {x : α} {ε : } :
0 < εx metric.ball x ε

theorem metric.mem_closed_ball_self {α : Type u} [metric_space α] {x : α} {ε : } :
0 εx metric.closed_ball x ε

theorem metric.mem_ball_comm {α : Type u} [metric_space α] {x y : α} {ε : } :

theorem metric.ball_subset_ball {α : Type u} [metric_space α] {x : α} {ε₁ ε₂ : } :
ε₁ ε₂metric.ball x ε₁ metric.ball x ε₂

theorem metric.closed_ball_subset_closed_ball {α : Type u} [metric_space α] {ε₁ ε₂ : } {x : α} :
ε₁ ε₂metric.closed_ball x ε₁ metric.closed_ball x ε₂

theorem metric.ball_disjoint {α : Type u} [metric_space α] {x y : α} {ε₁ ε₂ : } :
ε₁ + ε₂ dist x ymetric.ball x ε₁ metric.ball y ε₂ =

theorem metric.ball_disjoint_same {α : Type u} [metric_space α] {x y : α} {ε : } :
ε dist x y / 2metric.ball x ε metric.ball y ε =

theorem metric.ball_subset {α : Type u} [metric_space α] {x y : α} {ε₁ ε₂ : } :
dist x y ε₂ - ε₁metric.ball x ε₁ metric.ball y ε₂

theorem metric.ball_half_subset {α : Type u} [metric_space α] {x : α} {ε : } (y : α) :
y metric.ball x / 2)metric.ball y / 2) metric.ball x ε

theorem metric.exists_ball_subset_ball {α : Type u} [metric_space α] {x y : α} {ε : } :
y metric.ball x ε(∃ (ε' : ) (H : ε' > 0), metric.ball y ε' metric.ball x ε)

@[simp]
theorem metric.ball_eq_empty_iff_nonpos {α : Type u} [metric_space α] {x : α} {ε : } :
metric.ball x ε = ε 0

@[simp]
theorem metric.closed_ball_eq_empty_iff_neg {α : Type u} [metric_space α] {x : α} {ε : } :

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

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

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

theorem metric.mk_uniformity_basis {α : Type u} [metric_space α] {β : Type u_1} {p : β → Prop} {f : β → } :
(∀ (i : β), p i0 < f i)(∀ ⦃ε : ⦄, 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} [metric_space α] :
(𝓤 α).has_basis (λ (_x : ), true) (λ (n : ), {p : α × α | dist p.fst p.snd < 1 / (n + 1)})

theorem metric.uniformity_basis_dist_inv_nat_pos {α : Type u} [metric_space α] :
(𝓤 α).has_basis (λ (n : ), 0 < n) (λ (n : ), {p : α × α | dist p.fst p.snd < 1 / n})

theorem metric.mk_uniformity_basis_le {α : Type u} [metric_space α] {β : Type u_1} {p : β → Prop} {f : β → } :
(∀ (x : β), p x0 < f x)(∀ (ε : ), 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} [metric_space α] :
(𝓤 α).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.mem_uniformity_dist {α : Type u} [metric_space α] {s : set × α)} :
s 𝓤 α ∃ (ε : ) (H : ε > 0), ∀ {a b : α}, dist a b < ε(a, b) s

theorem metric.dist_mem_uniformity {α : Type u} [metric_space α] {ε : } :
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} [metric_space α] [metric_space β] {f : α → β} :
uniform_continuous f ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {a b : α}, dist a b < δdist (f a) (f b) < ε)

theorem metric.uniform_continuous_on_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {s : set α} :
uniform_continuous_on f s ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (x y : α), x sy sdist x y < δdist (f x) (f y) < ε)

theorem metric.uniform_embedding_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :
uniform_embedding f function.injective f uniform_continuous f ∀ (δ : ), δ > 0(∃ (ε : ) (H : ε > 0), ∀ {a b : α}, dist (f a) (f b) < εdist a b < δ)

theorem metric.uniform_embedding_iff' {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :
uniform_embedding 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.

theorem metric.totally_bounded_iff {α : Type u} [metric_space α] {s : set α} :
totally_bounded s ∀ (ε : ), ε > 0(∃ (t : set α), t.finite s ⋃ (y : α) (H : y t), metric.ball y ε)

theorem metric.totally_bounded_of_finite_discretization {α : Type u} [metric_space α] {s : set α} :
(∀ (ε : ), ε > 0(∃ (β : Type u) [_inst_2 : fintype β] (F : s → β), ∀ (x y : s), F x = F ydist x y < ε))totally_bounded s

A metric 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} [metric_space α] {s : set α} (hs : totally_bounded s) (ε : ) :
ε > 0(∃ (t : set α) (H : t s), t.finite s ⋃ (y : α) (H : y t), metric.ball y ε)

theorem metric.tendsto_locally_uniformly_on_iff {α : Type u} {β : Type v} [metric_space α] {ι : Type u_1} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :
tendsto_locally_uniformly_on F f p 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} [metric_space α] {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :
tendsto_uniformly_on F f 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} [metric_space α] {ι : Type u_1} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} :
tendsto_locally_uniformly F f p ∀ (ε : ), ε > 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} [metric_space α] {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} :
tendsto_uniformly F f p ∀ (ε : ), ε > 0(∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε)

Expressing uniform convergence using dist.

theorem metric.cauchy_iff {α : Type u} [metric_space α] {f : filter α} :
cauchy f f.ne_bot ∀ (ε : ), ε > 0(∃ (t : set α) (H : t f), ∀ (x y : α), x ty tdist x y < ε)

theorem metric.nhds_basis_ball {α : Type u} [metric_space α] {x : α} :
(𝓝 x).has_basis (λ (ε : ), 0 < ε) (metric.ball x)

theorem metric.mem_nhds_iff {α : Type u} [metric_space α] {x : α} {s : set α} :
s 𝓝 x ∃ (ε : ) (H : ε > 0), metric.ball x ε s

theorem metric.nhds_basis_closed_ball {α : Type u} [metric_space α] {x : α} :
(𝓝 x).has_basis (λ (ε : ), 0 < ε) (metric.closed_ball x)

theorem metric.nhds_basis_ball_inv_nat_succ {α : Type u} [metric_space α] {x : α} :
(𝓝 x).has_basis (λ (_x : ), true) (λ (n : ), metric.ball x (1 / (n + 1)))

theorem metric.nhds_basis_ball_inv_nat_pos {α : Type u} [metric_space α] {x : α} :
(𝓝 x).has_basis (λ (n : ), 0 < n) (λ (n : ), metric.ball x (1 / n))

theorem metric.is_open_iff {α : Type u} [metric_space α] {s : set α} :
is_open s ∀ (x : α), x s(∃ (ε : ) (H : ε > 0), metric.ball x ε s)

theorem metric.is_open_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.ball_mem_nhds {α : Type u} [metric_space α] (x : α) {ε : } :
0 < εmetric.ball x ε 𝓝 x

theorem metric.closed_ball_mem_nhds {α : Type u} [metric_space α] (x : α) {ε : } :
0 < εmetric.closed_ball x ε 𝓝 x

theorem metric.nhds_within_basis_ball {α : Type u} [metric_space α] {x : α} {s : set α} :
(𝓝[s] x).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), metric.ball x ε s)

theorem metric.mem_nhds_within_iff {α : Type u} [metric_space α] {x : α} {s t : set α} :
s 𝓝[t] x ∃ (ε : ) (H : ε > 0), metric.ball x ε t s

theorem metric.tendsto_nhds_within_nhds_within {α : Type u} {β : Type v} [metric_space α] {s : set α} [metric_space β] {t : set β} {f : α → β} {a : α} {b : β} :
filter.tendsto f (𝓝[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} [metric_space α] {s : set α} [metric_space β] {f : α → β} {a : α} {b : β} :
filter.tendsto f (𝓝[s] a) (𝓝 b) ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {x : α}, x sdist x a < δdist (f x) b < ε)

theorem metric.tendsto_nhds_nhds {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {a : α} {b : β} :
filter.tendsto f (𝓝 a) (𝓝 b) ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {x : α}, dist x a < δdist (f x) b < ε)

theorem metric.continuous_at_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {a : α} :
continuous_at f a ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {x : α}, dist x a < δdist (f x) (f a) < ε)

theorem metric.continuous_within_at_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {a : α} {s : set α} :
continuous_within_at f s a ∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ {x : α}, x sdist x a < δdist (f x) (f a) < ε)

theorem metric.continuous_on_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {s : set α} :
continuous_on f s ∀ (b : α), b s∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (a : α), a sdist a b < δdist (f a) (f b) < ε)

theorem metric.continuous_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :
continuous f ∀ (b : α) (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (a : α), dist a b < δdist (f a) (f b) < ε)

theorem metric.tendsto_nhds {α : Type u} {β : Type v} [metric_space α] {f : filter β} {u : β → α} {a : α} :
filter.tendsto u f (𝓝 a) ∀ (ε : ), ε > 0(∀ᶠ (x : β) in f, dist (u x) a < ε)

theorem metric.continuous_at_iff' {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f : β → α} {b : β} :
continuous_at f b ∀ (ε : ), ε > 0(∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε)

theorem metric.continuous_within_at_iff' {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f : β → α} {b : β} {s : set β} :
continuous_within_at f s b ∀ (ε : ), ε > 0(∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε)

theorem metric.continuous_on_iff' {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f : β → α} {s : set β} :
continuous_on f s ∀ (b : β), b s∀ (ε : ), ε > 0(∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε)

theorem metric.continuous_iff' {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f : β → α} :
continuous f ∀ (a : β) (ε : ), ε > 0(∀ᶠ (x : β) in 𝓝 a, dist (f x) (f a) < ε)

theorem metric.tendsto_at_top {α : Type u} {β : Type v} [metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} {a : α} :
filter.tendsto u filter.at_top (𝓝 a) ∀ (ε : ), ε > 0(∃ (N : β), ∀ (n : β), n Ndist (u n) a < ε)

@[instance]

theorem metric.uniformity_basis_edist {α : Type u} [metric_space α] :
(𝓤 α).has_basis (λ (ε : ennreal), 0 < ε) (λ (ε : ennreal), {p : α × α | edist p.fst p.snd < ε})

Expressing the uniformity in terms of edist

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

theorem metric.emetric_ball {α : Type u} [metric_space α] {x : α} {ε : } :

Balls defined using the distance or the edistance coincide

theorem metric.emetric_ball_nnreal {α : Type u} [metric_space α] {x : α} {ε : ℝ≥0} :

Balls defined using the distance or the edistance coincide

theorem metric.emetric_closed_ball {α : Type u} [metric_space α] {x : α} {ε : } :

Closed balls defined using the distance or the edistance coincide

Closed balls defined using the distance or the edistance coincide

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

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 : α → α → ) :
(∀ (x y : α), edist x y )(∀ (x y : α), dist x y = (edist x y).to_real)metric_space α

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 α] :
(∀ (x y : α), edist x y )metric_space α

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
theorem metric.complete_of_convergent_controlled_sequences {α : Type u} [metric_space α] (B : ) :
(∀ (n : ), 0 < B n)(∀ (u : → α), (∀ (N n m : ), N nN mdist (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 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} [metric_space α] :
(∀ (u : → α), cauchy_seq u(∃ (a : α), filter.tendsto u filter.at_top (𝓝 a)))complete_space α

@[instance]

Instantiate the reals as a metric 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 closed_ball_Icc {x r : } :
metric.closed_ball x r = set.Icc (x - r) (x + r)

theorem squeeze_zero' {α : Type u_1} {f g : α → } {t₀ : filter α} :
(∀ᶠ (t : α) in t₀, 0 f t)(∀ᶠ (t : α) in t₀, f t g t)filter.tendsto g t₀ (𝓝 0)filter.tendsto f 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 α} :
(∀ (t : α), 0 f t)(∀ (t : α), f t g t)filter.tendsto g t₀ (𝓝 0)filter.tendsto f 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} [metric_space α] :
𝓤 α = filter.comap (λ (p : α × α), dist p.fst p.snd) (𝓝 0)

theorem cauchy_seq_iff_tendsto_dist_at_top_0 {α : Type u} {β : Type v} [metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :
cauchy_seq u filter.tendsto (λ (n : β × β), dist (u n.fst) (u n.snd)) filter.at_top (𝓝 0)

theorem tendsto_uniformity_iff_dist_tendsto_zero {α : Type u} [metric_space α] {ι : Type u_1} {f : ι → α × α} {p : filter ι} :
filter.tendsto f p (𝓤 α) filter.tendsto (λ (x : ι), dist (f x).fst (f x).snd) p (𝓝 0)

theorem filter.tendsto.congr_dist {α : Type u} [metric_space α] {ι : Type u_1} {f₁ f₂ : ι → α} {p : filter ι} {a : α} :
filter.tendsto f₁ p (𝓝 a)filter.tendsto (λ (x : ι), dist (f₁ x) (f₂ x)) p (𝓝 0)filter.tendsto f₂ p (𝓝 a)

theorem tendsto_of_tendsto_of_dist {α : Type u} [metric_space α] {ι : Type u_1} {f₁ f₂ : ι → α} {p : filter ι} {a : α} :
filter.tendsto f₁ p (𝓝 a)filter.tendsto (λ (x : ι), dist (f₁ x) (f₂ x)) p (𝓝 0)filter.tendsto f₂ p (𝓝 a)

Alias of filter.tendsto.congr_dist.

theorem tendsto_iff_of_dist {α : Type u} [metric_space α] {ι : Type u_1} {f₁ f₂ : ι → α} {p : filter ι} {a : α} :
filter.tendsto (λ (x : ι), dist (f₁ x) (f₂ x)) p (𝓝 0)(filter.tendsto f₁ p (𝓝 a) filter.tendsto f₂ p (𝓝 a))

@[nolint]
theorem metric.cauchy_seq_iff {α : Type u} {β : Type v} [metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :
cauchy_seq u ∀ (ε : ), ε > 0(∃ (N : β), ∀ (m n : β), m Nn Ndist (u m) (u n) < ε)

In a metric 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} [metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :
cauchy_seq u ∀ (ε : ), ε > 0(∃ (N : β), ∀ (n : β), n Ndist (u n) (u N) < ε)

A variation around the metric characterization of Cauchy sequences

theorem cauchy_seq_of_le_tendsto_0 {α : Type u} {β : Type v} [metric_space α] [nonempty β] [semilattice_sup β] {s : β → α} (b : β → ) :
(∀ (n m N : β), N nN mdist (s n) (s m) b N)filter.tendsto b filter.at_top (𝓝 0)cauchy_seq s

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} [metric_space α] {u : → α} :
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} [metric_space α] {s : → α} :
cauchy_seq s ∃ (b : ), (∀ (n : ), 0 b n) (∀ (n m N : ), N nN mdist (s n) (s m) b N) filter.tendsto b filter.at_top (𝓝 0)

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

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

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} [metric_space α] {p : α → Prop} (x y : subtype p) :
dist x y = dist x y

@[instance]

Equations
theorem nnreal.dist_eq (a b : ℝ≥0) :
dist a b = abs (a - b)

theorem nnreal.nndist_eq (a b : ℝ≥0) :
nndist a b = max (a - b) (b - a)

@[instance]
def prod.metric_space_max {α : Type u} {β : Type v} [metric_space α] [metric_space β] :

Equations
theorem prod.dist_eq {α : Type u} {β : Type v} [metric_space α] [metric_space β] {x y : α × β} :
dist x y = max (dist x.fst y.fst) (dist x.snd y.snd)

theorem uniform_continuous_dist {α : Type u} [metric_space α] :
uniform_continuous (λ (p : α × α), dist p.fst p.snd)

theorem uniform_continuous.dist {α : Type u} {β : Type v} [metric_space α] [uniform_space β] {f g : β → α} :
uniform_continuous funiform_continuous guniform_continuous (λ (b : β), dist (f b) (g b))

theorem continuous_dist {α : Type u} [metric_space α] :
continuous (λ (p : α × α), dist p.fst p.snd)

theorem continuous.dist {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f g : β → α} :
continuous fcontinuous gcontinuous (λ (b : β), dist (f b) (g b))

theorem filter.tendsto.dist {α : Type u} {β : Type v} [metric_space α] {f g : β → α} {x : filter β} {a b : α} :
filter.tendsto f x (𝓝 a)filter.tendsto g x (𝓝 b)filter.tendsto (λ (x : β), dist (f x) (g x)) x (𝓝 (dist a b))

theorem nhds_comap_dist {α : Type u} [metric_space α] (a : α) :
filter.comap (λ (a' : α), dist a' a) (𝓝 0) = 𝓝 a

theorem tendsto_iff_dist_tendsto_zero {α : Type u} {β : Type v} [metric_space α] {f : β → α} {x : filter β} {a : α} :
filter.tendsto f x (𝓝 a) filter.tendsto (λ (b : β), dist (f b) a) x (𝓝 0)

theorem uniform_continuous_nndist {α : Type u} [metric_space α] :
uniform_continuous (λ (p : α × α), nndist p.fst p.snd)

theorem uniform_continuous.nndist {α : Type u} {β : Type v} [metric_space α] [uniform_space β] {f g : β → α} :
uniform_continuous funiform_continuous guniform_continuous (λ (b : β), nndist (f b) (g b))

theorem continuous_nndist {α : Type u} [metric_space α] :
continuous (λ (p : α × α), nndist p.fst p.snd)

theorem continuous.nndist {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f g : β → α} :
continuous fcontinuous gcontinuous (λ (b : β), nndist (f b) (g b))

theorem filter.tendsto.nndist {α : Type u} {β : Type v} [metric_space α] {f g : β → α} {x : filter β} {a b : α} :
filter.tendsto f x (𝓝 a)filter.tendsto g x (𝓝 b)filter.tendsto (λ (x : β), nndist (f x) (g x)) x (𝓝 (nndist a b))

theorem metric.is_closed_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.is_closed_sphere {α : Type u} [metric_space α] {x : α} {ε : } :

@[simp]
theorem metric.closure_closed_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.closure_ball_subset_closed_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.frontier_ball_subset_sphere {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.ball_subset_interior_closed_ball {α : Type u} [metric_space α] {x : α} {ε : } :

theorem metric.mem_closure_iff {α : Type u} [metric_space α] {s : set α} {a : α} :
a closure s ∀ (ε : ), ε > 0(∃ (b : α) (H : b s), dist a b < ε)

ε-characterization of the closure in metric spaces

theorem metric.mem_closure_range_iff {β : Type v} {α : Type u} [metric_space α] {e : β → α} {a : α} :
a closure (set.range e) ∀ (ε : ), ε > 0(∃ (k : β), dist a (e k) < ε)

theorem metric.mem_closure_range_iff_nat {β : Type v} {α : Type u} [metric_space α] {e : β → α} {a : α} :
a closure (set.range e) ∀ (n : ), ∃ (k : β), dist a (e k) < 1 / (n + 1)

theorem metric.mem_of_closed' {α : Type u} [metric_space α] {s : set α} (hs : is_closed s) {a : α} :
a s ∀ (ε : ), ε > 0(∃ (b : α) (H : b s), dist a b < ε)

@[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 dist_pi_def {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space («π» b)] (f g : Π (b : β), «π» b) :
dist f g = (finset.univ.sup (λ (b : β), nndist (f b) (g b)))

theorem dist_pi_lt_iff {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space («π» b)] {f g : Π (b : β), «π» b} {r : } :
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 : β), metric_space («π» b)] {f g : Π (b : β), «π» b} {r : } :
0 r(dist f g r ∀ (b : β), dist (f b) (g b) r)

theorem ball_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space («π» b)] (x : Π (b : β), «π» b) {r : } :
0 < rmetric.ball x 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 : β), metric_space («π» b)] (x : Π (b : β), «π» b) {r : } :
0 rmetric.closed_ball x 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} [metric_space α] {s : set α} (hs : is_compact s) {e : } :
0 < e(∃ (t : set α) (H : t s), t.finite s ⋃ (x : α) (H : x t), metric.ball x e)

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

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

Alias of finite_cover_balls_of_compact.

@[class]
structure proper_space (α : Type u) [metric_space α] :
Prop

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

Instances
theorem tendsto_dist_right_cocompact_at_top {α : Type u} [metric_space α] [proper_space α] (x : α) :

theorem proper_space_of_compact_closed_ball_of_le {α : Type u} [metric_space α] (R : ) :
(∀ (x : α) (r : ), R ris_compact (metric.closed_ball x r))proper_space α

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} [metric_space α] [compact_space α] :

@[instance]

A proper space is locally compact

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

A proper space is complete

@[instance]

A proper metric space is separable, and therefore second countable. Indeed, any ball is compact, and therefore admits a countable dense subset. Taking a countable union over the balls centered at a fixed point and with integer radius, one obtains a countable set which is dense in the whole space.

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

A finite product of proper spaces is proper.

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

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

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

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

theorem lebesgue_number_lemma_of_metric {α : Type u} [metric_space α] {s : set α} {ι : Sort u_1} {c : ι → set α} :
is_compact s(∀ (i : ι), is_open (c i))(s ⋃ (i : ι), c i)(∃ (δ : ) (H : δ > 0), ∀ (x : α), x s(∃ (i : ι), metric.ball x δ c i))

theorem lebesgue_number_lemma_of_metric_sUnion {α : Type u} [metric_space α] {s : set α} {c : set (set α)} :
is_compact s(∀ (t : set α), t cis_open t)s ⋃₀c(∃ (δ : ) (H : δ > 0), ∀ (x : α), x s(∃ (t : set α) (H : t c), metric.ball x δ t))

def metric.bounded {α : Type u} [metric_space α] :
set α → Prop

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

Equations
@[simp]
theorem metric.bounded_empty {α : Type u} [metric_space α] :

theorem metric.bounded_iff_mem_bounded {α : Type u} [metric_space α] {s : set α} :
metric.bounded s ∀ (x : α), x smetric.bounded s

theorem metric.bounded.subset {α : Type u} [metric_space α] {s t : set α} :

Subsets of a bounded set are also bounded

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

Closed balls are bounded

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

Open balls are bounded

theorem metric.bounded_iff_subset_ball {α : Type u} [metric_space α] {s : set α} (c : α) :

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

theorem bounded.closure {α : Type u} [metric_space α] {s : set α} :

Alias of bounded_closure_of_bounded.

@[simp]
theorem metric.bounded_union {α : Type u} [metric_space α] {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} [metric_space α] {I : set β} {s : β → set α} :
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} [metric_space α] {s : set α} :

A compact set is bounded

theorem is_compact.bounded {α : Type u} [metric_space α] {s : set α} :

Alias of bounded_of_compact.

theorem metric.bounded_of_finite {α : Type u} [metric_space α] {s : set α} :

A finite set is bounded

theorem metric.bounded_singleton {α : Type u} [metric_space α] {x : α} :

A singleton is bounded

theorem metric.bounded_range_iff {α : Type u} {β : Type v} [metric_space α] {f : β → α} :
metric.bounded (set.range 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} [metric_space α] {s : set α} [compact_space α] :

In a compact space, all sets are bounded

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

theorem metric.proper_image_of_proper {α : Type u} {β : Type v} [metric_space α] [proper_space α] [metric_space β] (f : α → β) (f_cont : continuous f) (hf : set.range f = set.univ) (C : ) :
(∀ (x y : α), dist x y C * dist (f x) (f y))proper_space β

The image of a proper space under an expanding onto map is proper.

def metric.diam {α : Type u} [metric_space α] :
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} [metric_space α] {s : set α} :

The diameter of a set is always nonnegative

theorem metric.diam_subsingleton {α : Type u} [metric_space α] {s : set α} :

@[simp]
theorem metric.diam_empty {α : Type u} [metric_space α] :

The empty set has zero diameter

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

A singleton has zero diameter

theorem metric.diam_pair {α : Type u} [metric_space α] {x y : α} :
metric.diam {x, y} = dist x y

theorem metric.diam_triple {α : Type u} [metric_space α] {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} [metric_space α] {s : set α} {C : } :
(∀ (x : α), x s∀ (y : α), y sdist x y C)emetric.diam s ennreal.of_real 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} [metric_space α] {s : set α} {C : } :
0 C(∀ (x : α), x s∀ (y : α), y sdist x y C)metric.diam s 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} [metric_space α] {s : set α} (hs : s.nonempty) {C : } :
(∀ (x : α), x s∀ (y : α), y sdist x y C)metric.diam s 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} [metric_space α] {s : set α} {x y : α} :
emetric.diam s x sy sdist x y metric.diam s

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

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

theorem metric.bounded.ediam_ne_top {α : Type u} [metric_space α] {s : set α} :

theorem metric.dist_le_diam_of_mem {α : Type u} [metric_space α] {s : set α} {x y : α} :
metric.bounded sx sy sdist x y metric.diam s

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} [metric_space α] {s : set α} :

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} [metric_space α] {s t : set α} :

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

theorem metric.diam_union {α : Type u} [metric_space α] {s : set α} {x y : α} {t : set α} :
x sy tmetric.diam (s t) metric.diam s + dist x y + metric.diam t

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} [metric_space α] {s t : set α} :

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

theorem metric.diam_closed_ball {α : Type u} [metric_space α] {x : α} {r : } :

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

theorem metric.diam_ball {α : Type u} [metric_space α] {x : α} {r : } :
0 rmetric.diam (metric.ball x r) 2 * r

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