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) ≤ ∑ i ∈ Finset.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) ≤ ∑ i ∈ Finset.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 ≤ k → k < n → dist (f k) (f (k + 1)) ≤ d k) : dist (f m) (f n) ≤ ∑ i ∈ Finset.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 < n → dist (f k) (f (k + 1)) ≤ d k) : dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i

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

theorem Metric.isUniformInducing_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : IsUniformInducing 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 < δ

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.

theorem Metric.totallyBounded_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, 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 y → dist ↑x ↑y < ε) : TotallyBounded s

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) (ε : ℝ) : ε > 0 → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

theorem Metric.tendstoUniformlyOnFilter_iff {α : Type u} {β : Type v} {ι : Type u_1} [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_1} [PseudoMetricSpace α] [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} : TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, 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_1} [PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} : TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε

Expressing uniform convergence on a set using dist.

theorem Metric.tendstoLocallyUniformly_iff {α : Type u} {β : Type v} {ι : Type u_1} [PseudoMetricSpace α] [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Expressing locally uniform convergence using dist.

theorem Metric.tendstoUniformly_iff {α : Type u} {β : Type v} {ι : Type u_1} [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, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, 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, 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, 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 : α} : Inseparable x y ↔ nndist x y = 0

theorem Inseparable.nndist_eq_zero {α : Type u} [PseudoMetricSpace α] {x y : α} : Inseparable x y → nndist 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 y → dist 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)

theorem Topology.IsInducing.isSeparable_preimage {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} [TopologicalSpace β] (hf : IsInducing f) {s : Set α} (hs : TopologicalSpace.IsSeparable s) : TopologicalSpace.IsSeparable (f ⁻¹' s)

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

theorem Topology.IsEmbedding.isSeparable_preimage {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} [TopologicalSpace β] (hf : IsEmbedding f) {s : Set α} (hs : TopologicalSpace.IsSeparable s) : TopologicalSpace.IsSeparable (f ⁻¹' s)

theorem IsCompact.isSeparable {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) : TopologicalSpace.IsSeparable s

A compact set is separable.

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

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

theorem finite_cover_balls_of_compact {X : Type u_2} [PseudoMetricSpace X] {s : Set X} (hs : IsCompact s) {e : ℝ} (he : 0 < e) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e

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

theorem IsCompact.finite_cover_balls {X : Type u_2} [PseudoMetricSpace X] {s : Set X} (hs : IsCompact s) {e : ℝ} (he : 0 < e) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e

Alias of finite_cover_balls_of_compact.

---

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

theorem exists_finite_cover_balls_of_isCompact_closure {X : Type u_2} [PseudoMetricSpace X] {s : Set X} {ε : ℝ} (hs : IsCompact (closure s)) (hε : 0 < ε) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x ε

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

theorem ContinuousOn.isSeparable_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hf : ContinuousOn f s) (hs : TopologicalSpace.IsSeparable s) : TopologicalSpace.IsSeparable (f '' s)

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