mathlib docs: topology.metric

def uniform_space_of_dist {α : Type u} (dist : α → α → ℝ) :

(∀ (x : α), dist x x = 0) → (∀ (x y : α), dist x y = dist y x) → (∀ (x y z : α), dist x z ≤ dist x y + dist y z) → uniform_space α

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

Equations

uniform_space_of_dist dist dist_self dist_comm dist_triangle = uniform_space.of_core {uniformity := ⨅ (ε : ℝ) (H : ε > 0), filter.principal {p : α × α | dist p.fst p.snd < ε}, refl := _, symm := _, comp := _}

source

@[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

@[class]

structure metric_space :

Type u → Type u

to_has_dist : has_dist α
dist_self : ∀ (x : α), has_dist.dist x x = 0
eq_of_dist_eq_zero : ∀ {x y : α}, has_dist.dist x y = 0 → x = y
dist_comm : ∀ (x y : α), has_dist.dist x y = has_dist.dist y x
dist_triangle : ∀ (x y z : α), has_dist.dist x z ≤ has_dist.dist x y + has_dist.dist y z
edist : α → α → ennreal
edist_dist : (∀ (x y : α), metric_space.edist x y = ennreal.of_real (has_dist.dist x y)) . "control_laws_tac"
to_uniform_space : uniform_space α
uniformity_dist : (uniformity α = ⨅ (ε : ℝ) (H : ε > 0), filter.principal {p : α × α | has_dist.dist p.fst p.snd < ε}) . "control_laws_tac"

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

@[instance]

def metric_space.to_uniform_space' {α : Type u} [metric_space α] :

uniform_space α

Equations

metric_space.to_uniform_space' = metric_space.to_uniform_space

source

@[instance]

def metric_space.to_has_edist {α : Type u} [metric_space α] :

has_edist α

Equations

metric_space.to_has_edist = {edist := metric_space.edist _inst_1}

source

@[simp]

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

has_dist.dist x x = 0

source

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

has_dist.dist x y = 0 → x = y

source

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

has_dist.dist x y = has_dist.dist y x

source

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

has_edist.edist x y = ennreal.of_real (has_dist.dist x y)

source

@[simp]

theorem dist_eq_zero {α : Type u} [metric_space α] {x y : α} :

has_dist.dist x y = 0 ↔ x = y

source

@[simp]

theorem zero_eq_dist {α : Type u} [metric_space α] {x y : α} :

0 = has_dist.dist x y ↔ x = y

source

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

has_dist.dist x z ≤ has_dist.dist x y + has_dist.dist y z

source

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

has_dist.dist x y ≤ has_dist.dist z x + has_dist.dist z y

source

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

has_dist.dist x y ≤ has_dist.dist x z + has_dist.dist y z

source

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

has_dist.dist x w ≤ has_dist.dist x y + has_dist.dist y z + has_dist.dist z w

source

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

has_dist.dist x₂ y₂ ≤ has_dist.dist x₁ y₁ + (has_dist.dist x₁ x₂ + has_dist.dist y₁ y₂)

source

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

has_dist.dist x₁ y₁ ≤ has_dist.dist x₁ x₂ + has_dist.dist y₁ y₂ + has_dist.dist x₂ y₂

source

theorem dist_le_Ico_sum_dist {α : Type u} [metric_space α] (f : ℕ → α) {m n : ℕ} :

m ≤ n → has_dist.dist (f m) (f n) ≤ (finset.Ico m n).sum (λ (i : ℕ), has_dist.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} [metric_space α] (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.

source

theorem dist_le_Ico_sum_of_dist_le {α : Type u} [metric_space α] {f : ℕ → α} {m n : ℕ} (hmn : m ≤ n) {d : ℕ → ℝ} :

(∀ {k : ℕ}, m ≤ k → k < n → has_dist.dist (f k) (f (k + 1)) ≤ d k) → has_dist.dist (f m) (f n) ≤ (finset.Ico m n).sum (λ (i : ℕ), 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} [metric_space α] {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ} :

(∀ {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.

source

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

function.swap has_dist.dist = has_dist.dist

source

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

abs (has_dist.dist x z - has_dist.dist y z) ≤ has_dist.dist x y

source

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

0 ≤ has_dist.dist x y

source

@[simp]

theorem dist_le_zero {α : Type u} [metric_space α] {x y : α} :

has_dist.dist x y ≤ 0 ↔ x = y

source

@[simp]

theorem dist_pos {α : Type u} [metric_space α] {x y : α} :

0 < has_dist.dist x y ↔ x ≠ y

source

@[simp]

theorem abs_dist {α : Type u} [metric_space α] {a b : α} :

abs (has_dist.dist a b) = has_dist.dist a b

source

theorem eq_of_forall_dist_le {α : Type u} [metric_space α] {x y : α} :

(∀ (ε : ℝ), ε > 0 → has_dist.dist x y ≤ ε) → x = y

source

def nndist {α : Type u} [metric_space α] :

α → α → nnreal

Distance as a nonnegative real number.

Equations

nndist a b = ⟨has_dist.dist a b, _⟩

source

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

nndist x y = (has_edist.edist x y).to_nnreal

Express nndist in terms of edist

source

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

has_edist.edist x y = ↑(nndist x y)

Express edist in terms of nndist

source

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

has_edist.edist x y ≠ ⊤

In a metric space, the extended distance is always finite

source

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

has_edist.edist x y < ⊤

In a metric space, the extended distance is always finite

source

@[simp]

theorem nndist_self {α : Type u} [metric_space α] (a : α) :

nndist a a = 0

nndist x x vanishes

source

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

has_dist.dist x y = ↑(nndist x y)

Express dist in terms of nndist

source

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

nndist x y = nnreal.of_real (has_dist.dist x y)

Express nndist in terms of dist

source

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

nndist x y = 0 → x = y

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

source

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

nndist x y = nndist y x

source

@[simp]

theorem nndist_eq_zero {α : Type u} [metric_space α] {x y : α} :

nndist x y = 0 ↔ x = y

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

source

@[simp]

theorem zero_eq_nndist {α : Type u} [metric_space α] {x y : α} :

0 = nndist x y ↔ x = y

source

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

nndist x z ≤ nndist x y + nndist y z

Triangle inequality for the nonnegative distance

source

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

nndist x y ≤ nndist z x + nndist z y

source

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

nndist x y ≤ nndist x z + nndist y z

source

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

has_dist.dist x y = (has_edist.edist x y).to_real

Express dist in terms of edist

source

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

α → ℝ → set α

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

Equations

metric.ball x ε = {y : α | has_dist.dist y x < ε}

source

@[simp]

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

y ∈ metric.ball x ε ↔ has_dist.dist y x < ε

source

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

y ∈ metric.ball x ε ↔ has_dist.dist x y < ε

source

@[simp]

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

0 < ε → (metric.ball x ε).nonempty

source

theorem metric.ball_eq_ball {α : Type u} [metric_space α] (ε : ℝ) (x : α) :

uniform_space.ball x {p : α × α | has_dist.dist p.snd p.fst < ε} = metric.ball x ε

source

theorem metric.ball_eq_ball' {α : Type u} [metric_space α] (ε : ℝ) (x : α) :

uniform_space.ball x {p : α × α | has_dist.dist p.fst p.snd < ε} = metric.ball x ε

source

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

α → ℝ → set α

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

Equations

metric.closed_ball x ε = {y : α | has_dist.dist y x ≤ ε}

source

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

α → ℝ → set α

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

Equations

metric.sphere x ε = {y : α | has_dist.dist y x = ε}

source

@[simp]

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

y ∈ metric.closed_ball x ε ↔ has_dist.dist y x ≤ ε

source

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

0 ≤ ε → (metric.closed_ball x ε).nonempty

source

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

metric.ball x ε ⊆ metric.closed_ball x ε

source

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

metric.sphere x ε ⊆ metric.closed_ball x ε

source

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

disjoint (metric.sphere x ε) (metric.ball x ε)

source

@[simp]

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

metric.ball x ε ∪ metric.sphere x ε = metric.closed_ball x ε

source

@[simp]

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

metric.sphere x ε ∪ metric.ball x ε = metric.closed_ball x ε

source

@[simp]

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

metric.closed_ball x ε \ metric.sphere x ε = metric.ball x ε

source

@[simp]

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

metric.closed_ball x ε \ metric.ball x ε = metric.sphere x ε

source

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

y ∈ metric.ball x ε → 0 < ε

source

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

0 < ε → x ∈ metric.ball x ε

source

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

0 ≤ ε → x ∈ metric.closed_ball x ε

source

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

x ∈ metric.ball y ε ↔ y ∈ metric.ball x ε

source

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

ε₁ ≤ ε₂ → metric.ball x ε₁ ⊆ metric.ball x ε₂

source

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

ε₁ ≤ ε₂ → metric.closed_ball x ε₁ ⊆ metric.closed_ball x ε₂

source

theorem metric.ball_disjoint {α : Type u} [metric_space α] {x y : α} {ε₁ ε₂ : ℝ} :

ε₁ + ε₂ ≤ has_dist.dist x y → metric.ball x ε₁ ∩ metric.ball y ε₂ = ∅

source

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

ε ≤ has_dist.dist x y / 2 → metric.ball x ε ∩ metric.ball y ε = ∅

source

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

has_dist.dist x y ≤ ε₂ - ε₁ → metric.ball x ε₁ ⊆ metric.ball y ε₂

source

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

y ∈ metric.ball x (ε / 2) → metric.ball y (ε / 2) ⊆ metric.ball x ε

source

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

y ∈ metric.ball x ε → (∃ (ε' : ℝ) (H : ε' > 0), metric.ball y ε' ⊆ metric.ball x ε)

source

@[simp]

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

metric.ball x ε = ∅ ↔ ε ≤ 0

source

@[simp]

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

metric.closed_ball x ε = ∅ ↔ ε < 0

source

@[simp]

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

metric.ball x 0 = ∅

source

@[simp]

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

metric.closed_ball x 0 = {x}

source

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

(uniformity α).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {p : α × α | has_dist.dist p.fst p.snd < ε})

source

theorem metric.mk_uniformity_basis {α : Type u} [metric_space α] {β : Type u_1} {p : β → Prop} {f : β → ℝ} :

(∀ (i : β), p i → 0 < f i) → (∀ ⦃ε : ℝ⦄, 0 < ε → (∃ (i : β) (hi : p i), f i ≤ ε)) → (uniformity α).has_basis p (λ (i : β), {p : α × α | has_dist.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} [metric_space α] :

(uniformity α).has_basis (λ (_x : ℕ), true) (λ (n : ℕ), {p : α × α | has_dist.dist p.fst p.snd < 1 / (↑n + 1)})

source

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

(uniformity α).has_basis (λ (n : ℕ), 0 < n) (λ (n : ℕ), {p : α × α | has_dist.dist p.fst p.snd < 1 / ↑n})

source

theorem metric.mk_uniformity_basis_le {α : Type u} [metric_space α] {β : Type u_1} {p : β → Prop} {f : β → ℝ} :

(∀ (x : β), p x → 0 < f x) → (∀ (ε : ℝ), 0 < ε → (∃ (x : β) (hx : p x), f x ≤ ε)) → (uniformity α).has_basis p (λ (x : β), {p : α × α | has_dist.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} [metric_space α] :

(uniformity α).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {p : α × α | has_dist.dist p.fst p.snd ≤ ε})

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

source

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

s ∈ uniformity α ↔ ∃ (ε : ℝ) (H : ε > 0), ∀ {a b : α}, has_dist.dist a b < ε → (a, b) ∈ s

source

theorem metric.dist_mem_uniformity {α : Type u} [metric_space α] {ε : ℝ} :

0 < ε → {p : α × α | has_dist.dist p.fst p.snd < ε} ∈ uniformity α

A constant size neighborhood of the diagonal is an entourage.

source

theorem metric.uniform_continuous_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :

uniform_continuous f ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {a b : α}, has_dist.dist a b < δ → has_dist.dist (f a) (f b) < ε)

source

theorem metric.uniform_continuous_on_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {s : set α} :

uniform_continuous_on f s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x y : α), x ∈ s → y ∈ s → has_dist.dist x y < δ → has_dist.dist (f x) (f y) < ε)

source

theorem metric.uniform_embedding_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :

uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧ ∀ (δ : ℝ), δ > 0 → (∃ (ε : ℝ) (H : ε > 0), ∀ {a b : α}, has_dist.dist (f a) (f b) < ε → has_dist.dist a b < δ)

source

theorem metric.uniform_embedding_iff' {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :

uniform_embedding f ↔ (∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {a b : α}, has_dist.dist a b < δ → has_dist.dist (f a) (f b) < ε)) ∧ ∀ (δ : ℝ), δ > 0 → (∃ (ε : ℝ) (H : ε > 0), ∀ {a b : α}, has_dist.dist (f a) (f b) < ε → has_dist.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

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

totally_bounded s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (t : set α), t.finite ∧ s ⊆ ⋃ (y : α) (H : y ∈ t), metric.ball y ε)

source

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

(∀ (ε : ℝ), ε > 0 → (∃ (β : Type u) [_inst_2 : fintype β] (F : ↥s → β), ∀ (x y : ↥s), F x = F y → has_dist.dist ↑x ↑y < ε)) → totally_bounded s

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

source

theorem metric.finite_approx_of_totally_bounded {α : Type u} [metric_space α] {s : set α} (hs : totally_bounded s) (ε : ℝ) :

ε > 0 → (∃ (t : set α) (H : t ⊆ s), t.finite ∧ s ⊆ ⋃ (y : α) (H : y ∈ t), metric.ball y ε)

source

theorem metric.tendsto_locally_uniformly_on_iff {α : Type u} {β : Type v} [metric_space α] {ι : Type u_1} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :

tendsto_locally_uniformly_on F f p s ↔ ∀ (ε : ℝ), ε > 0 → ∀ (x : β), x ∈ s → (∃ (t : set β) (H : t ∈ nhds_within x s), ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → has_dist.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} [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 → has_dist.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} [metric_space α] {ι : Type u_1} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} :

