mathlib docs: topology.metric_space.emetric

source

theorem uniformity_dist_of_mem_uniformity {α : Type u} {β : Type v} [linear_order β] {U : filter (α × α)} (z : β) (D : α → α → β) :

(∀ (s : set (α × α)), s ∈ U ↔ ∃ (ε : β) (H : ε > z), ∀ {a b : α}, D a b < ε → (a, b) ∈ s) → (U = ⨅ (ε : β) (H : ε > z), filter.principal {p : α × α | D p.fst p.snd < ε})

Characterizing uniformities associated to a (generalized) distance function D in terms of the elements of the uniformity.

source

@[class]

structure has_edist :

Type u_1 → Type u_1

edist : α → α → ennreal

Instances

source

def uniform_space_of_edist {α : Type u} (edist : α → α → ennreal) :

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

Creating a uniform space from an extended distance.

Equations

uniform_space_of_edist edist edist_self edist_comm edist_triangle = uniform_space.of_core {uniformity := ⨅ (ε : ennreal) (H : ε > 0), filter.principal {p : α × α | edist p.fst p.snd < ε}, refl := _, symm := _, comp := _}

source

@[class]

structure emetric_space :

Type u → Type u

to_has_edist : has_edist α
edist_self : ∀ (x : α), has_edist.edist x x = 0
eq_of_edist_eq_zero : ∀ {x y : α}, has_edist.edist x y = 0 → x = y
edist_comm : ∀ (x y : α), has_edist.edist x y = has_edist.edist y x
edist_triangle : ∀ (x y z : α), has_edist.edist x z ≤ has_edist.edist x y + has_edist.edist y z
to_uniform_space : uniform_space α
uniformity_edist : (uniformity α = ⨅ (ε : ennreal) (H : ε > 0), filter.principal {p : α × α | has_edist.edist p.fst p.snd < ε}) . "control_laws_tac"

Extended metric spaces, with an extended distance edist possibly taking the value ∞

Each emetric 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 an emetric_space structure, the uniformity fields are not necessary, they will be filled in by default. There is a default value for the uniformity, that can be substituted in cases of interest, for instance when instantiating an emetric_space structure on a product.

Continuity of edist is proved in topology.instances.ennreal

Instances

source

@[instance]

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

uniform_space α

Equations

emetric_space.to_uniform_space' = emetric_space.to_uniform_space

source

@[simp]

theorem edist_eq_zero {α : Type u} [emetric_space α] {x y : α} :

has_edist.edist x y = 0 ↔ x = y

Characterize the equality of points by the vanishing of their extended distance

source

@[simp]

theorem zero_eq_edist {α : Type u} [emetric_space α] {x y : α} :

0 = has_edist.edist x y ↔ x = y

source

theorem edist_le_zero {α : Type u} [emetric_space α] {x y : α} :

has_edist.edist x y ≤ 0 ↔ x = y

source

theorem edist_triangle_left {α : Type u} [emetric_space α] (x y z : α) :

has_edist.edist x y ≤ has_edist.edist z x + has_edist.edist z y

Triangle inequality for the extended distance

source

theorem edist_triangle_right {α : Type u} [emetric_space α] (x y z : α) :

has_edist.edist x y ≤ has_edist.edist x z + has_edist.edist y z

source

theorem edist_triangle4 {α : Type u} [emetric_space α] (x y z t : α) :

has_edist.edist x t ≤ has_edist.edist x y + has_edist.edist y z + has_edist.edist z t

source

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

m ≤ n → has_edist.edist (f m) (f n) ≤ (finset.Ico m n).sum (λ (i : ℕ), has_edist.edist (f i) (f (i + 1)))

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

source

theorem edist_le_range_sum_edist {α : Type u} [emetric_space α] (f : ℕ → α) (n : ℕ) :

has_edist.edist (f 0) (f n) ≤ (finset.range n).sum (λ (i : ℕ), has_edist.edist (f i) (f (i + 1)))

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

source

theorem edist_le_Ico_sum_of_edist_le {α : Type u} [emetric_space α] {f : ℕ → α} {m n : ℕ} (hmn : m ≤ n) {d : ℕ → ennreal} :

(∀ {k : ℕ}, m ≤ k → k < n → has_edist.edist (f k) (f (k + 1)) ≤ d k) → has_edist.edist (f m) (f n) ≤ (finset.Ico m n).sum (λ (i : ℕ), d i)

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

