# mathlib3documentation

topology.metric_space.basic

# Metric spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
• dist_self dist_comm dist_triangle = dist_self dist_comm dist_triangle uniform_space_of_dist._proof_1
def bornology.of_dist {α : Type u_1} (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 bornology from a distance function and metric space axioms.

Equations
@[ext, class]
structure has_dist (α : Type u_3) :
Type u_3

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

Instances of this typeclass
Instances of other typeclasses for `has_dist`
• has_dist.has_sizeof_inst
theorem has_dist.ext_iff {α : Type u_3} (x y : has_dist α) :
theorem has_dist.ext {α : Type u_3} (x y : has_dist α)  :
x = y
@[protected]

This tactic is used to populate `pseudo_metric_space.edist_dist` when the default `edist` is used.

@[class]
structure pseudo_metric_space (α : Type u) :
• to_has_dist :
• dist_self : (x : α), = 0
• dist_comm : (x y : α), =
• dist_triangle : (x y z : α), +
• edist : α
• edist_dist : ( (x y : α), . "edist_dist_tac"
• to_uniform_space :
• uniformity_dist : = (ε : ) (H : ε > 0), filter.principal {p : α × α | p.snd < ε}) . "control_laws_tac"
• to_bornology :
• cobounded_sets : = {s : set α | (C : ), ⦃x : α⦄, x s ⦃y : α⦄, y s C} . "control_laws_tac"

Pseudo metric and Metric spaces

A pseudo metric space is endowed with a distance for which the requirement `d(x,y)=0 → x = y` might not hold. A metric space is a pseudo metric space such that `d(x,y)=0 → x = y`. Each pseudo 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 `pseudo_metric_space` structure, the uniformity fields are not necessary, they will be filled in by default. In the same way, each (pseudo) metric space induces a (pseudo) emetric space structure. It is included in the structure, but filled in by default.

Instances of this typeclass
Instances of other typeclasses for `pseudo_metric_space`
• pseudo_metric_space.has_sizeof_inst
@[ext]
theorem pseudo_metric_space.ext {α : Type u_1} {m m' : pseudo_metric_space α}  :
m = m'

Two pseudo metric space structures with the same distance function coincide.

@[protected, instance]
Equations
def pseudo_metric_space.of_dist_topology {α : 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) (H : (s : set α), (x : α), x s ( (ε : ) (H : ε > 0), (y : α), dist x y < ε y s)) :

Construct a pseudo-metric space structure whose underlying topological space structure (definitionally) agrees which a pre-existing topology which is compatible with a given distance function.

Equations
@[simp]
theorem dist_self {α : Type u} (x : α) :
= 0
theorem dist_comm {α : Type u} (x y : α) :
=
theorem edist_dist {α : Type u} (x y : α) :
=
theorem dist_triangle {α : Type u} (x y z : α) :
+
theorem dist_triangle_left {α : Type u} (x y z : α) :
+
theorem dist_triangle_right {α : Type u} (x y z : α) :
+
theorem dist_triangle4 {α : Type u} (x y z w : α) :
+ +
theorem dist_triangle4_left {α : Type u} (x₁ y₁ x₂ y₂ : α) :
y₂ y₁ + x₂ + y₂)
theorem dist_triangle4_right {α : Type u} (x₁ y₁ x₂ y₂ : α) :
y₁ x₂ + y₂ + y₂
theorem dist_le_Ico_sum_dist {α : Type u} (f : α) {m n : } (h : m n) :
has_dist.dist (f m) (f n) n).sum (λ (i : ), has_dist.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 : ) :
has_dist.dist (f 0) (f n) (finset.range n).sum (λ (i : ), has_dist.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 k k < n has_dist.dist (f k) (f (k + 1)) d k) :
has_dist.dist (f m) (f n) n).sum (λ (i : ), 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 < n has_dist.dist (f k) (f (k + 1)) d k) :
has_dist.dist (f 0) (f n) (finset.range n).sum (λ (i : ), 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 : α) :
| - |
theorem dist_nonneg {α : Type u} {x y : α} :
0

Extension for the `positivity` tactic: distances are nonnegative.

@[simp]
theorem abs_dist {α : Type u} {a b : α} :
|| =
@[class]
structure has_nndist (α : Type u_3) :
Type u_3
• nndist : α

A version of `has_dist` that takes value in `ℝ≥0`.

Instances of this typeclass
Instances of other typeclasses for `has_nndist`
• has_nndist.has_sizeof_inst
@[protected, instance]

Distance as a nonnegative real number.

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

Express `nndist` in terms of `edist`

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

Express `edist` in terms of `nndist`

@[simp, norm_cast]
theorem coe_nnreal_ennreal_nndist {α : Type u} (x y : α) :
y) =
@[simp, norm_cast]
theorem edist_lt_coe {α : Type u} {x y : α} {c : nnreal} :
< c < c
@[simp, norm_cast]
theorem edist_le_coe {α : Type u} {x y : α} {c : nnreal} :
theorem edist_lt_top {α : Type u_1} (x y : α) :

In a pseudometric space, the extended distance is always finite

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

In a pseudometric space, the extended distance is always finite

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

`nndist x x` vanishes

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

Express `dist` in terms of `nndist`

@[simp, norm_cast]
theorem coe_nndist {α : Type u} (x y : α) :
y) =
@[simp, norm_cast]
theorem dist_lt_coe {α : Type u} {x y : α} {c : nnreal} :
< c < c
@[simp, norm_cast]
theorem dist_le_coe {α : Type u} {x y : α} {c : nnreal} :
@[simp]
theorem edist_lt_of_real {α : Type u} {x y : α} {r : } :
< r
@[simp]
theorem edist_le_of_real {α : Type u} {x y : α} {r : } (hr : 0 r) :
r
theorem nndist_dist {α : Type u} (x y : α) :