tendsto_locally_uniformly F f p ↔ ∀ (ε : ℝ), ε > 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.

source

theorem metric.tendsto_uniformly_iff {α : Type u} {β : Type v} [metric_space α] {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} :

tendsto_uniformly F f p ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (n : ι) in p, ∀ (x : β), has_dist.dist (f x) (F n x) < ε)

Expressing uniform convergence using dist.

source

theorem metric.cauchy_iff {α : Type u} [metric_space α] {f : filter α} :

cauchy f ↔ f.ne_bot ∧ ∀ (ε : ℝ), ε > 0 → (∃ (t : set α) (H : t ∈ f), ∀ (x y : α), x ∈ t → y ∈ t → has_dist.dist x y < ε)

source

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

(nhds x).has_basis (λ (ε : ℝ), 0 < ε) (metric.ball x)

source

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

s ∈ nhds x ↔ ∃ (ε : ℝ) (H : ε > 0), metric.ball x ε ⊆ s

source

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

(nhds x).has_basis (λ (ε : ℝ), 0 < ε) (metric.closed_ball x)

source

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

(nhds x).has_basis (λ (_x : ℕ), true) (λ (n : ℕ), metric.ball x (1 / (↑n + 1)))

source

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

(nhds x).has_basis (λ (n : ℕ), 0 < n) (λ (n : ℕ), metric.ball x (1 / ↑n))

