mathlib documentation

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 #

Additional useful definitions:

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

source
def uniform_space.core_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) :
uniform_space.core α

Construct a uniform structure core from a distance function and metric space axioms. This is a technical construction that can be immediately used to construct a uniform structure from a distance function and metric space axioms but is also useful when discussing metrizable topologies, see pseudo_metric_space.of_metrizable.

Equations
source
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) :
uniform_space α

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

Equations
source
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) :
bornology α

Construct a bornology from a distance function and metric space axioms.

Equations
source
@[ext, 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
source
theorem has_dist.ext_iff {α : Type u_1} (x y : has_dist α) :
x = y ↔ dist = dist
source
theorem has_dist.ext {α : Type u_1} (x y : has_dist α) (h : dist = dist) :
x = y
source
@[protected]
meta def pseudo_metric_space.edist_dist_tac  :
tactic unit

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

source
@[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
source
@[ext]
theorem pseudo_metric_space.ext {α : Type u_1} {m m' : pseudo_metric_space α} (h : pseudo_metric_space.to_has_dist = pseudo_metric_space.to_has_dist) :
m = m'

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

source
@[protected, instance]
def metric_space.to_uniform_space' {α : Type u} [pseudo_metric_space α] :
uniform_space α
Equations
source
@[protected, instance]
def pseudo_metric_space.to_has_edist {α : Type u} [pseudo_metric_space α] :
has_edist α
Equations
source
def pseudo_metric_space.of_metrizable {α : Type u_1} [topological_space α] (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 α), is_open s ↔ ∀ (x : α), x ∈ s → (∃ (ε : ℝ) (H : ε > 0), ∀ (y : α), dist x y < ε → y ∈ s)) :
pseudo_metric_space α

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
source
@[simp]
theorem dist_self {α : Type u} [pseudo_metric_space α] (x : α) :
dist x x = 0
source
theorem dist_comm {α : Type u} [pseudo_metric_space α] (x y : α) :
dist x y = dist y x
source
theorem edist_dist {α : Type u} [pseudo_metric_space α] (x y : α) :
edist x y = ennreal.of_real (dist x y)
source
theorem dist_triangle {α : Type u} [pseudo_metric_space α] (x y z : α) :
dist x z ≤ dist x y + dist y z
source
theorem dist_triangle_left {α : Type u} [pseudo_metric_space α] (x y z : α) :
dist x y ≤ dist z x + dist z y
source
theorem dist_triangle_right {α : Type u} [pseudo_metric_space α] (x y z : α) :
dist x y ≤ dist x z + dist y z
source
theorem dist_triangle4 {α : Type u} [pseudo_metric_space α] (x y z w : α) :
dist x w ≤ dist x y + dist y z + dist z w
source
theorem dist_triangle4_left {α : Type u} [pseudo_metric_space α] (x₁ y₁ x₂ y₂ : α) :
dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
source
theorem dist_triangle4_right {α : Type u} [pseudo_metric_space α] (x₁ y₁ x₂ y₂ : α) :
dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
source
theorem dist_le_Ico_sum_dist {α : Type u} [pseudo_metric_space α] (f : ℕ → α) {m n : ℕ} (h : m ≤ n) :
dist (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.

source
theorem dist_le_range_sum_dist {α : Type u} [pseudo_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.

source
theorem dist_le_Ico_sum_of_dist_le {α : Type u} [pseudo_metric_space α] {f : ℕ → α} {m n : ℕ} (hmn : m ≤ n) {d : ℕ → ℝ} (hd : ∀ {k : ℕ}, m ≤ k → k < n → dist (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.

source
theorem dist_le_range_sum_of_dist_le {α : Type u} [pseudo_metric_space α] {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ} (hd : ∀ {k : ℕ}, k < n → dist (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.

source
theorem swap_dist {α : Type u} [pseudo_metric_space α] :
function.swap dist = dist
source
theorem abs_dist_sub_le {α : Type u} [pseudo_metric_space α] (x y z : α) :
|dist x z - dist y z| ≤ dist x y
source
theorem dist_nonneg {α : Type u} [pseudo_metric_space α] {x y : α} :
0 ≤ dist x y
source
@[simp]
theorem abs_dist {α : Type u} [pseudo_metric_space α] {a b : α} :
|dist a b| = dist a b
source
@[class]
structure has_nndist (α : Type u_1) :
Type u_1

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

Instances
source
@[protected, instance]
def pseudo_metric_space.to_has_nndist {α : Type u} [pseudo_metric_space α] :
has_nndist α

Distance as a nonnegative real number.

Equations
source
theorem nndist_edist {α : Type u} [pseudo_metric_space α] (x y : α) :
nndist x y = (edist x y).to_nnreal

Express nndist in terms of edist

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

Express edist in terms of nndist

source
@[simp, norm_cast]
theorem coe_nnreal_ennreal_nndist {α : Type u} [pseudo_metric_space α] (x y : α) :
↑(nndist x y) = edist x y
source
@[simp, norm_cast]
theorem edist_lt_coe {α : Type u} [pseudo_metric_space α] {x y : α} {c : ℝ≥0} :
edist x y < ↑c ↔ nndist x y < c
source
@[simp, norm_cast]
theorem edist_le_coe {α : Type u} [pseudo_metric_space α] {x y : α} {c : ℝ≥0} :
edist x y ≤ ↑c ↔ nndist x y ≤ c
source
theorem edist_lt_top {α : Type u_1} [pseudo_metric_space α] (x y : α) :
edist x y < ⊤

In a pseudometric space, the extended distance is always finite

source
theorem edist_ne_top {α : Type u} [pseudo_metric_space α] (x y : α) :
edist x y ≠ ⊤

In a pseudometric space, the extended distance is always finite

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

nndist x x vanishes

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

Express dist in terms of nndist

source
@[simp, norm_cast]
theorem coe_nndist {α : Type u} [pseudo_metric_space α] (x y : α) :
↑(nndist x y) = dist x y
source
@[simp, norm_cast]
theorem dist_lt_coe {α : Type u} [pseudo_metric_space α] {x y : α} {c : ℝ≥0} :
dist x y < ↑c ↔ nndist x y < c
source
@[simp, norm_cast]
theorem dist_le_coe {α : Type u} [pseudo_metric_space α] {x y : α} {c : ℝ≥0} :
dist x y ≤ ↑c ↔ nndist x y ≤ c
source
theorem nndist_dist {α : Type u} [pseudo_metric_space α] (x y : α) :
nndist x y = (dist x y).to_nnreal

Express nndist in terms of dist

source
theorem nndist_comm {α : Type u} [pseudo_metric_space α] (x y : α) :
nndist x y = nndist y x
source
theorem nndist_triangle {α : Type u} [pseudo_metric_space α] (x y z : α) :
nndist x z ≤ nndist x y + nndist y z

Triangle inequality for the nonnegative distance

source
theorem nndist_triangle_left {α : Type u} [pseudo_metric_space α] (x y z : α) :
nndist x y ≤ nndist z x + nndist z y
source
theorem nndist_triangle_right {α : Type u} [pseudo_metric_space α] (x y z : α) :
nndist x y ≤ nndist x z + nndist y z
source
theorem dist_edist {α : Type u} [pseudo_metric_space α] (x y : α) :
dist x y = (edist x y).to_real

Express dist in terms of edist

source
def metric.ball {α : Type u} [pseudo_metric_space α] (x : α) (ε : ℝ) :
set α

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

Equations
source
@[simp]
theorem metric.mem_ball {α : Type u} [pseudo_metric_space α] {x y : α} {ε : ℝ} :
y ∈ metric.ball x ε ↔ dist y x < ε
source
theorem metric.mem_ball' {α : Type u} [pseudo_metric_space α] {x y : α} {ε : ℝ} :
y ∈ metric.ball x ε ↔ dist x y < ε
source
theorem metric.pos_of_mem_ball {α : Type u} [pseudo_metric_space α] {x y : α} {ε : ℝ} (hy : y ∈ metric.ball x ε) :
0 < ε
source
theorem metric.mem_ball_self {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} (h : 0 < ε) :
x ∈ metric.ball x ε
source
@[simp]
theorem metric.nonempty_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
(metric.ball x ε).nonempty ↔ 0 < ε
source
@[simp]
theorem metric.ball_eq_empty {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
metric.ball x ε = ∅ ↔ ε ≤ 0
source
@[simp]
theorem metric.ball_zero {α : Type u} [pseudo_metric_space α] {x : α} :
metric.ball x 0 = ∅
source
theorem metric.ball_eq_ball {α : Type u} [pseudo_metric_space α] (ε : ℝ) (x : α) :
uniform_space.ball x {p : α × α | dist p.snd p.fst < ε} = metric.ball x ε
source
theorem metric.ball_eq_ball' {α : Type u} [pseudo_metric_space α] (ε : ℝ) (x : α) :
uniform_space.ball x {p : α × α | dist p.fst p.snd < ε} = metric.ball x ε
source
@[simp]
theorem metric.Union_ball_nat {α : Type u} [pseudo_metric_space α] (x : α) :
(⋃ (n : ℕ), metric.ball x ↑n) = set.univ
source
@[simp]
theorem metric.Union_ball_nat_succ {α : Type u} [pseudo_metric_space α] (x : α) :
(⋃ (n : ℕ), metric.ball x (↑n + 1)) = set.univ
source
def metric.closed_ball {α : Type u} [pseudo_metric_space α] (x : α) (ε : ℝ) :
set α

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

Equations
source
@[simp]
theorem metric.mem_closed_ball {α : Type u} [pseudo_metric_space α] {x y : α} {ε : ℝ} :
y ∈ metric.closed_ball x ε ↔ dist y x ≤ ε
source
def metric.sphere {α : Type u} [pseudo_metric_space α] (x : α) (ε : ℝ) :
set α

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

Equations
source
@[simp]
theorem metric.mem_sphere {α : Type u} [pseudo_metric_space α] {x y : α} {ε : ℝ} :
y ∈ metric.sphere x ε ↔ dist y x = ε
source
theorem metric.ne_of_mem_sphere {α : Type u} [pseudo_metric_space α] {x y : α} {ε : ℝ} (h : y ∈ metric.sphere x ε) (hε : ε ≠ 0) :
y ≠ x
source
theorem metric.sphere_eq_empty_of_subsingleton {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} [subsingleton α] (hε : ε ≠ 0) :
metric.sphere x ε = ∅
source
theorem metric.sphere_is_empty_of_subsingleton {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} [subsingleton α] (hε : ε ≠ 0) :
is_empty ↥(metric.sphere x ε)
source
theorem metric.mem_closed_ball' {α : Type u} [pseudo_metric_space α] {x y : α} {ε : ℝ} :
y ∈ metric.closed_ball x ε ↔ dist x y ≤ ε
source
theorem metric.mem_closed_ball_self {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} (h : 0 ≤ ε) :
x ∈ metric.closed_ball x ε
source
@[simp]
theorem metric.nonempty_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
(metric.closed_ball x ε).nonempty ↔ 0 ≤ ε
source
@[simp]
theorem metric.closed_ball_eq_empty {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
metric.closed_ball x ε = ∅ ↔ ε < 0
source
theorem metric.ball_subset_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
metric.ball x ε ⊆ metric.closed_ball x ε
source
theorem metric.sphere_subset_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
metric.sphere x ε ⊆ metric.closed_ball x ε
source
theorem metric.closed_ball_disjoint_ball {α : Type u} [pseudo_metric_space α] {x y : α} {δ ε : ℝ} (h : δ + ε ≤ dist x y) :
disjoint (metric.closed_ball x δ) (metric.ball y ε)
source
theorem metric.ball_disjoint_closed_ball {α : Type u} [pseudo_metric_space α] {x y : α} {δ ε : ℝ} (h : δ + ε ≤ dist x y) :
disjoint (metric.ball x δ) (metric.closed_ball y ε)
source
theorem metric.ball_disjoint_ball {α : Type u} [pseudo_metric_space α] {x y : α} {δ ε : ℝ} (h : δ + ε ≤ dist x y) :
disjoint (metric.ball x δ) (metric.ball y ε)
source
theorem metric.closed_ball_disjoint_closed_ball {α : Type u} [pseudo_metric_space α] {x y : α} {δ ε : ℝ} (h : δ + ε < dist x y) :
disjoint (metric.closed_ball x δ) (metric.closed_ball y ε)
source
theorem metric.sphere_disjoint_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
disjoint (metric.sphere x ε) (metric.ball x ε)
source
@[simp]
theorem metric.ball_union_sphere {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
metric.ball x ε ∪ metric.sphere x ε = metric.closed_ball x ε
source
@[simp]
theorem metric.sphere_union_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
metric.sphere x ε ∪ metric.ball x ε = metric.closed_ball x ε
source
@[simp]
theorem metric.closed_ball_diff_sphere {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
metric.closed_ball x ε \ metric.sphere x ε = metric.ball x ε
source
@[simp]
theorem metric.closed_ball_diff_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
metric.closed_ball x ε \ metric.ball x ε = metric.sphere x ε
source
theorem metric.mem_ball_comm {α : Type u} [pseudo_metric_space α] {x y : α} {ε : ℝ} :
x ∈ metric.ball y ε ↔ y ∈ metric.ball x ε
source
theorem metric.ball_subset_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) :
metric.ball x ε₁ ⊆ metric.ball x ε₂
source
theorem metric.ball_subset_ball' {α : Type u} [pseudo_metric_space α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) :
metric.ball x ε₁ ⊆ metric.ball y ε₂
source
theorem metric.closed_ball_subset_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) :
metric.closed_ball x ε₁ ⊆ metric.closed_ball x ε₂
source
theorem metric.closed_ball_subset_closed_ball' {α : Type u} [pseudo_metric_space α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) :
metric.closed_ball x ε₁ ⊆ metric.closed_ball y ε₂
source
theorem metric.closed_ball_subset_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ < ε₂) :
metric.closed_ball x ε₁ ⊆ metric.ball x ε₂
source
theorem metric.dist_le_add_of_nonempty_closed_ball_inter_closed_ball {α : Type u} [pseudo_metric_space α] {x y : α} {ε₁ ε₂ : ℝ} (h : (metric.closed_ball x ε₁ ∩ metric.closed_ball y ε₂).nonempty) :
dist x y ≤ ε₁ + ε₂
source
theorem metric.dist_lt_add_of_nonempty_closed_ball_inter_ball {α : Type u} [pseudo_metric_space α] {x y : α} {ε₁ ε₂ : ℝ} (h : (metric.closed_ball x ε₁ ∩ metric.ball y ε₂).nonempty) :
dist x y < ε₁ + ε₂
source
theorem metric.dist_lt_add_of_nonempty_ball_inter_closed_ball {α : Type u} [pseudo_metric_space α] {x y : α} {ε₁ ε₂ : ℝ} (h : (metric.ball x ε₁ ∩ metric.closed_ball y ε₂).nonempty) :
dist x y < ε₁ + ε₂
source
theorem metric.dist_lt_add_of_nonempty_ball_inter_ball {α : Type u} [pseudo_metric_space α] {x y : α} {ε₁ ε₂ : ℝ} (h : (metric.ball x ε₁ ∩ metric.ball y ε₂).nonempty) :
dist x y < ε₁ + ε₂
source
@[simp]
theorem metric.Union_closed_ball_nat {α : Type u} [pseudo_metric_space α] (x : α) :
(⋃ (n : ℕ), metric.closed_ball x ↑n) = set.univ
source
theorem metric.Union_inter_closed_ball_nat {α : Type u} [pseudo_metric_space α] (s : set α) (x : α) :
(⋃ (n : ℕ), s ∩ metric.closed_ball x ↑n) = s
source
theorem metric.ball_subset {α : Type u} [pseudo_metric_space α] {x y : α} {ε₁ ε₂ : ℝ} (h : dist x y ≤ ε₂ - ε₁) :
metric.ball x ε₁ ⊆ metric.ball y ε₂
source
theorem metric.ball_half_subset {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} (y : α) (h : y ∈ metric.ball x (ε / 2)) :
metric.ball y (ε / 2) ⊆ metric.ball x ε
source
theorem metric.exists_ball_subset_ball {α : Type u} [pseudo_metric_space α] {x y : α} {ε : ℝ} (h : y ∈ metric.ball x ε) :
∃ (ε' : ℝ) (H : ε' > 0), metric.ball y ε' ⊆ metric.ball x ε
source
theorem metric.forall_of_forall_mem_closed_ball {α : Type u} [pseudo_metric_space α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in filter.at_top, ∀ (y : α), y ∈ metric.closed_ball x R → 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.

source
theorem metric.forall_of_forall_mem_ball {α : Type u} [pseudo_metric_space α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in filter.at_top, ∀ (y : α), y ∈ metric.ball x 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.

source
theorem metric.uniformity_basis_dist {α : Type u} [pseudo_metric_space α] :
(𝓤 α).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {p : α × α | dist p.fst p.snd < ε})
source
@[protected]
theorem metric.mk_uniformity_basis {α : Type u} [pseudo_metric_space α] {β : Type u_1} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ (i : β), p i → 0 < 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.

source
theorem metric.uniformity_basis_dist_inv_nat_succ {α : Type u} [pseudo_metric_space α] :
(𝓤 α).has_basis (λ (_x : ℕ), true) (λ (n : ℕ), {p : α × α | dist p.fst p.snd < 1 / (↑n + 1)})
source
theorem metric.uniformity_basis_dist_inv_nat_pos {α : Type u} [pseudo_metric_space α] :
(𝓤 α).has_basis (λ (n : ℕ), 0 < n) (λ (n : ℕ), {p : α × α | dist p.fst p.snd < 1 / ↑n})
source
theorem metric.uniformity_basis_dist_pow {α : Type u} [pseudo_metric_space α] {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
(𝓤 α).has_basis (λ (n : ℕ), true) (λ (n : ℕ), {p : α × α | dist p.fst p.snd < r ^ n})
source
theorem metric.uniformity_basis_dist_lt {α : Type u} [pseudo_metric_space α] {R : ℝ} (hR : 0 < R) :
(𝓤 α).has_basis (λ (r : ℝ), 0 < r ∧ r < R) (λ (r : ℝ), {p : α × α | dist p.fst p.snd < r})
source
@[protected]
theorem metric.mk_uniformity_basis_le {α : Type u} [pseudo_metric_space α] {β : Type u_1} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ (x : β), p x → 0 < 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.

source
theorem metric.uniformity_basis_dist_le {α : Type u} [pseudo_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.

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

A constant size neighborhood of the diagonal is an entourage.

source
theorem metric.uniform_continuous_iff {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} :
uniform_continuous f ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε)
source
theorem metric.uniform_continuous_on_iff {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} {s : set α} :
uniform_continuous_on f s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist x y < δ → dist (f x) (f y) < ε)
source
theorem metric.uniform_continuous_on_iff_le {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} {s : set α} :
uniform_continuous_on f s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist x y ≤ δ → dist (f x) (f y) ≤ ε)
source
theorem metric.uniform_embedding_iff {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_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 < δ)
source
theorem metric.controlled_of_uniform_embedding {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_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 < δ))

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.

source
theorem metric.totally_bounded_iff {α : Type u} [pseudo_metric_space α] {s : set α} :
totally_bounded s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (t : set α), t.finite ∧ s ⊆ ⋃ (y : α) (H : y ∈ t), metric.ball y ε)
source
theorem metric.totally_bounded_of_finite_discretization {α : Type u} [pseudo_metric_space α] {s : set α} (H : ∀ (ε : ℝ), ε > 0 → (∃ (β : Type u) (_x : fintype β) (F : ↥s → β), ∀ (x y : ↥s), F x = F y → dist ↑x ↑y < ε)) :
totally_bounded s

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

source
theorem metric.finite_approx_of_totally_bounded {α : Type u} [pseudo_metric_space α] {s : set α} (hs : totally_bounded s) (ε : ℝ) (H : ε > 0) :
∃ (t : set α) (H : t ⊆ s), t.finite ∧ s ⊆ ⋃ (y : α) (H : y ∈ t), metric.ball y ε
source
theorem metric.tendsto_locally_uniformly_on_iff {α : Type u} {β : Type v} [pseudo_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 ∈ t → dist (f y) (F n y) < ε)

Expressing locally uniform convergence on a set using dist.

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

Expressing uniform convergence on a set using dist.

source
theorem metric.tendsto_locally_uniformly_iff {α : Type u} {β : Type v} [pseudo_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 ∈ t → dist (f y) (F n y) < ε

Expressing locally uniform convergence using dist.

source
theorem metric.tendsto_uniformly_iff {α : Type u} {β : Type v} [pseudo_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.

source
@[protected]
theorem metric.cauchy_iff {α : Type u} [pseudo_metric_space α] {f : filter α} :
cauchy f ↔ f.ne_bot ∧ ∀ (ε : ℝ), ε > 0 → (∃ (t : set α) (H : t ∈ f), ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → dist x y < ε)
source
theorem metric.nhds_basis_ball {α : Type u} [pseudo_metric_space α] {x : α} :
(𝓝 x).has_basis (λ (ε : ℝ), 0 < ε) (metric.ball x)
source
theorem metric.mem_nhds_iff {α : Type u} [pseudo_metric_space α] {x : α} {s : set α} :
s ∈ 𝓝 x ↔ ∃ (ε : ℝ) (H : ε > 0), metric.ball x ε ⊆ s
source
theorem metric.eventually_nhds_iff {α : Type u} [pseudo_metric_space α] {x : α} {p : α → Prop} :
(∀ᶠ (y : α) in 𝓝 x, p y) ↔ ∃ (ε : ℝ) (H : ε > 0), ∀ ⦃y : α⦄, dist y x < ε → p y
source
theorem metric.eventually_nhds_iff_ball {α : Type u} [pseudo_metric_space α] {x : α} {p : α → Prop} :
(∀ᶠ (y : α) in 𝓝 x, p y) ↔ ∃ (ε : ℝ) (H : ε > 0), ∀ (y : α), y ∈ metric.ball x ε → p y
source
theorem metric.nhds_basis_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} :
(𝓝 x).has_basis (λ (ε : ℝ), 0 < ε) (metric.closed_ball x)
source
theorem metric.nhds_basis_ball_inv_nat_succ {α : Type u} [pseudo_metric_space α] {x : α} :
(𝓝 x).has_basis (λ (_x : ℕ), true) (λ (n : ℕ), metric.ball x (1 / (↑n + 1)))
source
theorem metric.nhds_basis_ball_inv_nat_pos {α : Type u} [pseudo_metric_space α] {x : α} :
(𝓝 x).has_basis (λ (n : ℕ), 0 < n) (λ (n : ℕ), metric.ball x (1 / ↑n))
source
theorem metric.nhds_basis_ball_pow {α : Type u} [pseudo_metric_space α] {x : α} {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
(𝓝 x).has_basis (λ (n : ℕ), true) (λ (n : ℕ), metric.ball x (r ^ n))
source
theorem metric.nhds_basis_closed_ball_pow {α : Type u} [pseudo_metric_space α] {x : α} {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
(𝓝 x).has_basis (λ (n : ℕ), true) (λ (n : ℕ), metric.closed_ball x (r ^ n))
source
theorem metric.is_open_iff {α : Type u} [pseudo_metric_space α] {s : set α} :
is_open s ↔ ∀ (x : α), x ∈ s → (∃ (ε : ℝ) (H : ε > 0), metric.ball x ε ⊆ s)
source
theorem metric.is_open_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
is_open (metric.ball x ε)
source
theorem metric.ball_mem_nhds {α : Type u} [pseudo_metric_space α] (x : α) {ε : ℝ} (ε0 : 0 < ε) :
metric.ball x ε ∈ 𝓝 x
source
theorem metric.closed_ball_mem_nhds {α : Type u} [pseudo_metric_space α] (x : α) {ε : ℝ} (ε0 : 0 < ε) :
metric.closed_ball x ε ∈ 𝓝 x
source
theorem metric.closed_ball_mem_nhds_of_mem {α : Type u} [pseudo_metric_space α] {x c : α} {ε : ℝ} (h : x ∈ metric.ball c ε) :
metric.closed_ball c ε ∈ 𝓝 x
source
theorem metric.nhds_within_basis_ball {α : Type u} [pseudo_metric_space α] {x : α} {s : set α} :
(𝓝[s] x).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), metric.ball x ε ∩ s)
source
theorem metric.mem_nhds_within_iff {α : Type u} [pseudo_metric_space α] {x : α} {s t : set α} :
s ∈ 𝓝[t] x ↔ ∃ (ε : ℝ) (H : ε > 0), metric.ball x ε ∩ t ⊆ s
source
theorem metric.tendsto_nhds_within_nhds_within {α : Type u} {β : Type v} [pseudo_metric_space α] {s : set α} [pseudo_metric_space β] {t : set β} {f : α → β} {a : α} {b : β} :
filter.tendsto f (𝓝[s] a) (𝓝[t] b) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε)
source
theorem metric.tendsto_nhds_within_nhds {α : Type u} {β : Type v} [pseudo_metric_space α] {s : set α} [pseudo_metric_space β] {f : α → β} {a : α} {b : β} :
filter.tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) b < ε)
source
theorem metric.tendsto_nhds_nhds {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} {a : α} {b : β} :
filter.tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, dist x a < δ → dist (f x) b < ε)
source
theorem metric.continuous_at_iff {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} {a : α} :
continuous_at f a ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, dist x a < δ → dist (f x) (f a) < ε)
source
theorem metric.continuous_within_at_iff {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} {a : α} {s : set α} :
continuous_within_at f s a ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) (f a) < ε)
source
theorem metric.continuous_on_iff {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} {s : set α} :
continuous_on f s ↔ ∀ (b : α), b ∈ s → ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (a : α), a ∈ s → dist a b < δ → dist (f a) (f b) < ε)
source
theorem metric.continuous_iff {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {f : α → β} :
continuous f ↔ ∀ (b : α) (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (a : α), dist a b < δ → dist (f a) (f b) < ε)
source
theorem metric.tendsto_nhds {α : Type u} {β : Type v} [pseudo_metric_space α] {f : filter β} {u : β → α} {a : α} :
filter.tendsto u f (𝓝 a) ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in f, dist (u x) a < ε)
source
theorem metric.continuous_at_iff' {α : Type u} {β : Type v} [pseudo_metric_space α] [topological_space β] {f : β → α} {b : β} :
continuous_at f b ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε)
source
theorem metric.continuous_within_at_iff' {α : Type u} {β : Type v} [pseudo_metric_space α] [topological_space β] {f : β → α} {b : β} {s : set β} :
continuous_within_at f s b ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε)
source
theorem metric.continuous_on_iff' {α : Type u} {β : Type v} [pseudo_metric_space α] [topological_space β] {f : β → α} {s : set β} :
continuous_on f s ↔ ∀ (b : β), b ∈ s → ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε)
source
theorem metric.continuous_iff' {α : Type u} {β : Type v} [pseudo_metric_space α] [topological_space β] {f : β → α} :
continuous f ↔ ∀ (a : β) (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in 𝓝 a, dist (f x) (f a) < ε)
source
theorem metric.tendsto_at_top {α : Type u} {β : Type v} [pseudo_metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} {a : α} :
filter.tendsto u filter.at_top (𝓝 a) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : β), ∀ (n : β), n ≥ N → dist (u n) a < ε)
source
theorem metric.tendsto_at_top' {α : Type u} {β : Type v} [pseudo_metric_space α] [nonempty β] [semilattice_sup β] [no_max_order β] {u : β → α} {a : α} :
filter.tendsto u filter.at_top (𝓝 a) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : β), ∀ (n : β), n > N → dist (u n) a < ε)

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