Express `nndist` in terms of `dist`

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

Triangle inequality for the nonnegative distance

theorem nndist_triangle_left {α : Type u} (x y z : α) :
theorem nndist_triangle_right {α : Type u} (x y z : α) :
theorem dist_edist {α : Type u} (x y : α) :

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 : α | < ε}
Instances for `↥metric.ball`
@[simp]
theorem metric.mem_ball {α : Type u} {x y : α} {ε : } :
y ε < ε
theorem metric.mem_ball' {α : Type u} {x y : α} {ε : } :
y ε < ε
theorem metric.pos_of_mem_ball {α : Type u} {x y : α} {ε : } (hy : y ε) :
0 < ε
theorem metric.mem_ball_self {α : Type u} {x : α} {ε : } (h : 0 < ε) :
x ε
@[simp]
theorem metric.nonempty_ball {α : Type u} {x : α} {ε : } :
ε).nonempty 0 < ε
@[simp]
theorem metric.ball_eq_empty {α : Type u} {x : α} {ε : } :
ε = ε 0
@[simp]
theorem metric.ball_zero {α : Type u} {x : α} :
0 =
theorem metric.exists_lt_mem_ball_of_mem_ball {α : Type u} {x y : α} {ε : } (h : x ε) :
(ε' : ) (H : ε' < ε), x ε'

If a point belongs to an open ball, then there is a strictly smaller radius whose ball also contains it.

See also `exists_lt_subset_ball`.

theorem metric.ball_eq_ball {α : Type u} (ε : ) (x : α) :
{p : α × α | p.fst < ε} = ε
theorem metric.ball_eq_ball' {α : Type u} (ε : ) (x : α) :
{p : α × α | p.snd < ε} = ε
@[simp]
theorem metric.Union_ball_nat {α : Type u} (x : α) :
( (n : ), n) = set.univ
@[simp]
theorem metric.Union_ball_nat_succ {α : Type u} (x : α) :
( (n : ), (n + 1)) = set.univ
def metric.closed_ball {α : Type u} (x : α) (ε : ) :
set α

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

Equations
• = {y : α | ε}
Instances for `↥metric.closed_ball`
@[simp]
theorem metric.mem_closed_ball {α : Type u} {x y : α} {ε : } :
y ε
theorem metric.mem_closed_ball' {α : Type u} {x y : α} {ε : } :
y ε
def metric.sphere {α : Type u} (x : α) (ε : ) :
set α

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

Equations
• = {y : α | = ε}
Instances for `↥metric.sphere`
@[simp]
theorem metric.mem_sphere {α : Type u} {x y : α} {ε : } :
y = ε
theorem metric.mem_sphere' {α : Type u} {x y : α} {ε : } :
y = ε
theorem metric.ne_of_mem_sphere {α : Type u} {x y : α} {ε : } (h : y ) (hε : ε 0) :
y x
theorem metric.nonneg_of_mem_sphere {α : Type u} {x y : α} {ε : } (hy : y ) :
0 ε
@[simp]
theorem metric.sphere_eq_empty_of_neg {α : Type u} {x : α} {ε : } (hε : ε < 0) :
theorem metric.sphere_eq_empty_of_subsingleton {α : Type u} {x : α} {ε : } [subsingleton α] (hε : ε 0) :
theorem metric.sphere_is_empty_of_subsingleton {α : Type u} {x : α} {ε : } [subsingleton α] (hε : ε 0) :
theorem metric.mem_closed_ball_self {α : Type u} {x : α} {ε : } (h : 0 ε) :
x
@[simp]
theorem metric.nonempty_closed_ball {α : Type u} {x : α} {ε : } :
ε).nonempty 0 ε
@[simp]
theorem metric.closed_ball_eq_empty {α : Type u} {x : α} {ε : } :
ε < 0
theorem metric.closed_ball_eq_sphere_of_nonpos {α : Type u} {x : α} {ε : } (hε : ε 0) :
=

Closed balls and spheres coincide when the radius is non-positive