source

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

is_open s ↔ ∀ (x : α), x ∈ s → (∃ (ε : ℝ) (H : ε > 0), metric.ball x ε ⊆ s)

source

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

is_open (metric.ball x ε)

source

theorem metric.ball_mem_nhds {α : Type u} [metric_space α] (x : α) {ε : ℝ} :

0 < ε → metric.ball x ε ∈ nhds x

source

theorem metric.closed_ball_mem_nhds {α : Type u} [metric_space α] (x : α) {ε : ℝ} :

0 < ε → metric.closed_ball x ε ∈ nhds x

source

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

(nhds_within x s).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), metric.ball x ε ∩ s)

source

theorem metric.mem_nhds_within_iff {α : Type u} [metric_space α] {x : α} {s t : set α} :

s ∈ nhds_within x t ↔ ∃ (ε : ℝ) (H : ε > 0), metric.ball x ε ∩ t ⊆ s

source

theorem metric.tendsto_nhds_within_nhds_within {α : Type u} {β : Type v} [metric_space α] {s : set α} [metric_space β] {t : set β} {f : α → β} {a : α} {b : β} :

filter.tendsto f (nhds_within a s) (nhds_within b t) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, x ∈ s → has_dist.dist x a < δ → f x ∈ t ∧ has_dist.dist (f x) b < ε)