source
theorem metric.is_open_singleton_iff {α : Type u_1} [pseudo_metric_space α] {x : α} :
is_open {x} ↔ ∃ (ε : ℝ) (H : ε > 0), ∀ (y : α), dist y x < ε → y = x
source
theorem metric.exists_ball_inter_eq_singleton_of_mem_discrete {α : Type u} [pseudo_metric_space α] {s : set α} [discrete_topology ↥s] {x : α} (hx : x ∈ s) :
∃ (ε : ℝ) (H : ε > 0), metric.ball x ε ∩ 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.

source
theorem metric.exists_closed_ball_inter_eq_singleton_of_discrete {α : Type u} [pseudo_metric_space α] {s : set α} [discrete_topology ↥s] {x : α} (hx : x ∈ s) :
∃ (ε : ℝ) (H : ε > 0), metric.closed_ball x ε ∩ 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.

source
theorem dense.exists_dist_lt {α : Type u} [pseudo_metric_space α] {s : set α} (hs : dense s) (x : α) {ε : ℝ} (hε : 0 < ε) :
∃ (y : α) (H : y ∈ s), dist x y < ε
source
theorem dense_range.exists_dist_lt {α : Type u} [pseudo_metric_space α] {β : Type u_1} {f : β → α} (hf : dense_range f) (x : α) {ε : ℝ} (hε : 0 < ε) :
∃ (y : β), dist x (f y) < ε
source
@[protected]
theorem pseudo_metric.uniformity_basis_edist {α : Type u} [pseudo_metric_space α] :
(𝓤 α).has_basis (λ (ε : ℝ≥0∞), 0 < ε) (λ (ε : ℝ≥0∞), {p : α × α | edist p.fst p.snd < ε})