source

theorem edist_le_range_sum_of_edist_le {α : Type u} [emetric_space α] {f : ℕ → α} (n : ℕ) {d : ℕ → ennreal} :

(∀ {k : ℕ}, k < n → has_edist.edist (f k) (f (k + 1)) ≤ d k) → has_edist.edist (f 0) (f n) ≤ (finset.range n).sum (λ (i : ℕ), d i)

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

source

theorem eq_of_forall_edist_le {α : Type u} [emetric_space α] {x y : α} :

(∀ (ε : ennreal), ε > 0 → has_edist.edist x y ≤ ε) → x = y

Two points coincide if their distance is < ε for all positive ε

source

theorem uniformity_edist {α : Type u} [emetric_space α] :

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

Reformulation of the uniform structure in terms of the extended distance

source

theorem uniformity_basis_edist {α : Type u} [emetric_space α] :

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

source

theorem mem_uniformity_edist {α : Type u} [emetric_space α] {s : set (α × α)} :

s ∈ uniformity α ↔ ∃ (ε : ennreal) (H : ε > 0), ∀ {a b : α}, has_edist.edist a b < ε → (a, b) ∈ s

Characterization of the elements of the uniformity in terms of the extended distance

source

theorem emetric.mk_uniformity_basis {α : Type u} [emetric_space α] {β : Type u_1} {p : β → Prop} {f : β → ennreal} :

(∀ (x : β), p x → 0 < f x) → (∀ (ε : ennreal), 0 < ε → (∃ (x : β) (hx : p x), f x ≤ ε)) → (uniformity α).has_basis p (λ (x : β), {p : α × α | has_edist.edist p.fst p.snd < f x})

Given f : β → ennreal, 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_edist, uniformity_basis_edist', uniformity_basis_edist_nnreal, and uniformity_basis_edist_inv_nat.

source

theorem emetric.mk_uniformity_basis_le {α : Type u} [emetric_space α] {β : Type u_1} {p : β → Prop} {f : β → ennreal} :

(∀ (x : β), p x → 0 < f x) → (∀ (ε : ennreal), 0 < ε → (∃ (x : β) (hx : p x), f x ≤ ε)) → (uniformity α).has_basis p (λ (x : β), {p : α × α | has_edist.edist p.fst p.snd ≤ f x})

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

For specific bases see uniformity_basis_edist_le and uniformity_basis_edist_le'.

source

theorem uniformity_basis_edist_le {α : Type u} [emetric_space α] :

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

source

theorem uniformity_basis_edist' {α : Type u} [emetric_space α] (ε' : ennreal) :

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

source

theorem uniformity_basis_edist_le' {α : Type u} [emetric_space α] (ε' : ennreal) :

0 < ε' → (uniformity α).has_basis (λ (ε : ennreal), ε ∈ set.Ioo 0 ε') (λ (ε : ennreal), {p : α × α | has_edist.edist p.fst p.snd ≤ ε})

source

theorem uniformity_basis_edist_nnreal {α : Type u} [emetric_space α] :

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

source

theorem uniformity_basis_edist_inv_nat {α : Type u} [emetric_space α] :

(uniformity α).has_basis (λ (_x : ℕ), true) (λ (n : ℕ), {p : α × α | has_edist.edist p.fst p.snd < (↑n)⁻¹})

source

theorem edist_mem_uniformity {α : Type u} [emetric_space α] {ε : ennreal} :

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

Fixed size neighborhoods of the diagonal belong to the uniform structure

source

theorem emetric.uniformity_has_countable_basis {α : Type u} [emetric_space α] :

(uniformity α).is_countably_generated

source