source

theorem metric.tendsto_nhds_within_nhds {α : Type u} {β : Type v} [metric_space α] {s : set α} [metric_space β] {f : α → β} {a : α} {b : β} :

filter.tendsto f (nhds_within a s) (nhds b) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, x ∈ s → has_dist.dist x a < δ → has_dist.dist (f x) b < ε)

source

theorem metric.tendsto_nhds_nhds {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {a : α} {b : β} :

filter.tendsto f (nhds a) (nhds b) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, has_dist.dist x a < δ → has_dist.dist (f x) b < ε)

source

theorem metric.continuous_at_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {a : α} :

continuous_at f a ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, has_dist.dist x a < δ → has_dist.dist (f x) (f a) < ε)

source

theorem metric.continuous_within_at_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {a : α} {s : set α} :

continuous_within_at f s a ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, x ∈ s → has_dist.dist x a < δ → has_dist.dist (f x) (f a) < ε)

source

theorem metric.continuous_on_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {s : set α} :

continuous_on f s ↔ ∀ (b : α), b ∈ s → ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (a : α), a ∈ s → has_dist.dist a b < δ → has_dist.dist (f a) (f b) < ε)

source

theorem metric.continuous_iff {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :

continuous f ↔ ∀ (b : α) (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (a : α), has_dist.dist a b < δ → has_dist.dist (f a) (f b) < ε)

source

theorem metric.tendsto_nhds {α : Type u} {β : Type v} [metric_space α] {f : filter β} {u : β → α} {a : α} :

filter.tendsto u f (nhds a) ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in f, has_dist.dist (u x) a < ε)

source

theorem metric.continuous_at_iff' {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f : β → α} {b : β} :

continuous_at f b ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in nhds b, has_dist.dist (f x) (f b) < ε)

source

theorem metric.continuous_within_at_iff' {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f : β → α} {b : β} {s : set β} :

continuous_within_at f s b ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in nhds_within b s, has_dist.dist (f x) (f b) < ε)

source

theorem metric.continuous_on_iff' {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f : β → α} {s : set β} :

continuous_on f s ↔ ∀ (b : β), b ∈ s → ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in nhds_within b s, has_dist.dist (f x) (f b) < ε)

source

theorem metric.continuous_iff' {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f : β → α} :

continuous f ↔ ∀ (a : β) (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in nhds a, has_dist.dist (f x) (f a) < ε)

source

theorem metric.tendsto_at_top {α : Type u} {β : Type v} [metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} {a : α} :

filter.tendsto u filter.at_top (nhds a) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : β), ∀ (n : β), n ≥ N → has_dist.dist (u n) a < ε)

source

@[instance]

def metric_space.to_separated {α : Type u} [metric_space α] :

separated_space α

Equations

metric_space.to_separated = _

source

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

(uniformity α).has_basis (λ (ε : ennreal), 0 < ε) (λ (ε : ennreal), {p : α × α | has_edist.edist p.fst p.snd < ε})

Expressing the uniformity in terms of edist

source

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

uniformity α = ⨅ (ε : ennreal) (H : ε > 0), filter.principal {p : α × α | has_edist.edist p.fst p.snd < ε}

source

@[instance]

def metric_space.to_emetric_space {α : Type u} [metric_space α] :

emetric_space α

A metric space induces an emetric space