theorem metric.ball_subset_closed_ball {α : Type u} {x : α} {ε : } :
ε
theorem metric.sphere_subset_closed_ball {α : Type u} {x : α} {ε : } :
theorem metric.closed_ball_disjoint_ball {α : Type u} {x y : α} {δ ε : } (h : δ + ε ) :
ε)
theorem metric.ball_disjoint_closed_ball {α : Type u} {x y : α} {δ ε : } (h : δ + ε ) :
disjoint δ) ε)
theorem metric.ball_disjoint_ball {α : Type u} {x y : α} {δ ε : } (h : δ + ε ) :
disjoint δ) ε)
theorem metric.closed_ball_disjoint_closed_ball {α : Type u} {x y : α} {δ ε : } (h : δ + ε < ) :
ε)
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.mem_ball_comm {α : Type u} {x y : α} {ε : } :
x ε y ε
theorem metric.mem_closed_ball_comm {α : Type u} {x y : α} {ε : } :
x y
theorem metric.mem_sphere_comm {α : Type u} {x y : α} {ε : } :
x y
theorem metric.ball_subset_ball {α : Type u} {x : α} {ε₁ ε₂ : } (h : ε₁ ε₂) :
ε₁ ε₂
theorem metric.closed_ball_eq_bInter_ball {α : Type u} {x : α} {ε : } :
= (δ : ) (H : δ > ε), δ
theorem metric.ball_subset_ball' {α : Type u} {x y : α} {ε₁ ε₂ : } (h : ε₁ + ε₂) :
ε₁ ε₂
theorem metric.closed_ball_subset_closed_ball {α : Type u} {x : α} {ε₁ ε₂ : } (h : ε₁ ε₂) :
theorem metric.closed_ball_subset_closed_ball' {α : Type u} {x y : α} {ε₁ ε₂ : } (h : ε₁ + ε₂) :
theorem metric.closed_ball_subset_ball {α : Type u} {x : α} {ε₁ ε₂ : } (h : ε₁ < ε₂) :
ε₂
theorem metric.closed_ball_subset_ball' {α : Type u} {x y : α} {ε₁ ε₂ : } (h : ε₁ + < ε₂) :
ε₂
theorem metric.dist_le_add_of_nonempty_closed_ball_inter_closed_ball {α : Type u} {x y : α} {ε₁ ε₂ : } (h : ε₁ ε₂).nonempty) :
ε₁ + ε₂
theorem metric.dist_lt_add_of_nonempty_closed_ball_inter_ball {α : Type u} {x y : α} {ε₁ ε₂ : } (h : ε₁ ε₂).nonempty) :
< ε₁ + ε₂
theorem metric.dist_lt_add_of_nonempty_ball_inter_closed_ball {α : Type u} {x y : α} {ε₁ ε₂ : } (h : ε₁ ε₂).nonempty) :
< ε₁ + ε₂
theorem metric.dist_lt_add_of_nonempty_ball_inter_ball {α : Type u} {x y : α} {ε₁ ε₂ : } (h : ε₁ ε₂).nonempty) :
< ε₁ + ε₂
@[simp]
theorem metric.Union_closed_ball_nat {α : Type u} (x : α) :
theorem metric.Union_inter_closed_ball_nat {α : Type u} (s : set α) (x : α) :
( (n : ), s = s
theorem metric.ball_subset {α : Type u} {x y : α} {ε₁ ε₂ : } (h : ε₂ - ε₁) :
ε₁ ε₂
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), ε' ε
theorem metric.forall_of_forall_mem_closed_ball {α : Type u} (p : α Prop) (x : α) (H : ∃ᶠ (R : ) in filter.at_top, (y : α), y p y) (y : α) :
p y

If a property holds for all points in closed balls of arbitrarily large radii, then it holds for all points.

theorem metric.forall_of_forall_mem_ball {α : Type u} (p : α Prop) (x : α) (H : ∃ᶠ (R : ) in filter.at_top, (y : α), y R p y) (y : α) :
p y

If a property holds for all points in balls of arbitrarily large radii, then it holds for all points.

theorem metric.is_bounded_iff {α : Type u} {s : set α} :
(C : ), ⦃x : α⦄, x s ⦃y : α⦄, y s C
theorem metric.is_bounded_iff_eventually {α : Type u} {s : set α} :
∀ᶠ (C : ) in filter.at_top, ⦃x : α⦄, x s ⦃y : α⦄, y s C
theorem metric.is_bounded_iff_exists_ge {α : Type u} {s : set α} (c : ) :
(C : ), c C ⦃x : α⦄, x s ⦃y : α⦄, y s C
theorem metric.is_bounded_iff_nndist {α : Type u} {s : set α} :
(C : nnreal), ⦃x : α⦄, x s ⦃y : α⦄, y s C
theorem metric.uniformity_basis_dist {α : Type u}  :
(uniformity α).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), {p : α × α | p.snd < ε})
@[protected]
theorem metric.mk_uniformity_basis {α : Type u} {β : Type u_1} {p : β Prop} {f : β } (hf₀ : (i : β), p i 0 < f i) (hf : ⦃ε : ⦄, 0 < ε ( (i : β) (hi : p i), f i ε)) :
(uniformity α).has_basis p (λ (i : β), {p : α × α | 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_rat {α : Type u}  :
(uniformity α).has_basis (λ (r : ), 0 < r) (λ (r : ), {p : α × α | p.snd < r})
theorem metric.uniformity_basis_dist_inv_nat_succ {α : Type u}  :
(uniformity α).has_basis (λ (_x : ), true) (λ (n : ), {p : α × α | p.snd < 1 / (n + 1)})
theorem metric.uniformity_basis_dist_inv_nat_pos {α : Type u}  :
(uniformity α).has_basis (λ (n : ), 0 < n) (λ (n : ), {p : α × α | p.snd < 1 / n})
theorem metric.uniformity_basis_dist_pow {α : Type u} {r : } (h0 : 0 < r) (h1 : r < 1) :
(uniformity α).has_basis (λ (n : ), true) (λ (n : ), {p : α × α | p.snd < r ^ n})
theorem metric.uniformity_basis_dist_lt {α : Type u} {R : } (hR : 0 < R) :
(uniformity α).has_basis (λ (r : ), 0 < r r < R) (λ (r : ), {p : α × α | p.snd < r})
@[protected]
theorem metric.mk_uniformity_basis_le {α : Type u} {β : Type u_1} {p : β Prop} {f : β } (hf₀ : (x : β), p x 0 < f x) (hf : (ε : ), 0 < ε ( (x : β) (hx : p x), f x ε)) :
(uniformity α).has_basis p (λ (x : β), {p : α × α | 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}  :
(uniformity α).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), {p : α × α | 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) :
(uniformity α).has_basis (λ (n : ), true) (λ (n : ), {p : α × α | p.snd r ^ n})
theorem metric.mem_uniformity_dist {α : Type u} {s : set × α)} :
s (ε : ) (H : ε > 0), {a b : α}, < ε (a, b) s
theorem metric.dist_mem_uniformity {α : Type u} {ε : } (ε0 : 0 < ε) :
{p : α × α | 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 : α}, < δ has_dist.dist (f a) (f b) < ε)
theorem metric.uniform_continuous_on_iff {α : Type u} {β : Type v} {f : α β} {s : set α} :
(ε : ), ε > 0 ( (δ : ) (H : δ > 0), (x : α), x s (y : α), y s < δ has_dist.dist (f x) (f y) < ε)
theorem metric.uniform_continuous_on_iff_le {α : Type u} {β : Type v} {f : α β} {s : set α} :
(ε : ), ε > 0 ( (δ : ) (H : δ > 0), (x : α), x s (y : α), y s δ has_dist.dist (f x) (f y) ε)
theorem metric.uniform_embedding_iff {α : Type u} {β : Type v} {f : α β} :
(δ : ), δ > 0 ( (ε : ) (H : ε > 0), {a b : α}, has_dist.dist (f a) (f b) < ε < δ)
theorem metric.controlled_of_uniform_embedding {α : Type u} {β : Type v} {f : α β} :
(( (ε : ), ε > 0 ( (δ : ) (H : δ > 0), {a b : α}, < δ has_dist.dist (f a) (f b) < ε)) (δ : ), δ > 0 ( (ε : ) (H : ε > 0), {a b : α}, has_dist.dist (f a) (f 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) (_x : fintype β) (F : s β), (x y : s), F x = F y < ε)) :