Expressing the uniformity in terms of edist

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

A pseudometric space induces a pseudoemetric space

Equations
source
theorem metric.eball_top_eq_univ {α : Type u} [pseudo_metric_space α] (x : α) :
emetric.ball x ⊤ = set.univ

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

source
@[simp]
theorem metric.emetric_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
emetric.ball x (ennreal.of_real ε) = metric.ball x ε

Balls defined using the distance or the edistance coincide

source
@[simp]
theorem metric.emetric_ball_nnreal {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ≥0} :
emetric.ball x ↑ε = metric.ball x ↑ε

Balls defined using the distance or the edistance coincide

source
theorem metric.emetric_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} (h : 0 ≤ ε) :
emetric.closed_ball x (ennreal.of_real ε) = metric.closed_ball x ε

Closed balls defined using the distance or the edistance coincide

source
@[simp]
theorem metric.emetric_closed_ball_nnreal {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ≥0} :
emetric.closed_ball x ↑ε = metric.closed_ball x ↑ε

Closed balls defined using the distance or the edistance coincide

source
@[simp]
theorem metric.emetric_ball_top {α : Type u} [pseudo_metric_space α] (x : α) :
emetric.ball x ⊤ = set.univ
source
def pseudo_metric_space.replace_uniformity {α : Type u_1} [U : uniform_space α] (m : pseudo_metric_space α) (H : 𝓤 α = 𝓤 α) :
pseudo_metric_space α

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
source
theorem pseudo_metric_space.replace_uniformity_eq {α : Type u_1} [U : uniform_space α] (m : pseudo_metric_space α) (H : 𝓤 α = 𝓤 α) :
m.replace_uniformity H = m
source
def pseudo_emetric_space.to_pseudo_metric_space_of_dist {α : Type u} [e : pseudo_emetric_space α] (dist : α → α → ℝ) (edist_ne_top : ∀ (x y : α), edist x y ≠ ⊤) (h : ∀ (x y : α), dist x y = (edist x y).to_real) :
pseudo_metric_space α

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
source
def pseudo_emetric_space.to_pseudo_metric_space {α : Type u} [e : pseudo_emetric_space α] (h : ∀ (x y : α), edist x y ≠ ⊤) :
pseudo_metric_space α

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
source
theorem metric.complete_of_convergent_controlled_sequences {α : Type u} [pseudo_metric_space α] (B : ℕ → ℝ) (hB : ∀ (n : ℕ), 0 < B n) (H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (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.

source
theorem metric.complete_of_cauchy_seq_tendsto {α : Type u} [pseudo_metric_space α] :
(∀ (u : ℕ → α), cauchy_seq u → (∃ (a : α), filter.tendsto u filter.at_top (𝓝 a))) → complete_space α
source
@[protected, instance]
noncomputable def real.pseudo_metric_space  :
pseudo_metric_space ℝ

Instantiate the reals as a pseudometric space.

Equations
source
theorem real.dist_eq (x y : ℝ) :
dist x y = |x - y|
source
theorem real.nndist_eq (x y : ℝ) :
nndist x y = ⇑real.nnabs (x - y)
source
theorem real.nndist_eq' (x y : ℝ) :
nndist x y = ⇑real.nnabs (y - x)
source
theorem real.dist_0_eq_abs (x : ℝ) :
dist x 0 = |x|
source
theorem real.dist_left_le_of_mem_interval {x y z : ℝ} (h : y ∈ [x, z]) :
dist x y ≤ dist x z
source
theorem real.dist_right_le_of_mem_interval {x y z : ℝ} (h : y ∈ [x, z]) :
dist y z ≤ dist x z
source
theorem real.dist_le_of_mem_interval {x y x' y' : ℝ} (hx : x ∈ [x', y']) (hy : y ∈ [x', y']) :
dist x y ≤ dist x' y'
source
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 ≤ y' - x'
source
theorem real.dist_le_of_mem_Icc_01 {x y : ℝ} (hx : x ∈ set.Icc 0 1) (hy : y ∈ set.Icc 0 1) :
dist x y ≤ 1
source
@[protected, instance]
def real.order_topology  :
order_topology ℝ
source
theorem real.ball_eq_Ioo (x r : ℝ) :
metric.ball x r = set.Ioo (x - r) (x + r)
source
theorem real.closed_ball_eq_Icc {x r : ℝ} :
metric.closed_ball x r = set.Icc (x - r) (x + r)
source
theorem real.Ioo_eq_ball (x y : ℝ) :
set.Ioo x y = metric.ball ((x + y) / 2) ((y - x) / 2)
source
theorem real.Icc_eq_closed_ball (x y : ℝ) :
set.Icc x y = metric.closed_ball ((x + y) / 2) ((y - x) / 2)
source
theorem totally_bounded_Icc {α : Type u} [pseudo_metric_space α] [preorder α] [compact_Icc_space α] (a b : α) :
totally_bounded (set.Icc a b)
source
theorem totally_bounded_Ico {α : Type u} [pseudo_metric_space α] [preorder α] [compact_Icc_space α] (a b : α) :
totally_bounded (set.Ico a b)
source
theorem totally_bounded_Ioc {α : Type u} [pseudo_metric_space α] [preorder α] [compact_Icc_space α] (a b : α) :
totally_bounded (set.Ioc a b)
source
theorem totally_bounded_Ioo {α : Type u} [pseudo_metric_space α] [preorder α] [compact_Icc_space α] (a b : α) :
totally_bounded (set.Ioo a b)
source
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 : 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.

source
theorem squeeze_zero {α : Type u_1} {f g : α → ℝ} {t₀ : filter α} (hf : ∀ (t : α), 0 ≤ f t) (hft : ∀ (t : α), f t ≤ g t) (g0 : 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.

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

Alias of filter.tendsto.congr_dist.

source
theorem tendsto_iff_of_dist {α : Type u} [pseudo_metric_space α] {ι : Type u_1} {f₁ f₂ : ι → α} {p : filter ι} {a : α} (h : filter.tendsto (λ (x : ι), dist (f₁ x) (f₂ x)) p (𝓝 0)) :
filter.tendsto f₁ p (𝓝 a) ↔ filter.tendsto f₂ p (𝓝 a)
source
theorem eventually_closed_ball_subset {α : Type u} [pseudo_metric_space α] {x : α} {u : set α} (hu : u ∈ 𝓝 x) :
∀ᶠ (r : ℝ) in 𝓝 0, metric.closed_ball x r ⊆ u

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

source
@[nolint]
theorem metric.cauchy_seq_iff {α : Type u} {β : Type v} [pseudo_metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :
cauchy_seq u ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : β), ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → 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

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

A variation around the pseudometric characterization of Cauchy sequences

source
theorem cauchy_seq_of_le_tendsto_0' {α : Type u} {β : Type v} [pseudo_metric_space α] [nonempty β] [semilattice_sup β] {s : β → α} (b : β → ℝ) (h : ∀ (n m : β), n ≤ m → dist (s n) (s m) ≤ b n) (h₀ : filter.tendsto b filter.at_top (𝓝 0)) :
cauchy_seq s

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.

source
theorem cauchy_seq_of_le_tendsto_0 {α : Type u} {β : Type v} [pseudo_metric_space α] [nonempty β] [semilattice_sup β] {s : β → α} (b : β → ℝ) (h : ∀ (n m N : β), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) (h₀ : 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.

source
theorem cauchy_seq_bdd {α : Type u} [pseudo_metric_space α] {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.

source
theorem cauchy_seq_iff_le_tendsto_0 {α : Type u} [pseudo_metric_space α] {s : ℕ → α} :
cauchy_seq s ↔ ∃ (b : ℕ → ℝ), (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (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.

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

Pseudometric space structure pulled back by a function.

Equations
source
def uniform_inducing.comap_pseudo_metric_space {α : Type u_1} {β : Type u_2} [uniform_space α] [pseudo_metric_space β] (f : α → β) (h : uniform_inducing f) :
pseudo_metric_space α

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
source
@[protected, instance]
def subtype.pseudo_metric_space {α : Type u} [pseudo_metric_space α] {p : α → Prop} :
pseudo_metric_space (subtype p)
Equations
source
theorem subtype.dist_eq {α : Type u} [pseudo_metric_space α] {p : α → Prop} (x y : subtype p) :
dist x y = dist ↑x ↑y
source
theorem subtype.nndist_eq {α : Type u} [pseudo_metric_space α] {p : α → Prop} (x y : subtype p) :
nndist x y = nndist ↑x ↑y
source
@[protected, instance]
def add_opposite.pseudo_metric_space {α : Type u} [pseudo_metric_space α] :
pseudo_metric_space αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.pseudo_metric_space {α : Type u} [pseudo_metric_space α] :
pseudo_metric_space αᵐᵒᵖ
Equations
source
@[simp]
theorem mul_opposite.dist_unop {α : Type u} [pseudo_metric_space α] (x y : αᵐᵒᵖ) :
dist (mul_opposite.unop x) (mul_opposite.unop y) = dist x y
source
@[simp]
theorem add_opposite.dist_unop {α : Type u} [pseudo_metric_space α] (x y : αᵃᵒᵖ) :
dist (add_opposite.unop x) (add_opposite.unop y) = dist x y
source
@[simp]
theorem mul_opposite.dist_op {α : Type u} [pseudo_metric_space α] (x y : α) :
dist (mul_opposite.op x) (mul_opposite.op y) = dist x y
source
@[simp]
theorem add_opposite.dist_op {α : Type u} [pseudo_metric_space α] (x y : α) :
dist (add_opposite.op x) (add_opposite.op y) = dist x y
source
@[simp]
theorem add_opposite.nndist_unop {α : Type u} [pseudo_metric_space α] (x y : αᵃᵒᵖ) :
nndist (add_opposite.unop x) (add_opposite.unop y) = nndist x y
source
@[simp]
theorem mul_opposite.nndist_unop {α : Type u} [pseudo_metric_space α] (x y : αᵐᵒᵖ) :
nndist (mul_opposite.unop x) (mul_opposite.unop y) = nndist x y
source
@[simp]
theorem mul_opposite.nndist_op {α : Type u} [pseudo_metric_space α] (x y : α) :
nndist (mul_opposite.op x) (mul_opposite.op y) = nndist x y
source
@[simp]
theorem add_opposite.nndist_op {α : Type u} [pseudo_metric_space α] (x y : α) :
nndist (add_opposite.op x) (add_opposite.op y) = nndist x y
source
@[protected, instance]
noncomputable def nnreal.pseudo_metric_space  :
pseudo_metric_space ℝ≥0
Equations
source
theorem nnreal.dist_eq (a b : ℝ≥0) :
dist a b = |↑a - ↑b|
source
theorem nnreal.nndist_eq (a b : ℝ≥0) :
nndist a b = max (a - b) (b - a)
source
@[simp]
theorem nnreal.nndist_zero_eq_val (z : ℝ≥0) :
nndist 0 z = z
source
@[simp]
theorem nnreal.nndist_zero_eq_val' (z : ℝ≥0) :
nndist z 0 = z
source
theorem nnreal.le_add_nndist (a b : ℝ≥0) :
a ≤ b + nndist a b
source
@[protected, instance]
noncomputable def prod.pseudo_metric_space_max {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] :
pseudo_metric_space (α × β)
Equations
source
theorem prod.dist_eq {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {x y : α × β} :
dist x y = max (dist x.fst y.fst) (dist x.snd y.snd)
source
@[simp]
theorem dist_prod_same_left {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {x : α} {y₁ y₂ : β} :
dist (x, y₁) (x, y₂) = dist y₁ y₂
source
@[simp]
theorem dist_prod_same_right {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {x₁ x₂ : α} {y : β} :
dist (x₁, y) (x₂, y) = dist x₁ x₂
source
theorem ball_prod_same {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] (x : α) (y : β) (r : ℝ) :
metric.ball x r ×ˢ metric.ball y r = metric.ball (x, y) r
source
theorem closed_ball_prod_same {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] (x : α) (y : β) (r : ℝ) :
metric.closed_ball x r ×ˢ metric.closed_ball y r = metric.closed_ball (x, y) r
source
theorem uniform_continuous_dist {α : Type u} [pseudo_metric_space α] :
uniform_continuous (λ (p : α × α), dist p.fst p.snd)
source
theorem uniform_continuous.dist {α : Type u} {β : Type v} [pseudo_metric_space α] [uniform_space β] {f g : β → α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (b : β), dist (f b) (g b))
source
@[continuity]
theorem continuous_dist {α : Type u} [pseudo_metric_space α] :
continuous (λ (p : α × α), dist p.fst p.snd)
source
@[continuity]
theorem continuous.dist {α : Type u} {β : Type v} [pseudo_metric_space α] [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), dist (f b) (g b))
source
theorem filter.tendsto.dist {α : Type u} {β : Type v} [pseudo_metric_space α] {f g : β → α} {x : filter β} {a b : α} (hf : filter.tendsto f x (𝓝 a)) (hg : filter.tendsto g x (𝓝 b)) :
filter.tendsto (λ (x : β), dist (f x) (g x)) x (𝓝 (dist a b))
source
theorem nhds_comap_dist {α : Type u} [pseudo_metric_space α] (a : α) :
filter.comap (λ (a' : α), dist a' a) (𝓝 0) = 𝓝 a
source
theorem tendsto_iff_dist_tendsto_zero {α : Type u} {β : Type v} [pseudo_metric_space α] {f : β → α} {x : filter β} {a : α} :
filter.tendsto f x (𝓝 a) ↔ filter.tendsto (λ (b : β), dist (f b) a) x (𝓝 0)
source
theorem uniform_continuous_nndist {α : Type u} [pseudo_metric_space α] :
uniform_continuous (λ (p : α × α), nndist p.fst p.snd)
source
theorem uniform_continuous.nndist {α : Type u} {β : Type v} [pseudo_metric_space α] [uniform_space β] {f g : β → α} (hf : uniform_continuous f) (hg : uniform_continuous g) :
uniform_continuous (λ (b : β), nndist (f b) (g b))
source
theorem continuous_nndist {α : Type u} [pseudo_metric_space α] :
continuous (λ (p : α × α), nndist p.fst p.snd)
source
theorem continuous.nndist {α : Type u} {β : Type v} [pseudo_metric_space α] [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), nndist (f b) (g b))
source
theorem filter.tendsto.nndist {α : Type u} {β : Type v} [pseudo_metric_space α] {f g : β → α} {x : filter β} {a b : α} (hf : filter.tendsto f x (𝓝 a)) (hg : filter.tendsto g x (𝓝 b)) :
filter.tendsto (λ (x : β), nndist (f x) (g x)) x (𝓝 (nndist a b))
source
theorem metric.is_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
is_closed (metric.closed_ball x ε)
source
theorem metric.is_closed_sphere {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
is_closed (metric.sphere x ε)
source
@[simp]
theorem metric.closure_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
closure (metric.closed_ball x ε) = metric.closed_ball x ε
source
theorem metric.closure_ball_subset_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
closure (metric.ball x ε) ⊆ metric.closed_ball x ε
source
theorem metric.frontier_ball_subset_sphere {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
frontier (metric.ball x ε) ⊆ metric.sphere x ε
source
theorem metric.frontier_closed_ball_subset_sphere {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
frontier (metric.closed_ball x ε) ⊆ metric.sphere x ε
source
theorem metric.ball_subset_interior_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {ε : ℝ} :
metric.ball x ε ⊆ interior (metric.closed_ball x ε)
source
theorem metric.mem_closure_iff {α : Type u} [pseudo_metric_space α] {s : set α} {a : α} :
a ∈ closure s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (b : α) (H : b ∈ s), dist a b < ε)

ε-characterization of the closure in pseudometric spaces

source
theorem metric.mem_closure_range_iff {α : Type u} {β : Type v} [pseudo_metric_space α] {e : β → α} {a : α} :
a ∈ closure (set.range e) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (k : β), dist a (e k) < ε)
source
theorem metric.mem_closure_range_iff_nat {α : Type u} {β : Type v} [pseudo_metric_space α] {e : β → α} {a : α} :
a ∈ closure (set.range e) ↔ ∀ (n : ℕ), ∃ (k : β), dist a (e k) < 1 / (↑n + 1)
source
theorem metric.mem_of_closed' {α : Type u} [pseudo_metric_space α] {s : set α} (hs : is_closed s) {a : α} :
a ∈ s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (b : α) (H : b ∈ s), dist a b < ε)
source
theorem metric.closed_ball_zero' {α : Type u} [pseudo_metric_space α] (x : α) :
metric.closed_ball x 0 = closure {x}
source
theorem metric.dense_iff {α : Type u} [pseudo_metric_space α] {s : set α} :
dense s ↔ ∀ (x : α) (r : ℝ), r > 0 → (metric.ball x r ∩ s).nonempty
source
theorem metric.dense_range_iff {α : Type u} {β : Type v} [pseudo_metric_space α] {f : β → α} :
dense_range f ↔ ∀ (x : α) (r : ℝ), r > 0 → (∃ (y : β), dist x (f y) < r)
source
theorem topological_space.is_separable.separable_space {α : Type u} [pseudo_metric_space α] {s : set α} (hs : topological_space.is_separable s) :
topological_space.separable_space ↥s

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.

source
@[protected]
theorem inducing.is_separable_preimage {α : Type u} {β : Type v} [pseudo_metric_space α] {f : β → α} [topological_space β] (hf : inducing f) {s : set α} (hs : topological_space.is_separable s) :
topological_space.is_separable (f ⁻¹' s)

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

source
@[protected]
theorem embedding.is_separable_preimage {α : Type u} {β : Type v} [pseudo_metric_space α] {f : β → α} [topological_space β] (hf : embedding f) {s : set α} (hs : topological_space.is_separable s) :
topological_space.is_separable (f ⁻¹' s)
source
theorem continuous_on.is_separable_image {α : Type u} {β : Type v} [pseudo_metric_space α] [topological_space β] {f : α → β} {s : set α} (hf : continuous_on f s) (hs : topological_space.is_separable s) :
topological_space.is_separable (f '' s)

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

source
@[protected, instance]
noncomputable 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
source
theorem nndist_pi_def {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (f g : Π (b : β), π b) :
nndist f g = finset.univ.sup (λ (b : β), nndist (f b) (g b))
source
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)))
source
@[simp]
theorem dist_pi_const {α : Type u} {β : Type v} [pseudo_metric_space α] [fintype β] [nonempty β] (a b : α) :
dist (λ (x : β), a) (λ (_x : β), b) = dist a b
source
@[simp]
theorem nndist_pi_const {α : Type u} {β : Type v} [pseudo_metric_space α] [fintype β] [nonempty β] (a b : α) :
nndist (λ (x : β), a) (λ (_x : β), b) = nndist a b
source
theorem nndist_pi_le_iff {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space (π b)] {f g : Π (b : β), π b} {r : ℝ≥0} :
nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r
source
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
source
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
source
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) ≤ nndist f g
source
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
source
theorem ball_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (x : Π (b : β), π b) {r : ℝ} (hr : 0 < r) :
metric.ball x 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.

source
theorem ball_pi' {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space (π b)] [nonempty β] (x : Π (b : β), π b) (r : ℝ) :
metric.ball x 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 β.

source
theorem closed_ball_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space (π b)] (x : Π (b : β), π b) {r : ℝ} (hr : 0 ≤ r) :
metric.closed_ball x 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.

source
theorem closed_ball_pi' {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), pseudo_metric_space (π b)] [nonempty β] (x : Π (b : β), π b) (r : ℝ) :
metric.closed_ball x 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 β.

source
@[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)) :
nndist (i.insert_nth x f) (i.insert_nth y g) = max (nndist x y) (nndist f g)
source
@[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)) :
dist (i.insert_nth x f) (i.insert_nth y g) = max (dist x y) (dist f g)
source
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') :
dist x y ≤ dist x' y'
source
theorem finite_cover_balls_of_compact {α : Type u} [pseudo_metric_space α] {s : set α} (hs : is_compact s) {e : ℝ} (he : 0 < e) :
∃ (t : set α) (H : t ⊆ s), t.finite ∧ s ⊆ ⋃ (x : α) (H : x ∈ t), metric.ball x e

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

source
theorem is_compact.finite_cover_balls {α : Type u} [pseudo_metric_space α] {s : set α} (hs : is_compact s) {e : ℝ} (he : 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.

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

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

Instances
source
theorem is_compact_sphere {α : Type u_1} [pseudo_metric_space α] [proper_space α] (x : α) (r : ℝ) :
is_compact (metric.sphere x r)

In a proper pseudometric space, all spheres are compact.

source
@[protected, instance]
def metric.sphere.compact_space {α : Type u_1} [pseudo_metric_space α] [proper_space α] (x : α) (r : ℝ) :
compact_space ↥(metric.sphere x r)

In a proper pseudometric space, any sphere is a compact_space when considered as a subtype.

source
@[protected, instance]
def second_countable_of_proper {α : Type u} [pseudo_metric_space α] [proper_space α] :
topological_space.second_countable_topology α

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

source
theorem tendsto_dist_right_cocompact_at_top {α : Type u} [pseudo_metric_space α] [proper_space α] (x : α) :
filter.tendsto (λ (y : α), dist y x) (filter.cocompact α) filter.at_top
source
theorem tendsto_dist_left_cocompact_at_top {α : Type u} [pseudo_metric_space α] [proper_space α] (x : α) :
filter.tendsto (dist x) (filter.cocompact α) filter.at_top
source
theorem proper_space_of_compact_closed_ball_of_le {α : Type u} [pseudo_metric_space α] (R : ℝ) (h : ∀ (x : α) (r : ℝ), R ≤ r → is_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.

source
@[protected, instance]
def proper_of_compact {α : Type u} [pseudo_metric_space α] [compact_space α] :
proper_space α
source
@[protected, instance]
def locally_compact_of_proper {α : Type u} [pseudo_metric_space α] [proper_space α] :
locally_compact_space α

A proper space is locally compact

source
@[protected, instance]
def complete_of_proper {α : Type u} [pseudo_metric_space α] [proper_space α] :
complete_space α

A proper space is complete

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

source
theorem exists_pos_lt_subset_ball {α : Type u} [pseudo_metric_space α] [proper_space α] {x : α} {r : ℝ} {s : set α} (hr : 0 < r) (hs : is_closed s) (h : s ⊆ metric.ball x r) :
∃ (r' : ℝ) (H : r' ∈ set.Ioo 0 r), s ⊆ metric.ball x 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.

source
theorem exists_lt_subset_ball {α : Type u} [pseudo_metric_space α] [proper_space α] {x : α} {r : ℝ} {s : set α} (hs : is_closed s) (h : s ⊆ metric.ball x r) :
∃ (r' : ℝ) (H : r' < r), s ⊆ metric.ball x 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.

source
theorem is_compact.is_separable {α : Type u} [pseudo_metric_space α] {s : set α} (hs : is_compact s) :
topological_space.is_separable s
source
theorem metric.second_countable_of_almost_dense_set {α : Type u} [pseudo_metric_space α] (H : ∀ (ε : ℝ), ε > 0 → (∃ (s : set α), s.countable ∧ ∀ (x : α), ∃ (y : α) (H : y ∈ s), dist x y ≤ ε)) :
topological_space.second_countable_topology α

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

source
theorem lebesgue_number_lemma_of_metric {α : Type u} [pseudo_metric_space α] {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 : ι), metric.ball x δ ⊆ c i)
source
theorem lebesgue_number_lemma_of_metric_sUnion {α : Type u} [pseudo_metric_space α] {s : set α} {c : set (set α)} (hs : is_compact s) (hc₁ : ∀ (t : set α), t ∈ c → is_open t) (hc₂ : s ⊆ ⋃₀c) :
∃ (δ : ℝ) (H : δ > 0), ∀ (x : α), x ∈ s → (∃ (t : set α) (H : t ∈ c), metric.ball x δ ⊆ t)
source
def metric.bounded {α : Type u} [pseudo_metric_space α] (s : set α) :
Prop

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

Equations
source
@[simp]
theorem metric.bounded_empty {α : Type u} [pseudo_metric_space α] :
metric.bounded ∅
source
theorem metric.bounded_iff_mem_bounded {α : Type u} [pseudo_metric_space α] {s : set α} :
metric.bounded s ↔ ∀ (x : α), x ∈ s → metric.bounded s
source
theorem metric.bounded.mono {α : Type u} [pseudo_metric_space α] {s t : set α} (incl : s ⊆ t) :
metric.bounded t → metric.bounded s

Subsets of a bounded set are also bounded

source
theorem metric.bounded_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {r : ℝ} :
metric.bounded (metric.closed_ball x r)

Closed balls are bounded

source
theorem metric.bounded_ball {α : Type u} [pseudo_metric_space α] {x : α} {r : ℝ} :
metric.bounded (metric.ball x r)

Open balls are bounded

source
theorem metric.bounded_sphere {α : Type u} [pseudo_metric_space α] {x : α} {r : ℝ} :
metric.bounded (metric.sphere x r)

Spheres are bounded

source
theorem metric.bounded_iff_subset_ball {α : Type u} [pseudo_metric_space α] {s : set α} (c : α) :
metric.bounded s ↔ ∃ (r : ℝ), s ⊆ metric.closed_ball c r

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

source
theorem metric.bounded.subset_ball {α : Type u} [pseudo_metric_space α] {s : set α} (h : metric.bounded s) (c : α) :
∃ (r : ℝ), s ⊆ metric.closed_ball c r
source
theorem metric.bounded.subset_ball_lt {α : Type u} [pseudo_metric_space α] {s : set α} (h : metric.bounded s) (a : ℝ) (c : α) :
∃ (r : ℝ), a < r ∧ s ⊆ metric.closed_ball c r
source
theorem metric.bounded_closure_of_bounded {α : Type u} [pseudo_metric_space α] {s : set α} (h : metric.bounded s) :
metric.bounded (closure s)
source
theorem metric.bounded.closure {α : Type u} [pseudo_metric_space α] {s : set α} (h : metric.bounded s) :
metric.bounded (closure s)

Alias of bounded_closure_of_bounded.

source
@[simp]
theorem metric.bounded_closure_iff {α : Type u} [pseudo_metric_space α] {s : set α} :
metric.bounded (closure s) ↔ metric.bounded s
source
theorem metric.bounded.union {α : Type u} [pseudo_metric_space α] {s t : set α} (hs : metric.bounded s) (ht : metric.bounded t) :
metric.bounded (s ∪ t)

The union of two bounded sets is bounded.

source
@[simp]
theorem metric.bounded_union {α : Type u} [pseudo_metric_space α] {s t : set α} :
metric.bounded (s ∪ t) ↔ metric.bounded s ∧ metric.bounded t

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

source
theorem metric.bounded_bUnion {α : Type u} {β : Type v} [pseudo_metric_space α] {I : set β} {s : β → set α} (H : I.finite) :
metric.bounded (⋃ (i : β) (H : i ∈ I), s i) ↔ ∀ (i : β), i ∈ I → metric.bounded (s i)

A finite union of bounded sets is bounded

source
@[protected]
theorem metric.bounded.prod {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β] {s : set α} {t : set β} (hs : metric.bounded s) (ht : metric.bounded t) :
metric.bounded (s ×ˢ t)
source
theorem totally_bounded.bounded {α : Type u} [pseudo_metric_space α] {s : set α} (h : totally_bounded s) :
metric.bounded s

A totally bounded set is bounded

source
theorem is_compact.bounded {α : Type u} [pseudo_metric_space α] {s : set α} (h : is_compact s) :
metric.bounded s

A compact set is bounded

source
theorem metric.bounded_of_finite {α : Type u} [pseudo_metric_space α] {s : set α} (h : s.finite) :
metric.bounded s

A finite set is bounded

source
theorem set.finite.bounded {α : Type u} [pseudo_metric_space α] {s : set α} (h : s.finite) :
metric.bounded s

Alias of bounded_of_finite.

source
theorem metric.bounded_singleton {α : Type u} [pseudo_metric_space α] {x : α} :
metric.bounded {x}

A singleton is bounded

source
theorem metric.bounded_range_iff {α : Type u} {β : Type v} [pseudo_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

source
theorem metric.bounded_range_of_tendsto_cofinite_uniformity {α : Type u} {β : Type v} [pseudo_metric_space α] {f : β → α} (hf : filter.tendsto (prod.map f f) (filter.cofinite ×ᶠ filter.cofinite) (𝓤 α)) :
metric.bounded (set.range f)
source
theorem metric.bounded_range_of_cauchy_map_cofinite {α : Type u} {β : Type v} [pseudo_metric_space α] {f : β → α} (hf : cauchy (filter.map f filter.cofinite)) :
metric.bounded (set.range f)
source
theorem cauchy_seq.bounded_range {α : Type u} [pseudo_metric_space α] {f : ℕ → α} (hf : cauchy_seq f) :
metric.bounded (set.range f)
source
theorem metric.bounded_range_of_tendsto_cofinite {α : Type u} {β : Type v} [pseudo_metric_space α] {f : β → α} {a : α} (hf : filter.tendsto f filter.cofinite (𝓝 a)) :
metric.bounded (set.range f)
source
theorem metric.bounded_of_compact_space {α : Type u} [pseudo_metric_space α] {s : set α} [compact_space α] :
metric.bounded s

In a compact space, all sets are bounded

source
theorem metric.bounded_range_of_tendsto {α : Type u_1} [pseudo_metric_space α] (u : ℕ → α) {x : α} (hu : filter.tendsto u filter.at_top (𝓝 x)) :
metric.bounded (set.range u)
source
theorem metric.is_compact_of_is_closed_bounded {α : Type u} [pseudo_metric_space α] {s : set α} [proper_space α] (hc : is_closed s) (hb : metric.bounded s) :
is_compact s

The Heine–Borel theorem: In a proper space, a closed bounded set is compact.

source
theorem metric.bounded.is_compact_closure {α : Type u} [pseudo_metric_space α] {s : set α} [proper_space α] (h : metric.bounded s) :
is_compact (closure s)

The Heine–Borel theorem: In a proper space, the closure of a bounded set is compact.

source
theorem metric.compact_iff_closed_bounded {α : Type u} [pseudo_metric_space α] {s : set α} [t2_space α] [proper_space α] :
is_compact s ↔ is_closed s ∧ metric.bounded s

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

source
theorem metric.compact_space_iff_bounded_univ {α : Type u} [pseudo_metric_space α] [proper_space α] :
compact_space α ↔ metric.bounded set.univ
source
theorem metric.bounded_Icc {α : Type u} [pseudo_metric_space α] [preorder α] [compact_Icc_space α] (a b : α) :
metric.bounded (set.Icc a b)
source
theorem metric.bounded_Ico {α : Type u} [pseudo_metric_space α] [preorder α] [compact_Icc_space α] (a b : α) :
metric.bounded (set.Ico a b)
source
theorem metric.bounded_Ioc {α : Type u} [pseudo_metric_space α] [preorder α] [compact_Icc_space α] (a b : α) :
metric.bounded (set.Ioc a b)
source
theorem metric.bounded_Ioo {α : Type u} [pseudo_metric_space α] [preorder α] [compact_Icc_space α] (a b : α) :
metric.bounded (set.Ioo a b)
source
theorem metric.bounded_of_bdd_above_of_bdd_below {α : Type u} [pseudo_metric_space α] [preorder α] [compact_Icc_space α] {s : set α} (h₁ : bdd_above s) (h₂ : bdd_below s) :
metric.bounded s

In a pseudo metric space with a conditionally complete linear order such that the order and the metric structure give the same topology, any order-bounded set is metric-bounded.

source
noncomputable def metric.diam {α : Type u} [pseudo_metric_space α] (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
source
theorem metric.diam_nonneg {α : Type u} [pseudo_metric_space α] {s : set α} :
0 ≤ metric.diam s

The diameter of a set is always nonnegative

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

The empty set has zero diameter

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

A singleton has zero diameter

source
theorem metric.diam_pair {α : Type u} [pseudo_metric_space α] {x y : α} :
metric.diam {x, y} = dist x y
source
theorem metric.diam_triple {α : Type u} [pseudo_metric_space α] {x y z : α} :
metric.diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)
source
theorem metric.ediam_le_of_forall_dist_le {α : Type u} [pseudo_metric_space α] {s : set α} {C : ℝ} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist 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.

source
theorem metric.diam_le_of_forall_dist_le {α : Type u} [pseudo_metric_space α] {s : set α} {C : ℝ} (h₀ : 0 ≤ C) (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist 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.

source
theorem metric.diam_le_of_forall_dist_le_of_nonempty {α : Type u} [pseudo_metric_space α] {s : set α} (hs : s.nonempty) {C : ℝ} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist 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.

source
theorem metric.dist_le_diam_of_mem' {α : Type u} [pseudo_metric_space α] {s : set α} {x y : α} (h : emetric.diam s ≠ ⊤) (hx : x ∈ s) (hy : y ∈ s) :
dist x y ≤ metric.diam s

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

source
theorem metric.bounded_iff_ediam_ne_top {α : Type u} [pseudo_metric_space α] {s : set α} :
metric.bounded s ↔ emetric.diam s ≠ ⊤

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

source
theorem metric.bounded.ediam_ne_top {α : Type u} [pseudo_metric_space α] {s : set α} (h : metric.bounded s) :
emetric.diam s ≠ ⊤
source
theorem metric.ediam_univ_eq_top_iff_noncompact {α : Type u} [pseudo_metric_space α] [proper_space α] :
emetric.diam set.univ = ⊤ ↔ noncompact_space α
source
@[simp]
theorem metric.ediam_univ_of_noncompact {α : Type u} [pseudo_metric_space α] [proper_space α] [noncompact_space α] :
emetric.diam set.univ = ⊤
source
@[simp]
theorem metric.diam_univ_of_noncompact {α : Type u} [pseudo_metric_space α] [proper_space α] [noncompact_space α] :
metric.diam set.univ = 0
source
theorem metric.dist_le_diam_of_mem {α : Type u} [pseudo_metric_space α] {s : set α} {x y : α} (h : metric.bounded s) (hx : x ∈ s) (hy : y ∈ s) :
dist x y ≤ metric.diam s

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

source
theorem metric.ediam_of_unbounded {α : Type u} [pseudo_metric_space α] {s : set α} (h : ¬metric.bounded s) :
emetric.diam s = ⊤
source
theorem metric.diam_eq_zero_of_unbounded {α : Type u} [pseudo_metric_space α] {s : set α} (h : ¬metric.bounded s) :
metric.diam s = 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

source
theorem metric.diam_mono {α : Type u} [pseudo_metric_space α] {s t : set α} (h : s ⊆ t) (ht : metric.bounded t) :
metric.diam s ≤ metric.diam t

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

source
theorem metric.diam_union {α : Type u} [pseudo_metric_space α] {s : set α} {x y : α} {t : set α} (xs : x ∈ s) (yt : y ∈ t) :
metric.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.

source
theorem metric.diam_union' {α : Type u} [pseudo_metric_space α] {s t : set α} (h : (s ∩ t).nonempty) :
metric.diam (s ∪ t) ≤ metric.diam s + metric.diam t

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

source
theorem metric.diam_le_of_subset_closed_ball {α : Type u} [pseudo_metric_space α] {s : set α} {x : α} {r : ℝ} (hr : 0 ≤ r) (h : s ⊆ metric.closed_ball x r) :
metric.diam s ≤ 2 * r
source
theorem metric.diam_closed_ball {α : Type u} [pseudo_metric_space α] {x : α} {r : ℝ} (h : 0 ≤ r) :
metric.diam (metric.closed_ball x r) ≤ 2 * r

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

source
theorem metric.diam_ball {α : Type u} [pseudo_metric_space α] {x : α} {r : ℝ} (h : 0 ≤ r) :
metric.diam (metric.ball x r) ≤ 2 * r

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

source
theorem is_complete.nonempty_Inter_of_nonempty_bInter {α : Type u} [pseudo_metric_space α] {s : ℕ → set α} (h0 : is_complete (s 0)) (hs : ∀ (n : ℕ), is_closed (s n)) (h's : ∀ (n : ℕ), metric.bounded (s n)) (h : ∀ (N : ℕ), (⋂ (n : ℕ) (H : n ≤ N), s n).nonempty) (h' : filter.tendsto (λ (n : ℕ), metric.diam (s n)) filter.at_top (𝓝 0)) :
(⋂ (n : ℕ), s n).nonempty

If a family of complete sets with diameter tending to 0 is such that each finite intersection is nonempty, then the total intersection is also nonempty.

source
theorem metric.nonempty_Inter_of_nonempty_bInter {α : Type u} [pseudo_metric_space α] [complete_space α] {s : ℕ → set α} (hs : ∀ (n : ℕ), is_closed (s n)) (h's : ∀ (n : ℕ), metric.bounded (s n)) (h : ∀ (N : ℕ), (⋂ (n : ℕ) (H : n ≤ N), s n).nonempty) (h' : filter.tendsto (λ (n : ℕ), metric.diam (s n)) filter.at_top (𝓝 0)) :
(⋂ (n : ℕ), s n).nonempty

In a complete space, if a family of closed sets with diameter tending to 0 is such that each finite intersection is nonempty, then the total intersection is also nonempty.

source
theorem comap_dist_right_at_top_le_cocompact {α : Type u} [pseudo_metric_space α] (x : α) :
filter.comap (λ (y : α), dist y x) filter.at_top ≤ filter.cocompact α
source
theorem comap_dist_left_at_top_le_cocompact {α : Type u} [pseudo_metric_space α] (x : α) :
filter.comap (dist x) filter.at_top ≤ filter.cocompact α
source
theorem comap_dist_right_at_top_eq_cocompact {α : Type u} [pseudo_metric_space α] [proper_space α] (x : α) :
filter.comap (λ (y : α), dist y x) filter.at_top = filter.cocompact α
source
theorem comap_dist_left_at_top_eq_cocompact {α : Type u} [pseudo_metric_space α] [proper_space α] (x : α) :
filter.comap (dist x) filter.at_top = filter.cocompact α
source
theorem tendsto_cocompact_of_tendsto_dist_comp_at_top {α : Type u} {β : Type v} [pseudo_metric_space α] {f : β → α} {l : filter β} (x : α) (h : filter.tendsto (λ (y : β), dist (f y) x) l filter.at_top) :
filter.tendsto f l (filter.cocompact α)
source
theorem int.tendsto_coe_cofinite  :
filter.tendsto coe filter.cofinite (filter.cocompact ℝ)

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

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

We now define metric_space, extending pseudo_metric_space.

Instances
source
@[ext]
theorem metric_space.ext {α : Type u_1} {m m' : metric_space α} (h : pseudo_metric_space.to_has_dist = pseudo_metric_space.to_has_dist) :
m = m'

Two metric space structures with the same distance coincide.

source
def metric_space.of_metrizable {α : Type u_1} [topological_space α] (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 α), is_open s ↔ ∀ (x : α), x ∈ s → (∃ (ε : ℝ) (H : ε > 0), ∀ (y : α), dist x y < ε → y ∈ s)) (eq_of_dist_eq_zero : ∀ (x y : α), dist x y = 0 → x = y) :
metric_space α

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

Equations
source
theorem eq_of_dist_eq_zero {γ : Type w} [metric_space γ] {x y : γ} :
dist x y = 0 → x = y
source
@[simp]
theorem dist_eq_zero {γ : Type w} [metric_space γ] {x y : γ} :
dist x y = 0 ↔ x = y
source
@[simp]
theorem zero_eq_dist {γ : Type w} [metric_space γ] {x y : γ} :
0 = dist x y ↔ x = y
source
theorem dist_ne_zero {γ : Type w} [metric_space γ] {x y : γ} :
dist x y ≠ 0 ↔ x ≠ y
source
@[simp]
theorem dist_le_zero {γ : Type w} [metric_space γ] {x y : γ} :
dist x y ≤ 0 ↔ x = y
source
@[simp]
theorem dist_pos {γ : Type w} [metric_space γ] {x y : γ} :
0 < dist x y ↔ x ≠ y
source
theorem eq_of_forall_dist_le {γ : Type w} [metric_space γ] {x y : γ} (h : ∀ (ε : ℝ), ε > 0 → dist x y ≤ ε) :
x = y
source
theorem eq_of_nndist_eq_zero {γ : Type w} [metric_space γ] {x y : γ} :
nndist x y = 0 → x = y

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

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

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

source
@[simp]
theorem zero_eq_nndist {γ : Type w} [metric_space γ] {x y : γ} :
0 = nndist x y ↔ x = y
source
@[simp]
theorem metric.closed_ball_zero {γ : Type w} [metric_space γ] {x : γ} :
metric.closed_ball x 0 = {x}
source
@[simp]
theorem metric.sphere_zero {γ : Type w} [metric_space γ] {x : γ} :
metric.sphere x 0 = {x}
source
theorem metric.subsingleton_closed_ball {γ : Type w} [metric_space γ] (x : γ) {r : ℝ} (hr : r ≤ 0) :
(metric.closed_ball x r).subsingleton
source
theorem metric.subsingleton_sphere {γ : Type w} [metric_space γ] (x : γ) {r : ℝ} (hr : r ≤ 0) :
(metric.sphere x r).subsingleton
source
theorem metric.uniform_embedding_iff' {β : Type v} {γ : Type w} [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.

source
@[protected, instance]
def metric.metric_space.to_separated {γ : Type w} [metric_space γ] :
separated_space γ
source
def metric.of_t2_pseudo_metric_space {α : Type u_1} [pseudo_metric_space α] (h : separated_space α) :
metric_space α

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

Equations
source
@[protected, instance]
def metric.metric_space.to_emetric_space {γ : Type w} [metric_space γ] :
emetric_space γ

A metric space induces an emetric space

Equations
source
theorem metric.is_closed_of_pairwise_le_dist {γ : Type w} [metric_space γ] {s : set γ} {ε : ℝ} (hε : 0 < ε) (hs : s.pairwise (λ (x y : γ), ε ≤ dist x y)) :
is_closed s
source
theorem metric.closed_embedding_of_pairwise_le_dist {γ : Type w} [metric_space γ] {α : Type u_1} [topological_space α] [discrete_topology α] {ε : ℝ} (hε : 0 < ε) {f : α → γ} (hf : pairwise (λ (x y : α), ε ≤ dist (f x) (f y))) :
closed_embedding f
source
theorem metric.uniform_embedding_bot_of_pairwise_le_dist {α : Type u} [pseudo_metric_space α] {β : Type u_1} {ε : ℝ} (hε : 0 < ε) {f : β → α} (hf : pairwise (λ (x y : β), ε ≤ dist (f x) (f y))) :
uniform_embedding f

If f : β → α sends any two distinct points to points at distance at least ε > 0, then f is a uniform embedding with respect to the discrete uniformity on β.

source
def metric_space.replace_uniformity {γ : Type u_1} [U : uniform_space γ] (m : metric_space γ) (H : 𝓤 γ = 𝓤 γ) :
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
source
theorem metric_space.replace_uniformity_eq {γ : Type u_1} [U : uniform_space γ] (m : metric_space γ) (H : 𝓤 γ = 𝓤 γ) :
m.replace_uniformity H = m
source
def metric_space.replace_topology {γ : Type u_1} [U : topological_space γ] (m : metric_space γ) (H : U = uniform_space.to_topological_space) :
metric_space γ

Build a new 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
source
theorem metric_space.replace_topology_eq {γ : Type u_1} [U : topological_space γ] (m : metric_space γ) (H : U = uniform_space.to_topological_space) :
m.replace_topology H = m
source
def emetric_space.to_metric_space_of_dist {α : Type u} [e : emetric_space α] (dist : α → α → ℝ) (edist_ne_top : ∀ (x y : α), edist x y ≠ ⊤) (h : ∀ (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
source
def emetric_space.to_metric_space {α : Type u} [e : emetric_space α] (h : ∀ (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
source
def metric_space.induced {γ : Type u_1} {β : Type u_2} (f : γ → β) (hf : function.injective f) (m : metric_space β) :
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
source
def uniform_embedding.comap_metric_space {α : Type u_1} {β : Type u_2} [uniform_space α] [metric_space β] (f : α → β) (h : uniform_embedding f) :
metric_space α

Pull back a metric space structure by a uniform embedding. This is a version of metric_space.induced useful in case if the domain already has a uniform_space structure.

Equations
source
def embedding.comap_metric_space {α : Type u_1} {β : Type u_2} [topological_space α] [metric_space β] (f : α → β) (h : embedding f) :
metric_space α

Pull back a metric space structure by an embedding. This is a version of metric_space.induced useful in case if the domain already has a topological_space structure.

Equations
source
@[protected, instance]
def subtype.metric_space {α : Type u_1} {p : α → Prop} [metric_space α] :
metric_space (subtype p)
Equations
source
@[protected, instance]
def mul_opposite.metric_space {α : Type u_1} [metric_space α] :
metric_space αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.metric_space {α : Type u_1} [metric_space α] :
metric_space αᵃᵒᵖ
Equations
source
@[protected, instance]
def empty.metric_space  :
metric_space empty
Equations
source
@[protected, instance]
def punit.metric_space  :
metric_space punit
Equations
source
@[protected, instance]
noncomputable def real.metric_space  :
metric_space ℝ

Instantiate the reals as a metric space.

Equations
source
@[protected, instance]
noncomputable def nnreal.metric_space  :
metric_space ℝ≥0
Equations
source
@[protected, instance]
noncomputable def prod.metric_space_max {β : Type v} {γ : Type w} [metric_space γ] [metric_space β] :
metric_space (γ × β)
Equations
source
@[protected, instance]
noncomputable 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
source
theorem metric.second_countable_of_countable_discretization {α : Type u} [metric_space α] (H : ∀ (ε : ℝ), ε > 0 → (∃ (β : Type u_1) (_x : encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε)) :
topological_space.second_countable_topology α

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

source
def pseudo_metric.dist_setoid (α : Type u) [pseudo_metric_space α] :
setoid α

The canonical equivalence relation on a pseudometric space.

Equations
source
def pseudo_metric_quot (α : Type u) [pseudo_metric_space α] :
Type u

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

Equations
source
@[protected, instance]
def has_dist_metric_quot {α : Type u} [pseudo_metric_space α] :
has_dist (pseudo_metric_quot α)
Equations
source
theorem pseudo_metric_quot_dist_eq {α : Type u} [pseudo_metric_space α] (p q : α) :
dist ⟦p⟧ ⟦q⟧ = dist p q
source
@[protected, instance]
def metric_space_quot {α : Type u} [pseudo_metric_space α] :
metric_space (pseudo_metric_quot α)
Equations