Equations

metric_space.to_emetric_space = {to_has_edist := {edist := has_edist.edist metric_space.to_has_edist}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := metric_space.to_uniform_space _inst_1, uniformity_edist := _}

source

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

emetric.ball x (ennreal.of_real ε) = metric.ball x ε

Balls defined using the distance or the edistance coincide

source

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

emetric.ball x ↑ε = metric.ball x ↑ε

Balls defined using the distance or the edistance coincide

source

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

0 ≤ ε → emetric.closed_ball x (ennreal.of_real ε) = metric.closed_ball x ε

Closed balls defined using the distance or the edistance coincide

source

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

emetric.closed_ball x ↑ε = metric.closed_ball x ↑ε

Closed balls defined using the distance or the edistance coincide

source

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

uniformity α = uniformity α → 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

m.replace_uniformity H = {to_has_dist := {dist := has_dist.dist metric_space.to_has_dist}, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := has_edist.edist metric_space.to_has_edist, edist_dist := _, to_uniform_space := U, uniformity_dist := _}

source

def emetric_space.to_metric_space_of_dist {α : Type u} [e : emetric_space α] (dist : α → α → ℝ) :

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

emetric_space.to_metric_space_of_dist dist edist_ne_top h = let m : metric_space α := {to_has_dist := {dist := dist}, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : α), has_edist.edist x y, edist_dist := _, to_uniform_space := uniform_space_of_dist dist _ _ _, uniformity_dist := _} in m.replace_uniformity _

source

def emetric_space.to_metric_space {α : Type u} [e : emetric_space α] :

(∀ (x y : α), has_edist.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

emetric_space.to_metric_space h = emetric_space.to_metric_space_of_dist (λ (x y : α), (has_edist.edist x y).to_real) h emetric_space.to_metric_space._proof_1

source

theorem metric.complete_of_convergent_controlled_sequences {α : Type u} [metric_space α] (B : ℕ → ℝ) :

(∀ (n : ℕ), 0 < B n) → (∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → has_dist.dist (u n) (u m) < B N) → (∃ (x : α), filter.tendsto u filter.at_top (nhds 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} [metric_space α] :

(∀ (u : ℕ → α), cauchy_seq u → (∃ (a : α), filter.tendsto u filter.at_top (nhds a))) → complete_space α

source

@[instance]

def real.metric_space :

metric_space ℝ

Instantiate the reals as a metric space.

Equations

real.metric_space = {to_has_dist := {dist := λ (x y : ℝ), abs (x - y)}, dist_self := real.metric_space._proof_1, eq_of_dist_eq_zero := real.metric_space._proof_2, dist_comm := real.metric_space._proof_3, dist_triangle := real.metric_space._proof_4, edist := λ (x y : ℝ), ennreal.of_real ((λ (x y : ℝ), abs (x - y)) x y), edist_dist := real.metric_space._proof_5, to_uniform_space := uniform_space_of_dist (λ (x y : ℝ), abs (x - y)) real.metric_space._proof_6 real.metric_space._proof_7 real.metric_space._proof_8, uniformity_dist := real.metric_space._proof_9}

source

theorem real.dist_eq (x y : ℝ) :

has_dist.dist x y = abs (x - y)

source

theorem real.dist_0_eq_abs (x : ℝ) :

has_dist.dist x 0 = abs x

source

@[instance]

def real.order_topology :

order_topology ℝ

Equations

real.order_topology = _

source

theorem closed_ball_Icc {x r : ℝ} :

metric.closed_ball x r = set.Icc (x - r) (x + r)

source

theorem squeeze_zero' {α : Type u_1} {f g : α → ℝ} {t₀ : filter α} :

(∀ᶠ (t : α) in t₀, 0 ≤ f t) → (∀ᶠ (t : α) in t₀, f t ≤ g t) → filter.tendsto g t₀ (nhds 0) → filter.tendsto f t₀ (nhds 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 α} :

(∀ (t : α), 0 ≤ f t) → (∀ (t : α), f t ≤ g t) → filter.tendsto g t₀ (nhds 0) → filter.tendsto f 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.

source

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

uniformity α = filter.comap (λ (p : α × α), has_dist.dist p.fst p.snd) (nhds 0)

source

theorem cauchy_seq_iff_tendsto_dist_at_top_0 {α : Type u} {β : Type v} [metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :

cauchy_seq u ↔ filter.tendsto (λ (n : β × β), has_dist.dist (u n.fst) (u n.snd)) filter.at_top (nhds 0)

source

theorem tendsto_uniformity_iff_dist_tendsto_zero {α : Type u} [metric_space α] {ι : Type u_1} {f : ι → α × α} {p : filter ι} :

filter.tendsto f p (uniformity α) ↔ filter.tendsto (λ (x : ι), has_dist.dist (f x).fst (f x).snd) p (nhds 0)

source

theorem filter.tendsto.congr_dist {α : Type u} [metric_space α] {ι : Type u_1} {f₁ f₂ : ι → α} {p : filter ι} {a : α} :

filter.tendsto f₁ p (nhds a) → filter.tendsto (λ (x : ι), has_dist.dist (f₁ x) (f₂ x)) p (nhds 0) → filter.tendsto f₂ p (nhds a)

source

theorem tendsto_iff_of_dist {α : Type u} [metric_space α] {ι : Type u_1} {f₁ f₂ : ι → α} {p : filter ι} {a : α} :

filter.tendsto (λ (x : ι), has_dist.dist (f₁ x) (f₂ x)) p (nhds 0) → (filter.tendsto f₁ p (nhds a) ↔ filter.tendsto f₂ p (nhds a))

source

@[nolint]

theorem metric.cauchy_seq_iff {α : Type u} {β : Type v} [metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :

cauchy_seq u ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : β), ∀ (m n : β), m ≥ N → n ≥ N → has_dist.dist (u m) (u n) < ε)

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

source

theorem metric.cauchy_seq_iff' {α : Type u} {β : Type v} [metric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :

cauchy_seq u ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : β), ∀ (n : β), n ≥ N → has_dist.dist (u n) (u N) < ε)