A pseudometric 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_uniformly_on_filter_iff {α : Type u} {β : Type v} {ι : Type u_1} {F : ι β α} {f : β α} {p : filter ι} {p' : filter β} :
p' (ε : ), ε > 0 (∀ᶠ (n : ι × β) in p.prod p', has_dist.dist (f n.snd) (F n.fst n.snd) < ε)

Expressing uniform convergence using `dist`

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), ∀ᶠ (n : ι) in p, (y : β), y t has_dist.dist (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 s has_dist.dist (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 nhds x), ∀ᶠ (n : ι) in p, (y : β), y t has_dist.dist (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 : β), has_dist.dist (f x) (F n x) < ε)

Expressing uniform convergence using `dist`.

@[protected]
theorem metric.cauchy_iff {α : Type u} {f : filter α} :
f.ne_bot (ε : ), ε > 0 ( (t : set α) (H : t f), (x : α), x t (y : α), y t < ε)
theorem metric.nhds_basis_ball {α : Type u} {x : α} :
(nhds x).has_basis (λ (ε : ), 0 < ε) (metric.ball x)
theorem metric.mem_nhds_iff {α : Type u} {x : α} {s : set α} :
s nhds x (ε : ) (H : ε > 0), ε s
theorem metric.eventually_nhds_iff {α : Type u} {x : α} {p : α Prop} :
(∀ᶠ (y : α) in nhds x, p y) (ε : ) (H : ε > 0), ⦃y : α⦄, < ε p y
theorem metric.eventually_nhds_iff_ball {α : Type u} {x : α} {p : α Prop} :
(∀ᶠ (y : α) in nhds x, p y) (ε : ) (H : ε > 0), (y : α), y ε p y
theorem metric.eventually_prod_nhds_iff {α : Type u} {ι : Type u_2} {f : filter ι} {x₀ : α} {p : ι × α Prop} :
(∀ᶠ (x : ι × α) in f.prod (nhds x₀), p x) (pa : ι Prop) (ha : ∀ᶠ (i : ι) in f, pa i) (ε : ) (H : ε > 0), {i : ι}, pa i {x : α}, x₀ < ε p (i, x)

A version of `filter.eventually_prod_iff` where the second filter consists of neighborhoods in a pseudo-metric space.

theorem metric.eventually_nhds_prod_iff {ι : Type u_1} {α : Type u_2} {f : filter ι} {x₀ : α} {p : α × ι Prop} :
(∀ᶠ (x : α × ι) in (nhds x₀).prod f, p x) (ε : ) (H : ε > 0) (pa : ι Prop) (ha : ∀ᶠ (i : ι) in f, pa i), {x : α}, x₀ < ε {i : ι}, pa i p (x, i)

A version of `filter.eventually_prod_iff` where the first filter consists of neighborhoods in a pseudo-metric space.

