Documentation

Mathlib.Topology.MetricSpace.Pseudo.Basic

Pseudo-metric spaces #

Further results about pseudo-metric spaces.

theorem dist_le_Ico_sum_dist {α : Type u} [PseudoMetricSpace α] (f : α) {m : } {n : } (h : m n) :
dist (f m) (f n) iFinset.Ico m n, dist (f i) (f (i + 1))

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

theorem dist_le_range_sum_dist {α : Type u} [PseudoMetricSpace α] (f : α) (n : ) :
dist (f 0) (f n) iFinset.range n, dist (f i) (f (i + 1))

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

theorem dist_le_Ico_sum_of_dist_le {α : Type u} [PseudoMetricSpace α] {f : α} {m : } {n : } (hmn : m n) {d : } (hd : ∀ {k : }, m kk < ndist (f k) (f (k + 1)) d k) :
dist (f m) (f n) iFinset.Ico m n, d i

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

theorem dist_le_range_sum_of_dist_le {α : Type u} [PseudoMetricSpace α] {f : α} (n : ) {d : } (hd : ∀ {k : }, k < ndist (f k) (f (k + 1)) d k) :
dist (f 0) (f n) iFinset.range n, d i

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

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

Alias of Metric.isUniformEmbedding_iff.

theorem Metric.controlled_of_isUniformEmbedding {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} (h : IsUniformEmbedding f) :
(∀ ε > 0, δ > 0, ∀ {a b : α}, dist a b < δdist (f a) (f b) < ε) δ > 0, ε > 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.

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

Alias of Metric.controlled_of_isUniformEmbedding.


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

theorem Metric.totallyBounded_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} :
TotallyBounded s ε > 0, ∃ (t : Set α), t.Finite s yt, Metric.ball y ε
theorem Metric.totallyBounded_of_finite_discretization {α : Type u} [PseudoMetricSpace α] {s : Set α} (H : ε > 0, ∃ (β : Type u) (x : Fintype β) (F : sβ), ∀ (x y : s), F x = F ydist x y < ε) :

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

theorem Metric.finite_approx_of_totallyBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : TotallyBounded s) (ε : ) :
ε > 0ts, t.Finite s yt, Metric.ball y ε
theorem Metric.tendstoUniformlyOnFilter_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] {F : ιβα} {f : βα} {p : Filter ι} {p' : Filter β} :
TendstoUniformlyOnFilter F f p p' ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε

Expressing uniform convergence using dist

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

Expressing locally uniform convergence on a set using dist.

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

Expressing uniform convergence on a set using dist.

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

Expressing locally uniform convergence using dist.

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

Expressing uniform convergence using dist.

theorem Metric.cauchy_iff {α : Type u} [PseudoMetricSpace α] {f : Filter α} :
Cauchy f f.NeBot ε > 0, tf, xt, yt, dist x y < ε
theorem Metric.exists_ball_inter_eq_singleton_of_mem_discrete {α : Type u} [PseudoMetricSpace α] {s : Set α} [DiscreteTopology s] {x : α} (hx : x s) :
ε > 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.

theorem Metric.exists_closedBall_inter_eq_singleton_of_discrete {α : Type u} [PseudoMetricSpace α] {s : Set α} [DiscreteTopology s] {x : α} (hx : x s) :
ε > 0, Metric.closedBall 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.

theorem Metric.inseparable_iff_nndist {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} :
theorem Inseparable.nndist_eq_zero {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} :
Inseparable x ynndist x y = 0

Alias of the forward direction of Metric.inseparable_iff_nndist.

theorem Metric.inseparable_iff {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} :
Inseparable x y dist x y = 0
theorem Inseparable.dist_eq_zero {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} :
Inseparable x ydist x y = 0

Alias of the forward direction of Metric.inseparable_iff.

theorem tendsto_nhds_unique_dist {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} {l : Filter β} {x : α} {y : α} [l.NeBot] (ha : Filter.Tendsto f l (nhds x)) (hb : Filter.Tendsto f l (nhds y)) :
dist x y = 0

A weaker version of tendsto_nhds_unique for PseudoMetricSpace.

theorem cauchySeq_iff_tendsto_dist_atTop_0 {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : βα} :
CauchySeq u Filter.Tendsto (fun (n : β × β) => dist (u n.1) (u n.2)) Filter.atTop (nhds 0)

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

A compact set is separable.

theorem Metric.secondCountable_of_almost_dense_set {α : Type u} [PseudoMetricSpace α] (H : ε > 0, ∃ (s : Set α), s.Countable ∀ (x : α), ys, dist x y ε) :

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