A variation around the metric characterization of Cauchy sequences

source

theorem cauchy_seq_of_le_tendsto_0 {α : Type u} {β : Type v} [metric_space α] [nonempty β] [semilattice_sup β] {s : β → α} (b : β → ℝ) :

(∀ (n m N : β), N ≤ n → N ≤ m → has_dist.dist (s n) (s m) ≤ b N) → filter.tendsto b filter.at_top (nhds 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} [metric_space α] {u : ℕ → α} :

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.

source

theorem cauchy_seq_iff_le_tendsto_0 {α : Type u} [metric_space α] {s : ℕ → α} :

cauchy_seq s ↔ ∃ (b : ℕ → ℝ), (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → has_dist.dist (s n) (s m) ≤ b N) ∧ filter.tendsto b filter.at_top (nhds 0)

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

source

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

function.injective f → 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

metric_space.induced f hf m = {to_has_dist := {dist := λ (x y : α), has_dist.dist (f x) (f y)}, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : α), has_edist.edist (f x) (f y), edist_dist := _, to_uniform_space := uniform_space.comap f metric_space.to_uniform_space, uniformity_dist := _}

source

@[instance]

def subtype.metric_space {α : Type u_1} {p : α → Prop} [t : metric_space α] :

metric_space (subtype p)

Equations

subtype.metric_space = metric_space.induced coe subtype.metric_space._proof_1 t

source

theorem subtype.dist_eq {α : Type u} [metric_space α] {p : α → Prop} (x y : subtype p) :

has_dist.dist x y = has_dist.dist ↑x ↑y

source

@[instance]

def nnreal.metric_space :

metric_space nnreal

Equations

nnreal.metric_space = nnreal.metric_space._proof_1.mpr subtype.metric_space

source

theorem nnreal.dist_eq (a b : nnreal) :

has_dist.dist a b = abs (↑a - ↑b)

source

theorem nnreal.nndist_eq (a b : nnreal) :

nndist a b = max (a - b) (b - a)

source

@[instance]

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

metric_space (α × β)

Equations

prod.metric_space_max = {to_has_dist := {dist := λ (x y : α × β), max (has_dist.dist x.fst y.fst) (has_dist.dist x.snd y.snd)}, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : α × β), max (has_edist.edist x.fst y.fst) (has_edist.edist x.snd y.snd), edist_dist := _, to_uniform_space := prod.uniform_space metric_space.to_uniform_space', uniformity_dist := _}

source

theorem prod.dist_eq {α : Type u} {β : Type v} [metric_space α] [metric_space β] {x y : α × β} :

has_dist.dist x y = max (has_dist.dist x.fst y.fst) (has_dist.dist x.snd y.snd)

source

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

uniform_continuous (λ (p : α × α), has_dist.dist p.fst p.snd)

source

theorem uniform_continuous.dist {α : Type u} {β : Type v} [metric_space α] [uniform_space β] {f g : β → α} :

uniform_continuous f → uniform_continuous g → uniform_continuous (λ (b : β), has_dist.dist (f b) (g b))

source

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

continuous (λ (p : α × α), has_dist.dist p.fst p.snd)

source

theorem continuous.dist {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f g : β → α} :

continuous f → continuous g → continuous (λ (b : β), has_dist.dist (f b) (g b))

source

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

filter.tendsto f x (nhds a) → filter.tendsto g x (nhds b) → filter.tendsto (λ (x : β), has_dist.dist (f x) (g x)) x (nhds (has_dist.dist a b))

source

theorem nhds_comap_dist {α : Type u} [metric_space α] (a : α) :