theorem metric.nhds_basis_closed_ball {α : Type u} {x : α} :
(nhds x).has_basis (λ (ε : ), 0 < ε)
theorem metric.nhds_basis_ball_inv_nat_succ {α : Type u} {x : α} :
(nhds x).has_basis (λ (_x : ), true) (λ (n : ), (1 / (n + 1)))
theorem metric.nhds_basis_ball_inv_nat_pos {α : Type u} {x : α} :
(nhds 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) :
(nhds 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) :
(nhds 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 < ε) :
ε nhds x
theorem metric.closed_ball_mem_nhds {α : Type u} (x : α) {ε : } (ε0 : 0 < ε) :
theorem metric.closed_ball_mem_nhds_of_mem {α : Type u} {x c : α} {ε : } (h : x ε) :
theorem metric.nhds_within_basis_ball {α : Type u} {x : α} {s : set α} :
s).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), ε s)
theorem metric.mem_nhds_within_iff {α : Type u} {x : α} {s t : set α} :
s t (ε : ) (H : ε > 0), ε t s
theorem metric.tendsto_nhds_within_nhds_within {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α β} {a : α} {b : β} :
s) t) (ε : ), ε > 0 ( (δ : ) (H : δ > 0), {x : α}, x s < δ f x t has_dist.dist (f x) b < ε)
theorem metric.tendsto_nhds_within_nhds {α : Type u} {β : Type v} {s : set α} {f : α β} {a : α} {b : β} :
s) (nhds b) (ε : ), ε > 0 ( (δ : ) (H : δ > 0), {x : α}, x s < δ has_dist.dist (f x) b < ε)
theorem metric.tendsto_nhds_nhds {α : Type u} {β : Type v} {f : α β} {a : α} {b : β} :
(nhds a) (nhds b) (ε : ), ε > 0 ( (δ : ) (H : δ > 0), {x : α}, < δ has_dist.dist (f x) b < ε)
theorem metric.continuous_at_iff {α : Type u} {β : Type v} {f : α β} {a : α} :
(ε : ), ε > 0 ( (δ : ) (H : δ > 0), {x : α}, < δ has_dist.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 s < δ has_dist.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 s < δ has_dist.dist (f a) (f b) < ε)
theorem metric.continuous_iff {α : Type u} {β : Type v} {f : α β} :
(b : α) (ε : ), ε > 0 ( (δ : ) (H : δ > 0), (a : α), < δ has_dist.dist (f a) (f b) < ε)
theorem metric.tendsto_nhds {α : Type u} {β : Type v} {f : filter β} {u : β α} {a : α} :
(nhds a) (ε : ), ε > 0 (∀ᶠ (x : β) in f, has_dist.dist (u x) a < ε)
theorem metric.continuous_at_iff' {α : Type u} {β : Type v} {f : β α} {b : β} :
(ε : ), ε > 0 (∀ᶠ (x : β) in nhds b, has_dist.dist (f x) (f b) < ε)
theorem metric.continuous_within_at_iff' {α : Type u} {β : Type v} {f : β α} {b : β} {s : set β} :
b (ε : ), ε > 0 (∀ᶠ (x : β) in s, has_dist.dist (f x) (f b) < ε)
theorem metric.continuous_on_iff' {α : Type u} {β : Type v} {f : β α} {s : set β} :
(b : β), b s (ε : ), ε > 0 (∀ᶠ (x : β) in s, has_dist.dist (f x) (f b) < ε)
theorem metric.continuous_iff' {α : Type u} {β : Type v} {f : β α} :
(a : β) (ε : ), ε > 0 (∀ᶠ (x : β) in nhds a, has_dist.dist (f x) (f a) < ε)
theorem metric.tendsto_at_top {α : Type u} {β : Type v} [nonempty β] {u : β α} {a : α} :
(ε : ), ε > 0 ( (N : β), (n : β), n N has_dist.dist (u n) a < ε)
theorem metric.tendsto_at_top' {α : Type u} {β : Type v} [nonempty β] [no_max_order β] {u : β α} {a : α} :
(ε : ), ε > 0 ( (N : β), (n : β), n > N has_dist.dist (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 {α : Type u_1} {x : α} :
is_open {x} (ε : ) (H : ε > 0), (y : α), < ε 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 dense.exists_dist_lt {α : Type u} {s : set α} (hs : dense s) (x : α) {ε : } (hε : 0 < ε) :
(y : α) (H : y s), < ε
theorem dense_range.exists_dist_lt {α : Type u} {β : Type u_1} {f : β α} (hf : dense_range f) (x : α) {ε : } (hε : 0 < ε) :
(y : β), (f y) < ε
@[protected]
theorem pseudo_metric.uniformity_basis_edist {α : Type u}  :
(uniformity α).has_basis (λ (ε : ennreal), 0 < ε) (λ (ε : ennreal), {p : α × α | < ε})

Expressing the uniformity in terms of `edist`

theorem metric.uniformity_edist {α : Type u}  :
= (ε : ennreal) (H : ε > 0), filter.principal {p : α × α | < ε}
@[protected, instance]

A pseudometric space induces a pseudoemetric space

Equations
theorem metric.eball_top_eq_univ {α : Type u} (x : α) :

In a pseudometric space, an open ball of infinite radius is the whole space

@[simp]
theorem metric.emetric_ball {α : Type u} {x : α} {ε : } :
= ε

Balls defined using the distance or the edistance coincide

@[simp]
theorem metric.emetric_ball_nnreal {α : Type u} {x : α} {ε : nnreal} :
= ε

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

@[simp]
theorem metric.emetric_closed_ball_nnreal {α : Type u} {x : α} {ε : nnreal} :

Closed balls defined using the distance or the edistance coincide

@[simp]
theorem metric.emetric_ball_top {α : Type u} (x : α) :
theorem metric.inseparable_iff {α : Type u} {x y : α} :
y = 0

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
theorem pseudo_metric_space.replace_uniformity_eq {α : Type u_1} [U : uniform_space α] (m : pseudo_metric_space α) (H : = ) :
= m
@[reducible]

Build a new pseudo metric space from an old one where the bundled topological structure is provably (but typically non-definitionaly) equal to some given topological 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 : α), ) (h : (x y : α), dist x y = 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 : pseudo_emetric_space α] (h : (x 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
def pseudo_metric_space.replace_bornology {α : Type u_1} [B : bornology α] (m : pseudo_metric_space α) (H : (s : set α), ) :

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

Equations
theorem pseudo_metric_space.replace_bornology_eq {α : Type u_1} [m : pseudo_metric_space α] [B : bornology α] (H : (s : set α), ) :
= m
theorem metric.complete_of_convergent_controlled_sequences {α : Type u} (B : ) (hB : (n : ), 0 < B n) (H : (u : α), ( (N n m : ), N n N m has_dist.dist (u n) (u m) < B N) ( (x : α), (nhds 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 : α), (nhds a)))
@[protected, instance]

Instantiate the reals as a pseudometric space.

Equations
theorem real.dist_eq (x y : ) :
= |x - y|
theorem real.nndist_eq (x y : ) :
theorem real.nndist_eq' (x y : ) :
theorem real.dist_0_eq_abs (x : ) :
= |x|
theorem real.dist_left_le_of_mem_uIcc {x y z : } (h : y z) :
theorem real.dist_right_le_of_mem_uIcc {x y z : } (h : y z) :
theorem real.dist_le_of_mem_uIcc {x y x' y' : } (hx : x set.uIcc x' y') (hy : y set.uIcc x' y') :
y'
theorem real.dist_le_of_mem_Icc {x y x' y' : } (hx : x set.Icc x' y') (hy : y set.Icc x' y') :
y' - x'
theorem real.dist_le_of_mem_Icc_01 {x y : } (hx : x 1) (hy : y 1) :
1
@[protected, instance]
theorem real.ball_eq_Ioo (x r : ) :
r = set.Ioo (x - r) (x + r)
theorem real.closed_ball_eq_Icc {x r : } :
= set.Icc (x - r) (x + r)
theorem real.Ioo_eq_ball (x y : ) :
y = metric.ball ((x + y) / 2) ((y - x) / 2)
theorem real.Icc_eq_closed_ball (x y : ) :
y = metric.closed_ball ((x + y) / 2) ((y - x) / 2)
theorem totally_bounded_Icc {α : Type u} [preorder α] (a b : α) :
theorem totally_bounded_Ico {α : Type u} [preorder α] (a b : α) :
theorem totally_bounded_Ioc {α : Type u} [preorder α] (a b : α) :
theorem totally_bounded_Ioo {α : Type u} [preorder α] (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₀ (nhds 0)) :
t₀ (nhds 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₀ (nhds 0)) :
t₀ (nhds 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 : α × α), p.snd) (nhds 0)
theorem cauchy_seq_iff_tendsto_dist_at_top_0 {α : Type u} {β : Type v} [nonempty β] {u : β α} :
filter.tendsto (λ (n : β × β), has_dist.dist (u n.fst) (u n.snd)) filter.at_top (nhds 0)
theorem tendsto_uniformity_iff_dist_tendsto_zero {α : Type u} {ι : Type u_1} {f : ι α × α} {p : filter ι} :
(uniformity α) filter.tendsto (λ (x : ι), has_dist.dist (f x).fst (f x).snd) p (nhds 0)
theorem filter.tendsto.congr_dist {α : Type u} {ι : Type u_1} {f₁ f₂ : ι α} {p : filter ι} {a : α} (h₁ : p (nhds a)) (h : filter.tendsto (λ (x : ι), has_dist.dist (f₁ x) (f₂ x)) p (nhds 0)) :
p (nhds a)
theorem tendsto_of_tendsto_of_dist {α : Type u} {ι : Type u_1} {f₁ f₂ : ι α} {p : filter ι} {a : α} (h₁ : p (nhds a)) (h : filter.tendsto (λ (x : ι), has_dist.dist (f₁ x) (f₂ x)) p (nhds 0)) :
p (nhds 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 : ι), has_dist.dist (f₁ x) (f₂ x)) p (nhds 0)) :
p (nhds a) p (nhds a)
theorem eventually_closed_ball_subset {α : Type u} {x : α} {u : set α} (hu : u nhds x) :
∀ᶠ (r : ) in nhds 0, u

