Documentation

Mathlib.Topology.EMetricSpace.Basic

Extended metric spaces #

Further results about extended metric spaces.

theorem edist_le_Ico_sum_edist {α : Type u} [PseudoEMetricSpace α] (f : α) {m : } {n : } (h : m n) :
edist (f m) (f n) iFinset.Ico m n, edist (f i) (f (i + 1))

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

theorem edist_le_range_sum_edist {α : Type u} [PseudoEMetricSpace α] (f : α) (n : ) :
edist (f 0) (f n) iFinset.range n, edist (f i) (f (i + 1))

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

theorem edist_le_Ico_sum_of_edist_le {α : Type u} [PseudoEMetricSpace α] {f : α} {m : } {n : } (hmn : m n) {d : ENNReal} (hd : ∀ {k : }, m kk < nedist (f k) (f (k + 1)) d k) :
edist (f m) (f n) iFinset.Ico m n, d i

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

theorem edist_le_range_sum_of_edist_le {α : Type u} [PseudoEMetricSpace α] {f : α} (n : ) {d : ENNReal} (hd : ∀ {k : }, k < nedist (f k) (f (k + 1)) d k) :
edist (f 0) (f n) iFinset.range n, d i

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

theorem EMetric.isUniformInducing_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} :
IsUniformInducing f UniformContinuous f δ > 0, ε > 0, ∀ {a b : α}, edist (f a) (f b) < εedist a b < δ
@[deprecated EMetric.isUniformInducing_iff]
theorem EMetric.uniformInducing_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} :
IsUniformInducing f UniformContinuous f δ > 0, ε > 0, ∀ {a b : α}, edist (f a) (f b) < εedist a b < δ

Alias of EMetric.isUniformInducing_iff.

theorem EMetric.isUniformEmbedding_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} :
IsUniformEmbedding f Function.Injective f UniformContinuous f δ > 0, ε > 0, ∀ {a b : α}, edist (f a) (f b) < εedist a b < δ

ε-δ characterization of uniform embeddings on pseudoemetric spaces

@[deprecated EMetric.isUniformEmbedding_iff]
theorem EMetric.uniformEmbedding_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} :
IsUniformEmbedding f Function.Injective f UniformContinuous f δ > 0, ε > 0, ∀ {a b : α}, edist (f a) (f b) < εedist a b < δ

Alias of EMetric.isUniformEmbedding_iff.


ε-δ characterization of uniform embeddings on pseudoemetric spaces

theorem EMetric.controlled_of_isUniformEmbedding {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} (h : IsUniformEmbedding f) :
(∀ ε > 0, δ > 0, ∀ {a b : α}, edist a b < δedist (f a) (f b) < ε) δ > 0, ε > 0, ∀ {a b : α}, edist (f a) (f b) < εedist a b < δ

If a map between pseudoemetric spaces is a uniform embedding then the edistance between f x and f y is controlled in terms of the distance between x and y.

In fact, this lemma holds for a IsUniformInducing map. TODO: generalize?

@[deprecated EMetric.controlled_of_isUniformEmbedding]
theorem EMetric.controlled_of_uniformEmbedding {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} (h : IsUniformEmbedding f) :
(∀ ε > 0, δ > 0, ∀ {a b : α}, edist a b < δedist (f a) (f b) < ε) δ > 0, ε > 0, ∀ {a b : α}, edist (f a) (f b) < εedist a b < δ

Alias of EMetric.controlled_of_isUniformEmbedding.


If a map between pseudoemetric spaces is a uniform embedding then the edistance between f x and f y is controlled in terms of the distance between x and y.

In fact, this lemma holds for a IsUniformInducing map. TODO: generalize?

theorem EMetric.cauchy_iff {α : Type u} [PseudoEMetricSpace α] {f : Filter α} :
Cauchy f f ε > 0, tf, xt, yt, edist x y < ε

ε-δ characterization of Cauchy sequences on pseudoemetric spaces

theorem EMetric.complete_of_convergent_controlled_sequences {α : Type u} [PseudoEMetricSpace α] (B : ENNReal) (hB : ∀ (n : ), 0 < B n) (H : ∀ (u : α), (∀ (N n m : ), N nN medist (u n) (u m) < B N)∃ (x : α), Filter.Tendsto u Filter.atTop (nhds x)) :

A very useful criterion to show that a space is complete is to show that all sequences which satisfy a bound of the form 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.

theorem EMetric.complete_of_cauchySeq_tendsto {α : Type u} [PseudoEMetricSpace α] :
(∀ (u : α), CauchySeq u∃ (a : α), Filter.Tendsto u Filter.atTop (nhds a))CompleteSpace α

A sequentially complete pseudoemetric space is complete.