theorem emetric.uniform_continuous_iff {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {f : α → β} :

uniform_continuous f ↔ ∀ (ε : ennreal), ε > 0 → (∃ (δ : ennreal) (H : δ > 0), ∀ {a b : α}, has_edist.edist a b < δ → has_edist.edist (f a) (f b) < ε)

ε-δ characterization of uniform continuity on emetric spaces

source

theorem emetric.uniform_embedding_iff {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {f : α → β} :

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

ε-δ characterization of uniform embeddings on emetric spaces

source

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

uniform_embedding f ↔ (∀ (ε : ennreal), ε > 0 → (∃ (δ : ennreal) (H : δ > 0), ∀ {a b : α}, has_edist.edist a b < δ → has_edist.edist (f a) (f b) < ε)) ∧ ∀ (δ : ennreal), δ > 0 → (∃ (ε : ennreal) (H : ε > 0), ∀ {a b : α}, has_edist.edist (f a) (f b) < ε → has_edist.edist a b < δ)

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

source

theorem emetric.cauchy_iff {α : Type u} [emetric_space α] {f : filter α} :

cauchy f ↔ f ≠ ⊥ ∧ ∀ (ε : ennreal), ε > 0 → (∃ (t : set α) (H : t ∈ f), ∀ (x y : α), x ∈ t → y ∈ t → has_edist.edist x y < ε)

ε-δ characterization of Cauchy sequences on emetric spaces

source

theorem emetric.complete_of_convergent_controlled_sequences {α : Type u} [emetric_space α] (B : ℕ → ennreal) :

(∀ (n : ℕ), 0 < B n) → (∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → has_edist.edist (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 edist (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 emetric.complete_of_cauchy_seq_tendsto {α : Type u} [emetric_space α] :

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

A sequentially complete emetric space is complete.

source

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

tendsto_locally_uniformly_on F f p s ↔ ∀ (ε : ennreal), ε > 0 → ∀ (x : β), x ∈ s → (∃ (t : set β) (H : t ∈ nhds_within x s), ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → has_edist.edist (f y) (F n y) < ε)

Expressing locally uniform convergence on a set using edist.

source

theorem emetric.tendsto_uniformly_on_iff {α : Type u} {β : Type v} [emetric_space α] {ι : Type u_1} {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :

tendsto_uniformly_on F f p s ↔ ∀ (ε : ennreal), ε > 0 → (∀ᶠ (n : ι) in p, ∀ (x : β), x ∈ s → has_edist.edist (f x) (F n x) < ε)

Expressing uniform convergence on a set using edist.

source

theorem emetric.tendsto_locally_uniformly_iff {α : Type u} {β : Type v} [emetric_space α] {ι : Type u_1} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} :

tendsto_locally_uniformly F f p ↔ ∀ (ε : ennreal), ε > 0 → ∀ (x : β), ∃ (t : set β) (H : t ∈ nhds x), ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → has_edist.edist (f y) (F n y) < ε

Expressing locally uniform convergence using edist.

source

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

tendsto_uniformly F f p ↔ ∀ (ε : ennreal), ε > 0 → (∀ᶠ (n : ι) in p, ∀ (x : β), has_edist.edist (f x) (F n x) < ε)

Expressing uniform convergence using edist.

source

@[instance]

def to_separated {α : Type u} [emetric_space α] :

separated_space α

An emetric space is separated

Equations

to_separated = _

source

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

uniformity α = uniformity α → emetric_space α

Auxiliary function to replace the uniformity on an emetric space with a uniformity which is equal to the original one, but maybe not defeq. This is useful if one wants to construct an emetric space with a specified uniformity. See Note [forgetful inheritance] explaining why having definitionally the right uniformity is often important.

Equations

m.replace_uniformity H = {to_has_edist := {edist := has_edist.edist emetric_space.to_has_edist}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := U, uniformity_edist := _}

source

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

function.injective f → emetric_space β → emetric_space α

The extended metric induced by an injective function taking values in an emetric space.

Equations

emetric_space.induced f hf m = {to_has_edist := {edist := λ (x y : α), has_edist.edist (f x) (f y)}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := uniform_space.comap f emetric_space.to_uniform_space, uniformity_edist := _}

source

@[instance]

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

emetric_space (subtype p)

Emetric space instance on subsets of emetric spaces

Equations

subtype.emetric_space = emetric_space.induced coe subtype.emetric_space._proof_1 t

source

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

has_edist.edist x y = has_edist.edist ↑x ↑y

The extended distance on a subset of an emetric space is the restriction of the original distance, by definition

source

@[instance]

def prod.emetric_space_max {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] :

emetric_space (α × β)

The product of two emetric spaces, with the max distance, is an extended metric spaces. We make sure that the uniform structure thus constructed is the one corresponding to the product of uniform spaces, to avoid diamond problems.

Equations

prod.emetric_space_max = {to_has_edist := {edist := λ (x y : α × β), max (has_edist.edist x.fst y.fst) (has_edist.edist x.snd y.snd)}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := prod.uniform_space emetric_space.to_uniform_space', uniformity_edist := _}

source

theorem prod.edist_eq {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] (x y : α × β) :

has_edist.edist x y = max (has_edist.edist x.fst y.fst) (has_edist.edist x.snd y.snd)

source

@[instance]

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

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

The product of a finite number of emetric spaces, with the max distance, is still an emetric space. This construction would also work for infinite products, but it would not give rise to the product topology. Hence, we only formalize it in the good situation of finitely many spaces.

Equations

emetric_space_pi = {to_has_edist := {edist := λ (f g : Π (b : β), π b), finset.univ.sup (λ (b : β), has_edist.edist (f b) (g b))}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := Pi.uniform_space (λ (b : β), π b) (λ (i : β), emetric_space.to_uniform_space'), uniformity_edist := _}

source

def emetric.ball {α : Type u} [emetric_space α] :

α → ennreal → set α

emetric.ball x ε is the set of all points y with edist y x < ε

Equations

emetric.ball x ε = {y : α | has_edist.edist y x < ε}

source

@[simp]

theorem emetric.mem_ball {α : Type u} [emetric_space α] {x y : α} {ε : ennreal} :

y ∈ emetric.ball x ε ↔ has_edist.edist y x < ε

source

theorem emetric.mem_ball' {α : Type u} [emetric_space α] {x y : α} {ε : ennreal} :

y ∈ emetric.ball x ε ↔ has_edist.edist x y < ε

source

def emetric.closed_ball {α : Type u} [emetric_space α] :

α → ennreal → set α

emetric.closed_ball x ε is the set of all points y with edist y x ≤ ε

Equations

emetric.closed_ball x ε = {y : α | has_edist.edist y x ≤ ε}

source

@[simp]

theorem emetric.mem_closed_ball {α : Type u} [emetric_space α] {x y : α} {ε : ennreal} :

y ∈ emetric.closed_ball x ε ↔ has_edist.edist y x ≤ ε

source

theorem emetric.ball_subset_closed_ball {α : Type u} [emetric_space α] {x : α} {ε : ennreal} :

emetric.ball x ε ⊆ emetric.closed_ball x ε

source

theorem emetric.pos_of_mem_ball {α : Type u} [emetric_space α] {x y : α} {ε : ennreal} :

y ∈ emetric.ball x ε → 0 < ε

source

theorem emetric.mem_ball_self {α : Type u} [emetric_space α] {x : α} {ε : ennreal} :

0 < ε → x ∈ emetric.ball x ε

source

theorem emetric.mem_closed_ball_self {α : Type u} [emetric_space α] {x : α} {ε : ennreal} :

x ∈ emetric.closed_ball x ε

source

theorem emetric.mem_ball_comm {α : Type u} [emetric_space α] {x y : α} {ε : ennreal} :

x ∈ emetric.ball y ε ↔ y ∈ emetric.ball x ε

source

theorem emetric.ball_subset_ball {α : Type u} [emetric_space α] {x : α} {ε₁ ε₂ : ennreal} :

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

source

theorem emetric.closed_ball_subset_closed_ball {α : Type u} [emetric_space α] {x : α} {ε₁ ε₂ : ennreal} :

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

source

theorem emetric.ball_disjoint {α : Type u} [emetric_space α] {x y : α} {ε₁ ε₂ : ennreal} :

ε₁ + ε₂ ≤ has_edist.edist x y → emetric.ball x ε₁ ∩ emetric.ball y ε₂ = ∅

source

theorem emetric.ball_subset {α : Type u} [emetric_space α] {x y : α} {ε₁ ε₂ : ennreal} :

has_edist.edist x y + ε₁ ≤ ε₂ → has_edist.edist x y < ⊤ → emetric.ball x ε₁ ⊆ emetric.ball y ε₂

source

theorem emetric.exists_ball_subset_ball {α : Type u} [emetric_space α] {x y : α} {ε : ennreal} :

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

source

theorem emetric.ball_eq_empty_iff {α : Type u} [emetric_space α] {x : α} {ε : ennreal} :

emetric.ball x ε = ∅ ↔ ε = 0

source

def emetric.edist_lt_top_setoid {α : Type u} [emetric_space α] :

setoid α

Relation “two points are at a finite edistance” is an equivalence relation.

Equations

emetric.edist_lt_top_setoid = {r := λ (x y : α), has_edist.edist x y < ⊤, iseqv := _}

source

@[simp]

theorem emetric.ball_zero {α : Type u} [emetric_space α] {x : α} :

emetric.ball x 0 = ∅

source

theorem emetric.nhds_basis_eball {α : Type u} [emetric_space α] {x : α} :

(nhds x).has_basis (λ (ε : ennreal), 0 < ε) (emetric.ball x)

source

theorem emetric.nhds_basis_closed_eball {α : Type u} [emetric_space α] {x : α} :

(nhds x).has_basis (λ (ε : ennreal), 0 < ε) (emetric.closed_ball x)

source

theorem emetric.nhds_eq {α : Type u} [emetric_space α] {x : α} :

nhds x = ⨅ (ε : ennreal) (H : ε > 0), filter.principal (emetric.ball x ε)

source

theorem emetric.mem_nhds_iff {α : Type u} [emetric_space α] {x : α} {s : set α} :

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

source

theorem emetric.is_open_iff {α : Type u} [emetric_space α] {s : set α} :

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

source

theorem emetric.is_open_ball {α : Type u} [emetric_space α] {x : α} {ε : ennreal} :

is_open (emetric.ball x ε)

source

theorem emetric.is_closed_ball_top {α : Type u} [emetric_space α] {x : α} :

is_closed (emetric.ball x ⊤)

source

theorem emetric.ball_mem_nhds {α : Type u} [emetric_space α] (x : α) {ε : ennreal} :

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

source

theorem emetric.mem_closure_iff {α : Type u} [emetric_space α] {x : α} {s : set α} :

x ∈ closure s ↔ ∀ (ε : ennreal), ε > 0 → (∃ (y : α) (H : y ∈ s), has_edist.edist x y < ε)

ε-characterization of the closure in emetric spaces

source

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

filter.tendsto u f (nhds a) ↔ ∀ (ε : ennreal), ε > 0 → (∀ᶠ (x : β) in f, has_edist.edist (u x) a < ε)

source

theorem emetric.tendsto_at_top {α : Type u} {β : Type v} [emetric_space α] [nonempty β] [semilattice_sup β] (u : β → α) {a : α} :

filter.tendsto u filter.at_top (nhds a) ↔ ∀ (ε : ennreal), ε > 0 → (∃ (N : β), ∀ (n : β), n ≥ N → has_edist.edist (u n) a < ε)

source

@[nolint]

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

cauchy_seq u ↔ ∀ (ε : ennreal), ε > 0 → (∃ (N : β), ∀ (m n : β), m ≥ N → n ≥ N → has_edist.edist (u m) (u n) < ε)

In an emetric space, Cauchy sequences are characterized by the fact that, eventually, the edistance between its elements is arbitrarily small

source

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

cauchy_seq u ↔ ∀ (ε : ennreal), ε > 0 → (∃ (N : β), ∀ (n : β), n ≥ N → has_edist.edist (u n) (u N) < ε)

A variation around the emetric characterization of Cauchy sequences

source

theorem emetric.cauchy_seq_iff_nnreal {α : Type u} {β : Type v} [emetric_space α] [nonempty β] [semilattice_sup β] {u : β → α} :

cauchy_seq u ↔ ∀ (ε : nnreal), 0 < ε → (∃ (N : β), ∀ (n : β), N ≤ n → has_edist.edist (u n) (u N) < ↑ε)

A variation of the emetric characterization of Cauchy sequences that deals with nnreal upper bounds.

source

theorem emetric.totally_bounded_iff {α : Type u} [emetric_space α] {s : set α} :

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

source

theorem emetric.totally_bounded_iff' {α : Type u} [emetric_space α] {s : set α} :

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

source

theorem emetric.countable_closure_of_compact {α : Type u} [emetric_space α] {s : set α} :

is_compact s → (∃ (t : set α) (H : t ⊆ s), t.countable ∧ s = closure t)

A compact set in an emetric space is separable, i.e., it is the closure of a countable set

source

@[instance]

def emetric.topological_space.first_countable_topology (α : Type u) [emetric_space α] :

topological_space.first_countable_topology α

Equations

_ = _

source

theorem emetric.second_countable_of_separable (α : Type u) [emetric_space α] [topological_space.separable_space α] :

topological_space.second_countable_topology α

A separable emetric space is second countable: one obtains a countable basis by taking the balls centered at points in a dense subset, and with rational radii. We do not register this as an instance, as there is already an instance going in the other direction from second countable spaces to separable spaces, and we want to avoid loops.

source

def emetric.diam {α : Type u} [emetric_space α] :

set α → ennreal

The diameter of a set in an emetric space, named emetric.diam

Equations

emetric.diam s = ⨆ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), has_edist.edist x y

source

theorem emetric.diam_le_iff_forall_edist_le {α : Type u} [emetric_space α] {s : set α} {d : ennreal} :

emetric.diam s ≤ d ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_edist.edist x y ≤ d

source

theorem emetric.edist_le_diam_of_mem {α : Type u} [emetric_space α] {x y : α} {s : set α} :

x ∈ s → y ∈ s → has_edist.edist x y ≤ emetric.diam s

If two points belong to some set, their edistance is bounded by the diameter of the set

source

theorem emetric.diam_le_of_forall_edist_le {α : Type u} [emetric_space α] {s : set α} {d : ennreal} :

(∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_edist.edist x y ≤ d) → emetric.diam s ≤ d

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

source

theorem emetric.diam_subsingleton {α : Type u} [emetric_space α] {s : set α} :

s.subsingleton → emetric.diam s = 0

The diameter of a subsingleton vanishes.

source

@[simp]

theorem emetric.diam_empty {α : Type u} [emetric_space α] :

emetric.diam ∅ = 0

The diameter of the empty set vanishes

source

@[simp]

theorem emetric.diam_singleton {α : Type u} [emetric_space α] {x : α} :

emetric.diam {x} = 0

The diameter of a singleton vanishes

source

theorem emetric.diam_eq_zero_iff {α : Type u} [emetric_space α] {s : set α} :

emetric.diam s = 0 ↔ s.subsingleton

source

theorem emetric.diam_pos_iff {α : Type u} [emetric_space α] {s : set α} :

0 < emetric.diam s ↔ ∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x ≠ y

source

theorem emetric.diam_insert {α : Type u} [emetric_space α] {x : α} {s : set α} :

emetric.diam (has_insert.insert x s) = max (⨆ (y : α) (H : y ∈ s), has_edist.edist x y) (emetric.diam s)

source

theorem emetric.diam_pair {α : Type u} [emetric_space α] {x y : α} :

emetric.diam {x, y} = has_edist.edist x y

source

theorem emetric.diam_triple {α : Type u} [emetric_space α] {x y z : α} :

emetric.diam {x, y, z} = max (max (has_edist.edist x y) (has_edist.edist x z)) (has_edist.edist y z)

source

theorem emetric.diam_mono {α : Type u} [emetric_space α] {s t : set α} :

s ⊆ t → emetric.diam s ≤ emetric.diam t

The diameter is monotonous with respect to inclusion

source

theorem emetric.diam_union {α : Type u} [emetric_space α] {x y : α} {s t : set α} :

x ∈ s → y ∈ t → emetric.diam (s ∪ t) ≤ emetric.diam s + has_edist.edist x y + emetric.diam t

The diameter of a union is controlled by the diameter of the sets, and the edistance between two points in the sets.

source

theorem emetric.diam_union' {α : Type u} [emetric_space α] {s t : set α} :

(s ∩ t).nonempty → emetric.diam (s ∪ t) ≤ emetric.diam s + emetric.diam t

source

theorem emetric.diam_closed_ball {α : Type u} [emetric_space α] {x : α} {r : ennreal} :

emetric.diam (emetric.closed_ball x r) ≤ 2 * r

source

theorem emetric.diam_ball {α : Type u} [emetric_space α] {x : α} {r : ennreal} :

emetric.diam (emetric.ball x r) ≤ 2 * r

mathlib documentation

topology.metric_space.emetric_space

Extended metric spaces

General documentation

Additional documentation

Library

mathlib documentation

topology.​metric_space.​emetric_space

Extended metric spaces

General documentation

Additional documentation

Library

topology.metric_space.emetric_space