If `u` is a neighborhood of `x`, then for small enough `r`, the closed ball `closed_ball x r` is contained in `u`.

@[nolint]
theorem metric.cauchy_seq_iff {α : Type u} {β : Type v} [nonempty β] {u : β α} :
(ε : ), ε > 0 ( (N : β), (m : β), m N (n : β), n N has_dist.dist (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 N has_dist.dist (u n) (u N) < ε)

A variation around the pseudometric characterization of Cauchy sequences

@[nolint]
theorem metric.uniform_cauchy_seq_on_iff {α : Type u} {β : Type v} [nonempty β] {γ : Type u_1} {F : β γ α} {s : set γ} :
(ε : ), ε > 0 ( (N : β), (m : β), m N (n : β), n N (x : γ), x s has_dist.dist (F m x) (F n x) < ε)

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

theorem cauchy_seq_of_le_tendsto_0' {α : Type u} {β : Type v} [nonempty β] {s : β α} (b : β ) (h : (n m : β), n m has_dist.dist (s n) (s m) b n) (h₀ : (nhds 0)) :

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

theorem cauchy_seq_of_le_tendsto_0 {α : Type u} {β : Type v} [nonempty β] {s : β α} (b : β ) (h : (n m N : β), N n N m has_dist.dist (s n) (s m) b N) (h₀ : (nhds 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 : ), has_dist.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 n N m has_dist.dist (s n) (s m) b N)

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
def inducing.comap_pseudo_metric_space {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) :

Pull back a pseudometric space structure by an inducing map. This is a version of `pseudo_metric_space.induced` useful in case if the domain already has a `topological_space` structure.

Equations
def uniform_inducing.comap_pseudo_metric_space {α : Type u_1} {β : Type u_2} (f : α β) (h : uniform_inducing f) :

Pull back a pseudometric space structure by a uniform inducing map. This is a version of `pseudo_metric_space.induced` useful in case if the domain already has a `uniform_space` structure.

Equations
@[protected, instance]
def subtype.pseudo_metric_space {α : Type u} {p : α Prop} :
Equations
theorem subtype.dist_eq {α : Type u} {p : α Prop} (x y : subtype p) :
=
theorem subtype.nndist_eq {α : Type u} {p : α Prop} (x y : subtype p) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem mul_opposite.dist_unop {α : Type u} (x y : αᵐᵒᵖ) :
@[simp]
theorem add_opposite.dist_unop {α : Type u} (x y : αᵃᵒᵖ) :
@[simp]
theorem mul_opposite.dist_op {α : Type u} (x y : α) :
@[simp]
theorem add_opposite.dist_op {α : Type u} (x y : α) :
@[simp]
theorem add_opposite.nndist_unop {α : Type u} (x y : αᵃᵒᵖ) :
@[simp]
theorem mul_opposite.nndist_unop {α : Type u} (x y : αᵐᵒᵖ) :
@[simp]
theorem mul_opposite.nndist_op {α : Type u} (x y : α) :
@[simp]
theorem add_opposite.nndist_op {α : Type u} (x y : α) :
@[protected, instance]
Equations
theorem nnreal.dist_eq (a b : nnreal) :
theorem nnreal.nndist_eq (a b : nnreal) :
= linear_order.max (a - b) (b - a)
@[simp]
theorem nnreal.nndist_zero_eq_val (z : nnreal) :
= z
@[simp]
theorem nnreal.nndist_zero_eq_val' (z : nnreal) :
= z
theorem nnreal.le_add_nndist (a b : nnreal) :
a b +
@[protected, instance]
def ulift.pseudo_metric_space {β : Type v}  :
Equations
theorem ulift.dist_eq {β : Type v} (x y : ulift β) :
=
theorem ulift.nndist_eq {β : Type v} (x y : ulift β) :
@[simp]
theorem ulift.dist_up_up {β : Type v} (x y : β) :
has_dist.dist {down := x} {down := y} =
@[simp]
theorem ulift.nndist_up_up {β : Type v} (x y : β) :
has_nndist.nndist {down := x} {down := y} =
@[protected, instance]
def prod.pseudo_metric_space_max {α : Type u} {β : Type v}  :
Equations
theorem prod.dist_eq {α : Type u} {β : Type v} {x y : α × β} :
= y.snd)
@[simp]
theorem dist_prod_same_left {α : Type u} {β : Type v} {x : α} {y₁ y₂ : β} :
has_dist.dist (x, y₁) (x, y₂) = y₂
@[simp]
theorem dist_prod_same_right {α : Type u} {β : Type v} {x₁ x₂ : α} {y : β} :
has_dist.dist (x₁, y) (x₂, y) = x₂
theorem ball_prod_same {α : Type u} {β : Type v} (x : α) (y : β) (r : ) :
r ×ˢ r = metric.ball (x, y) r
theorem closed_ball_prod_same {α : Type u} {β : Type v} (x : α) (y : β) (r : ) :
theorem sphere_prod {α : Type u} {β : Type v} (x : α × β) (r : ) :
= r ×ˢ ×ˢ r
theorem uniform_continuous_dist {α : Type u}  :
uniform_continuous (λ (p : α × α), p.snd)
theorem uniform_continuous.dist {α : Type u} {β : Type v} {f g : β α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (b : β), has_dist.dist (f b) (g b))
@[continuity]
theorem continuous_dist {α : Type u}  :
continuous (λ (p : α × α), p.snd)
@[continuity]
theorem continuous.dist {α : Type u} {β : Type v} {f g : β α} (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), has_dist.dist (f b) (g b))
theorem filter.tendsto.dist {α : Type u} {β : Type v} {f g : β α} {x : filter β} {a b : α} (hf : (nhds a)) (hg : (nhds b)) :
filter.tendsto (λ (x : β), has_dist.dist (f x) (g x)) x (nhds b))
theorem nhds_comap_dist {α : Type u} (a : α) :
filter.comap (λ (a' : α), a) (nhds 0) = nhds a
theorem tendsto_iff_dist_tendsto_zero {α : Type u} {β : Type v} {f : β α} {x : filter β} {a : α} :
(nhds a) filter.tendsto (λ (b : β), has_dist.dist (f b) a) x (nhds 0)
theorem continuous_iff_continuous_dist {α : Type u} {β : Type v} {f : β α} :
continuous (λ (x : β × β), has_dist.dist (f x.fst) (f x.snd))
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 : β), has_nndist.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 : β), has_nndist.nndist (f b) (g b))
theorem filter.tendsto.nndist {α : Type u} {β : Type v} {f g : β α} {x : filter β} {a b : α} (hf : (nhds a)) (hg : (nhds b)) :
filter.tendsto (λ (x : β), has_nndist.nndist (f x) (g x)) x (nhds 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 : α} {ε : } :
=
@[simp]
theorem metric.closure_sphere {α : Type u} {x : α} {ε : } :
closure ε) =
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), < ε)