theorem EMetric.tendstoLocallyUniformlyOn_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] {ι : Type u_2} [TopologicalSpace β] {F : ιβα} {f : βα} {p : Filter ι} {s : Set β} :
TendstoLocallyUniformlyOn F f p s ε > 0, xs, tnhdsWithin x s, ∀ᶠ (n : ι) in p, yt, edist (f y) (F n y) < ε

Expressing locally uniform convergence on a set using edist.

theorem EMetric.tendstoUniformlyOn_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] {ι : Type u_2} {F : ιβα} {f : βα} {p : Filter ι} {s : Set β} :
TendstoUniformlyOn F f p s ε > 0, ∀ᶠ (n : ι) in p, xs, edist (f x) (F n x) < ε

Expressing uniform convergence on a set using edist.

theorem EMetric.tendstoLocallyUniformly_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] {ι : Type u_2} [TopologicalSpace β] {F : ιβα} {f : βα} {p : Filter ι} :
TendstoLocallyUniformly F f p ε > 0, ∀ (x : β), tnhds x, ∀ᶠ (n : ι) in p, yt, edist (f y) (F n y) < ε

Expressing locally uniform convergence using edist.

theorem EMetric.tendstoUniformly_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] {ι : Type u_2} {F : ιβα} {f : βα} {p : Filter ι} :
TendstoUniformly F f p ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε

Expressing uniform convergence using edist.

theorem EMetric.inseparable_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} :
theorem Inseparable.edist_eq_zero {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} :
Inseparable x yedist x y = 0

Alias of the forward direction of EMetric.inseparable_iff.

theorem EMetric.cauchySeq_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : βα} :
CauchySeq u ε > 0, ∃ (N : β), ∀ (m : β), N m∀ (n : β), N nedist (u m) (u n) < ε

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

theorem EMetric.cauchySeq_iff' {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : βα} :
CauchySeq u ε > 0, ∃ (N : β), nN, edist (u n) (u N) < ε

A variation around the emetric characterization of Cauchy sequences

theorem EMetric.cauchySeq_iff_NNReal {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : βα} :
CauchySeq u ∀ (ε : NNReal), 0 < ε∃ (N : β), ∀ (n : β), N nedist (u n) (u N) < ε

A variation of the emetric characterization of Cauchy sequences that deals with ℝ≥0 upper bounds.

theorem EMetric.totallyBounded_iff {α : Type u} [PseudoEMetricSpace α] {s : Set α} :
TotallyBounded s ε > 0, ∃ (t : Set α), t.Finite s yt, EMetric.ball y ε
theorem EMetric.totallyBounded_iff' {α : Type u} [PseudoEMetricSpace α] {s : Set α} :
TotallyBounded s ε > 0, ts, t.Finite s yt, EMetric.ball y ε
theorem EMetric.subset_countable_closure_of_compact {α : Type u} [PseudoEMetricSpace α] {s : Set α} (hs : IsCompact s) :
ts, t.Countable s closure t

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

@[instance 90]

A sigma compact pseudo emetric space has second countable topology.

Equations
  • =
theorem EMetric.secondCountable_of_almost_dense_set {α : Type u} [PseudoEMetricSpace α] (hs : ε > 0, ∃ (t : Set α), t.Countable xt, EMetric.closedBall x ε = Set.univ) :
@[instance 100]

An emetric space is separated

Equations
  • =
theorem EMetric.isUniformEmbedding_iff' {β : Type v} {γ : Type w} [EMetricSpace γ] [EMetricSpace β] {f : γβ} :
IsUniformEmbedding f (∀ ε > 0, δ > 0, ∀ {a b : γ}, edist a b < δedist (f a) (f b) < ε) δ > 0, ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε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.

@[deprecated EMetric.isUniformEmbedding_iff']
theorem EMetric.uniformEmbedding_iff' {β : Type v} {γ : Type w} [EMetricSpace γ] [EMetricSpace β] {f : γβ} :
IsUniformEmbedding f (∀ ε > 0, δ > 0, ∀ {a b : γ}, edist a b < δedist (f a) (f b) < ε) δ > 0, ε > 0, ∀ {a b : γ}, edist (f a) (f b) < εedist a b < δ

Alias of EMetric.isUniformEmbedding_iff'.


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.

@[reducible, inline]

If a PseudoEMetricSpace is a T₀ space, then it is an EMetricSpace.

Equations
Instances For
    instance Prod.emetricSpaceMax {β : Type v} {γ : Type w} [EMetricSpace γ] [EMetricSpace β] :

    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
    theorem EMetric.countable_closure_of_compact {γ : Type w} [EMetricSpace γ] {s : Set γ} (hs : IsCompact s) :
    ts, t.Countable s = closure t

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

    Separation quotient #

    Equations