filter.comap (λ (a' : α), has_dist.dist a' a) (nhds 0) = nhds a

source

theorem tendsto_iff_dist_tendsto_zero {α : Type u} {β : Type v} [metric_space α] {f : β → α} {x : filter β} {a : α} :

filter.tendsto f x (nhds a) ↔ filter.tendsto (λ (b : β), has_dist.dist (f b) a) x (nhds 0)

source

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

uniform_continuous (λ (p : α × α), nndist p.fst p.snd)

source

theorem uniform_continuous.nndist {α : Type u} {β : Type v} [metric_space α] [uniform_space β] {f g : β → α} :

uniform_continuous f → uniform_continuous g → uniform_continuous (λ (b : β), nndist (f b) (g b))

source

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

continuous (λ (p : α × α), nndist p.fst p.snd)

source

theorem continuous.nndist {α : Type u} {β : Type v} [metric_space α] [topological_space β] {f g : β → α} :

continuous f → continuous g → continuous (λ (b : β), nndist (f b) (g b))

source

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

filter.tendsto f x (nhds a) → filter.tendsto g x (nhds b) → filter.tendsto (λ (x : β), nndist (f x) (g x)) x (nhds (nndist a b))

source

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

is_closed (metric.closed_ball x ε)

source

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

is_closed (metric.sphere x ε)

source

@[simp]

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

closure (metric.closed_ball x ε) = metric.closed_ball x ε

source

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

closure (metric.ball x ε) ⊆ metric.closed_ball x ε

source

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

frontier (metric.ball x ε) ⊆ metric.sphere x ε

source

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

frontier (metric.closed_ball x ε) ⊆ metric.sphere x ε

source

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

metric.ball x ε ⊆ interior (metric.closed_ball x ε)

source

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

a ∈ closure s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (b : α) (H : b ∈ s), has_dist.dist a b < ε)

ε-characterization of the closure in metric spaces

source

theorem metric.mem_closure_range_iff {β : Type v} {α : Type u} [metric_space α] {e : β → α} {a : α} :

a ∈ closure (set.range e) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (k : β), has_dist.dist a (e k) < ε)

source

theorem metric.mem_closure_range_iff_nat {β : Type v} {α : Type u} [metric_space α] {e : β → α} {a : α} :

a ∈ closure (set.range e) ↔ ∀ (n : ℕ), ∃ (k : β), has_dist.dist a (e k) < 1 / (↑n + 1)

source

theorem metric.mem_of_closed' {α : Type u} [metric_space α] {s : set α} (hs : is_closed s) {a : α} :

a ∈ s ↔ ∀ (ε : ℝ), ε > 0 → (∃ (b : α) (H : b ∈ s), has_dist.dist a b < ε)

source

@[instance]

def metric_space_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space (π b)] :

metric_space (Π (b : β), π b)

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

Equations

metric_space_pi = emetric_space.to_metric_space_of_dist (λ (f g : Π (b : β), π b), ↑(finset.univ.sup (λ (b : β), nndist (f b) (g b)))) metric_space_pi._proof_1 metric_space_pi._proof_2

source

theorem dist_pi_def {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space (π b)] (f g : Π (b : β), π b) :

has_dist.dist f g = ↑(finset.univ.sup (λ (b : β), nndist (f b) (g b)))

source

theorem dist_pi_lt_iff {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space (π b)] {f g : Π (b : β), π b} {r : ℝ} :

0 < r → (has_dist.dist f g < r ↔ ∀ (b : β), has_dist.dist (f b) (g b) < r)

source

theorem dist_pi_le_iff {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space (π b)] {f g : Π (b : β), π b} {r : ℝ} :

0 ≤ r → (has_dist.dist f g ≤ r ↔ ∀ (b : β), has_dist.dist (f b) (g b) ≤ r)

source

theorem ball_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space (π b)] (x : Π (b : β), π b) {r : ℝ} :

0 < r → metric.ball x r = {y : Π (b : β), π b | ∀ (b : β), y b ∈ metric.ball (x b) r}

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

source

theorem closed_ball_pi {β : Type v} {π : β → Type u_1} [fintype β] [Π (b : β), metric_space (π b)] (x : Π (b : β), π b) {r : ℝ} :

0 ≤ r → metric.closed_ball x r = {y : Π (b : β), π b | ∀ (b : β), y b ∈ metric.closed_ball (x b) r}

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

source

theorem finite_cover_balls_of_compact {α : Type u} [metric_space α] {s : set α} (hs : is_compact s) {e : ℝ} :

0 < e → (∃ (t : set α) (H : t ⊆ s), t.finite ∧ s ⊆ ⋃ (x : α) (H : x ∈ t), metric.ball x e)

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

source

@[class]

structure proper_space (α : Type u) [metric_space α] :

Prop

compact_ball : ∀ (x : α) (r : ℝ), is_compact (metric.closed_ball x r)

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

Instances

source

theorem proper_space_of_compact_closed_ball_of_le {α : Type u} [metric_space α] (R : ℝ) :