ε-characterization of the closure in pseudometric spaces

theorem metric.mem_closure_range_iff {α : Type u} {β : Type v} {e : β α} {a : α} :
a closure (set.range e) (ε : ), ε > 0 ( (k : β), (e k) < ε)
theorem metric.mem_closure_range_iff_nat {α : Type u} {β : Type v} {e : β α} {a : α} :
a closure (set.range e) (n : ), (k : β), (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), < ε)
theorem metric.closed_ball_zero' {α : Type u} (x : α) :
= closure {x}
theorem metric.dense_iff {α : Type u} {s : set α} :
(x : α) (r : ), r > 0 r s).nonempty
theorem metric.dense_range_iff {α : Type u} {β : Type v} {f : β α} :
(x : α) (r : ), r > 0 ( (y : β), (f y) < r)

If a set `s` is separable, then the corresponding subtype is separable in a metric space. This is not obvious, as the countable set whose closure covers `s` does not need in general to be contained in `s`.

@[protected]
theorem inducing.is_separable_preimage {α : Type u} {β : Type v} {f : β α} (hf : inducing f) {s : set α}  :

The preimage of a separable set by an inducing map is separable.

@[protected]
theorem embedding.is_separable_preimage {α : Type u} {β : Type v} {f : β α} (hf : embedding f) {s : set α}  :
theorem continuous_on.is_separable_image {α : Type u} {β : Type v} {f : α β} {s : set α} (hf : s)  :