(∀ (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

@[instance]

def proper_of_compact {α : Type u} [metric_space α] [compact_space α] :

proper_space α

Equations

proper_of_compact = _

source

@[instance]

def locally_compact_of_proper {α : Type u} [metric_space α] [proper_space α] :

locally_compact_space α

A proper space is locally compact

Equations

locally_compact_of_proper = _

source

@[instance]

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

complete_space α

A proper space is complete

Equations

complete_of_proper = _

source

@[instance]

def second_countable_of_proper {α : Type u} [metric_space α] [proper_space α] :

topological_space.second_countable_topology α

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

Equations

second_countable_of_proper = _

source

@[instance]

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

proper_space (Π (b : β), π b)

A finite product of proper spaces is proper.

Equations

pi_proper_space = _

source

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

(∀ (ε : ℝ), ε > 0 → (∃ (s : set α), s.countable ∧ ∀ (x : α), ∃ (y : α) (H : y ∈ s), has_dist.dist x y ≤ ε)) → topological_space.second_countable_topology α

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

source

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

(∀ (ε : ℝ), ε > 0 → (∃ (β : Type u) [_inst_3 : encodable β] (F : α → β), ∀ (x y : α), F x = F y → has_dist.dist x y ≤ ε)) → topological_space.second_countable_topology α

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

source

theorem lebesgue_number_lemma_of_metric {α : Type u} [metric_space α] {s : set α} {ι : Sort u_1} {c : ι → set α} :

is_compact s → (∀ (i : ι), is_open (c i)) → (s ⊆ ⋃ (i : ι), c i) → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : α), x ∈ s → (∃ (i : ι), metric.ball x δ ⊆ c i))

source

theorem lebesgue_number_lemma_of_metric_sUnion {α : Type u} [metric_space α] {s : set α} {c : set (set α)} :

is_compact s → (∀ (t : set α), t ∈ c → is_open t) → s ⊆ ⋃₀c → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : α), x ∈ s → (∃ (t : set α) (H : t ∈ c), metric.ball x δ ⊆ t))

source

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

set α → Prop

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

Equations

metric.bounded s = ∃ (C : ℝ), ∀ (x y : α), x ∈ s → y ∈ s → has_dist.dist x y ≤ C

source

@[simp]

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

metric.bounded ∅

source

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

metric.bounded s ↔ ∀ (x : α), x ∈ s → metric.bounded s

source

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

s ⊆ t → metric.bounded t → metric.bounded s

Subsets of a bounded set are also bounded

source

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

metric.bounded (metric.closed_ball x r)

Closed balls are bounded

source

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

metric.bounded (metric.ball x r)

Open balls are bounded

source

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

metric.bounded s → metric.bounded (closure s)

source

@[simp]

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

metric.bounded (s ∪ t) ↔ metric.bounded s ∧ metric.bounded t

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

source

theorem metric.bounded_bUnion {α : Type u} {β : Type v} [metric_space α] {I : set β} {s : β → set α} :

I.finite → (metric.bounded (⋃ (i : β) (H : i ∈ I), s i) ↔ ∀ (i : β), i ∈ I → metric.bounded (s i))

A finite union of bounded sets is bounded

source

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

is_compact s → metric.bounded s

A compact set is bounded

source

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

s.finite → metric.bounded s

A finite set is bounded

source

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

metric.bounded {x}

A singleton is bounded

source

theorem metric.bounded_range_iff {α : Type u} {β : Type v} [metric_space α] {f : β → α} :

metric.bounded (set.range f) ↔ ∃ (C : ℝ), ∀ (x y : β), has_dist.dist (f x) (f y) ≤ C

Characterization of the boundedness of the range of a function

source

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

metric.bounded s

In a compact space, all sets are bounded

source

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

is_compact s ↔ is_closed s ∧ metric.bounded s

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

source

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

(∀ (x y : α), has_dist.dist x y ≤ C * has_dist.dist (f x) (f y)) → proper_space β

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

source

def metric.diam {α : Type u} [metric_space α] :

set α → ℝ

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

Equations

metric.diam s = (emetric.diam s).to_real

source

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

0 ≤ metric.diam s

The diameter of a set is always nonnegative

source

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

s.subsingleton → metric.diam s = 0

source

@[simp]

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

metric.diam ∅ = 0

The empty set has zero diameter

source

@[simp]

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

metric.diam {x} = 0

A singleton has zero diameter

source

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

metric.diam {x, y} = has_dist.dist x y

source

theorem metric.diam_triple {α : Type u} [metric_space α] {x y z : α} :

metric.diam {x, y, z} = max (max (has_dist.dist x y) (has_dist.dist x z)) (has_dist.dist y z)

source

theorem metric.ediam_le_of_forall_dist_le {α : Type u} [metric_space α] {s : set α} {C : ℝ} :

(∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.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} [metric_space α] {s : set α} {C : ℝ} :

0 ≤ C → (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.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} [metric_space α] {s : set α} (hs : s.nonempty) {C : ℝ} :

(∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.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} [metric_space α] {s : set α} {x y : α} :

emetric.diam s ≠ ⊤ → x ∈ s → y ∈ s → has_dist.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} [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} [metric_space α] {s : set α} :

metric.bounded s → emetric.diam s ≠ ⊤

source

theorem metric.dist_le_diam_of_mem {α : Type u} [metric_space α] {s : set α} {x y : α} :

metric.bounded s → x ∈ s → y ∈ s → has_dist.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.diam_eq_zero_of_unbounded {α : Type u} [metric_space α] {s : set α} :

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

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

x ∈ s → y ∈ t → metric.diam (s ∪ t) ≤ metric.diam s + has_dist.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