If a map is continuous on a separable set `s`, then the image of `s` is also separable.

@[protected, instance]
def pseudo_metric_space_pi {β : Type v} {π : β Type u_3} [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_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (f g : Π (b : β), π b) :
= finset.univ.sup (λ (b : β), has_nndist.nndist (f b) (g b))
theorem dist_pi_def {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (f g : Π (b : β), π b) :
= (finset.univ.sup (λ (b : β), has_nndist.nndist (f b) (g b)))
theorem nndist_pi_le_iff {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] {f g : Π (b : β), π b} {r : nnreal} :
r (b : β), has_nndist.nndist (f b) (g b) r
theorem nndist_pi_lt_iff {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] {f g : Π (b : β), π b} {r : nnreal} (hr : 0 < r) :
< r (b : β), has_nndist.nndist (f b) (g b) < r
theorem nndist_pi_eq_iff {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] {f g : Π (b : β), π b} {r : nnreal} (hr : 0 < r) :
= r ( (i : β), has_nndist.nndist (f i) (g i) = r) (b : β), has_nndist.nndist (f b) (g b) r
theorem dist_pi_lt_iff {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] {f g : Π (b : β), π b} {r : } (hr : 0 < r) :
< r (b : β), has_dist.dist (f b) (g b) < r
theorem dist_pi_le_iff {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] {f g : Π (b : β), π b} {r : } (hr : 0 r) :
r (b : β), has_dist.dist (f b) (g b) r
theorem dist_pi_eq_iff {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] {f g : Π (b : β), π b} {r : } (hr : 0 < r) :
= r ( (i : β), has_dist.dist (f i) (g i) = r) (b : β), has_dist.dist (f b) (g b) r
theorem dist_pi_le_iff' {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] [nonempty β] {f g : Π (b : β), π b} {r : } :
r (b : β), has_dist.dist (f b) (g b) r
theorem dist_pi_const_le {α : Type u} {β : Type v} [fintype β] (a b : α) :
has_dist.dist (λ (_x : β), a) (λ (_x : β), b)
theorem nndist_pi_const_le {α : Type u} {β : Type v} [fintype β] (a b : α) :
has_nndist.nndist (λ (_x : β), a) (λ (_x : β), b)
@[simp]
theorem dist_pi_const {α : Type u} {β : Type v} [fintype β] [nonempty β] (a b : α) :
has_dist.dist (λ (x : β), a) (λ (_x : β), b) =
@[simp]
theorem nndist_pi_const {α : Type u} {β : Type v} [fintype β] [nonempty β] (a b : α) :
has_nndist.nndist (λ (x : β), a) (λ (_x : β), b) =
theorem nndist_le_pi_nndist {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (f g : Π (b : β), π b) (b : β) :
has_nndist.nndist (f b) (g b)
theorem dist_le_pi_dist {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (f g : Π (b : β), π b) (b : β) :
has_dist.dist (f b) (g b)
theorem ball_pi {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (x : Π (b : β), π b) {r : } (hr : 0 < r) :
r = set.univ.pi (λ (b : β), metric.ball (x b) r)

An open ball in a product space is a product of open balls. See also `metric.ball_pi'` for a version assuming `nonempty β` instead of `0 < r`.

theorem ball_pi' {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] [nonempty β] (x : Π (b : β), π b) (r : ) :
r = set.univ.pi (λ (b : β), metric.ball (x b) r)

An open ball in a product space is a product of open balls. See also `metric.ball_pi` for a version assuming `0 < r` instead of `nonempty β`.

theorem closed_ball_pi {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (x : Π (b : β), π b) {r : } (hr : 0 r) :
= set.univ.pi (λ (b : β), metric.closed_ball (x b) r)

A closed ball in a product space is a product of closed balls. See also `metric.closed_ball_pi'` for a version assuming `nonempty β` instead of `0 ≤ r`.

theorem closed_ball_pi' {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] [nonempty β] (x : Π (b : β), π b) (r : ) :
= set.univ.pi (λ (b : β), metric.closed_ball (x b) r)

A closed ball in a product space is a product of closed balls. See also `metric.closed_ball_pi` for a version assuming `0 ≤ r` instead of `nonempty β`.

theorem sphere_pi {β : Type v} {π : β Type u_3} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (x : Π (b : β), π b) {r : } (h : 0 < r ) :
= ( (i : β), ⁻¹' metric.sphere (x i) r)

A sphere in a product space is a union of spheres on each component restricted to the closed ball.

@[simp]
theorem fin.nndist_insert_nth_insert_nth {n : } {α : fin (n + 1) Type u_1} [Π (i : fin (n + 1)), pseudo_metric_space (α i)] (i : fin (n + 1)) (x y : α i) (f g : Π (j : fin n), α ((i.succ_above) j)) :
@[simp]
theorem fin.dist_insert_nth_insert_nth {n : } {α : fin (n + 1) Type u_1} [Π (i : fin (n + 1)), pseudo_metric_space (α i)] (i : fin (n + 1)) (x y : α i) (f g : Π (j : fin n), α ((i.succ_above) j)) :
theorem real.dist_le_of_mem_pi_Icc {β : Type v} [fintype β] {x y x' y' : β } (hx : x set.Icc x' y') (hy : y set.Icc x' y') :
y'
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