Boundedness in (pseudo)-metric spaces

This file contains one definition, and various results on boundedness in pseudo-metric spaces.

• Metric.diam s : The iSup of the distances of members of s. Defined in terms of EMetric.diam, for better handling of the case when it should be infinite.

• isBounded_iff_subset_closedBall: a non-empty set is bounded if and only if it is is included in some closed ball

• describing the cobounded filter, relating to the cocompact filter

• IsCompact.isBounded: compact sets are bounded

• TotallyBounded.isBounded: totally bounded sets are bounded

• isCompact_iff_isClosed_bounded, the Heine–Borel theorem: in a proper space, a set is compact if and only if it is closed and bounded.

• cobounded_eq_cocompact: in a proper space, cobounded and compact sets are the same diameter of a subset, and its relation to boundedness

Tags

metric, pseudo_metric, bounded, diameter, Heine-Borel theorem

theorem Metric.isBounded_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} : Bornology.IsBounded (Metric.closedBall x r)

Closed balls are bounded

theorem Metric.isBounded_ball {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} : Bornology.IsBounded (Metric.ball x r)

Open balls are bounded

theorem Metric.isBounded_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} : Bornology.IsBounded (Metric.sphere x r)

Spheres are bounded

theorem Metric.isBounded_iff_subset_closedBall {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : α) : Bornology.IsBounded s ↔ ∃ (r : ℝ), s ⊆ Metric.closedBall c r

Given a point, a bounded subset is included in some ball around this point

theorem Bornology.IsBounded.subset_closedBall {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (c : α) : ∃ (r : ℝ), s ⊆ Metric.closedBall c r

theorem Bornology.IsBounded.subset_ball_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (a : ℝ) (c : α) : ∃ (r : ℝ), a < r ∧ s ⊆ Metric.ball c r

theorem Bornology.IsBounded.subset_ball {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (c : α) : ∃ (r : ℝ), s ⊆ Metric.ball c r

theorem Metric.isBounded_iff_subset_ball {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : α) : Bornology.IsBounded s ↔ ∃ (r : ℝ), s ⊆ Metric.ball c r

theorem Bornology.IsBounded.subset_closedBall_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (a : ℝ) (c : α) : ∃ (r : ℝ), a < r ∧ s ⊆ Metric.closedBall c r

theorem Metric.isBounded_closure_of_isBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) : Bornology.IsBounded (closure s)

theorem Bornology.IsBounded.closure {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) : Bornology.IsBounded (closure s)

@[simp]

theorem Metric.isBounded_closure_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded (closure s) ↔ Bornology.IsBounded s

theorem Metric.hasBasis_cobounded_compl_closedBall {α : Type u} [PseudoMetricSpace α] (c : α) : Filter.HasBasis (Bornology.cobounded α) (fun (x : ℝ) => True) fun (r : ℝ) => (Metric.closedBall c r)ᶜ

theorem Metric.hasBasis_cobounded_compl_ball {α : Type u} [PseudoMetricSpace α] (c : α) : Filter.HasBasis (Bornology.cobounded α) (fun (x : ℝ) => True) fun (r : ℝ) => (Metric.ball c r)ᶜ

@[simp]

theorem Metric.comap_dist_right_atTop {α : Type u} [PseudoMetricSpace α] (c : α) : Filter.comap (fun (x : α) => dist x c) Filter.atTop = Bornology.cobounded α

@[simp]

theorem Metric.comap_dist_left_atTop {α : Type u} [PseudoMetricSpace α] (c : α) : Filter.comap (dist c) Filter.atTop = Bornology.cobounded α

@[simp]

theorem Metric.tendsto_dist_right_atTop_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] (c : α) {f : β → α} {l : Filter β} : Filter.Tendsto (fun (x : β) => dist (f x) c) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded α)

@[simp]

theorem Metric.tendsto_dist_left_atTop_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] (c : α) {f : β → α} {l : Filter β} : Filter.Tendsto (fun (x : β) => dist c (f x)) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded α)

theorem Metric.tendsto_dist_right_cobounded_atTop {α : Type u} [PseudoMetricSpace α] (c : α) : Filter.Tendsto (fun (x : α) => dist x c) (Bornology.cobounded α) Filter.atTop

theorem Metric.tendsto_dist_left_cobounded_atTop {α : Type u} [PseudoMetricSpace α] (c : α) : Filter.Tendsto (dist c) (Bornology.cobounded α) Filter.atTop

theorem TotallyBounded.isBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : TotallyBounded s) : Bornology.IsBounded s

A totally bounded set is bounded

theorem IsCompact.isBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : IsCompact s) : Bornology.IsBounded s

A compact set is bounded

theorem Metric.cobounded_le_cocompact {α : Type u} [PseudoMetricSpace α] : Bornology.cobounded α ≤ Filter.cocompact α

theorem Metric.isCobounded_iff_closedBall_compl_subset {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : α) : Bornology.IsCobounded s ↔ ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s

theorem Bornology.IsCobounded.closedBall_compl_subset {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Bornology.IsCobounded s) (c : α) : ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s

theorem Metric.closedBall_compl_subset_of_mem_cocompact {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : s ∈ Filter.cocompact α) (c : α) : ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s

theorem Metric.mem_cocompact_of_closedBall_compl_subset {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (c : α) (h : ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s) : s ∈ Filter.cocompact α

theorem Metric.mem_cocompact_iff_closedBall_compl_subset {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (c : α) : s ∈ Filter.cocompact α ↔ ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s

theorem Metric.isBounded_range_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} : Bornology.IsBounded (Set.range f) ↔ ∃ (C : ℝ), ∀ (x y : β), dist (f x) (f y) ≤ C

Characterization of the boundedness of the range of a function

theorem Metric.isBounded_image_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {s : Set β} : Bornology.IsBounded (f '' s) ↔ ∃ (C : ℝ), ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C

theorem Metric.isBounded_range_of_tendsto_cofinite_uniformity {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} (hf : Filter.Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (uniformity α)) : Bornology.IsBounded (Set.range f)

theorem Metric.isBounded_range_of_cauchy_map_cofinite {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} (hf : Cauchy (Filter.map f Filter.cofinite)) : Bornology.IsBounded (Set.range f)

theorem CauchySeq.isBounded_range {α : Type u} [PseudoMetricSpace α] {f : ℕ → α} (hf : CauchySeq f) : Bornology.IsBounded (Set.range f)

theorem Metric.isBounded_range_of_tendsto_cofinite {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {a : α} (hf : Filter.Tendsto f Filter.cofinite (nhds a)) : Bornology.IsBounded (Set.range f)

theorem Metric.isBounded_of_compactSpace {α : Type u} [PseudoMetricSpace α] {s : Set α} [CompactSpace α] : Bornology.IsBounded s

In a compact space, all sets are bounded

theorem Metric.isBounded_range_of_tendsto {α : Type u} [PseudoMetricSpace α] (u : ℕ → α) {x : α} (hu : Filter.Tendsto u Filter.atTop (nhds x)) : Bornology.IsBounded (Set.range u)

theorem Metric.disjoint_nhds_cobounded {α : Type u} [PseudoMetricSpace α] (x : α) : Disjoint (nhds x) (Bornology.cobounded α)

theorem Metric.disjoint_cobounded_nhds {α : Type u} [PseudoMetricSpace α] (x : α) : Disjoint (Bornology.cobounded α) (nhds x)

theorem Metric.disjoint_nhdsSet_cobounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) : Disjoint (nhdsSet s) (Bornology.cobounded α)

theorem Metric.disjoint_cobounded_nhdsSet {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) : Disjoint (Bornology.cobounded α) (nhdsSet s)

theorem Metric.exists_isBounded_image_of_tendsto {α : Type u_3} {β : Type u_4} [PseudoMetricSpace β] {l : Filter α} {f : α → β} {x : β} (hf : Filter.Tendsto f l (nhds x)) : ∃ s ∈ l, Bornology.IsBounded (f '' s)

theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {s : Set β} {f : β → α} (hk : IsCompact k) (hf : ∀ x ∈ k, ContinuousWithinAt f s x) : ∃ (t : Set β), k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

If a function is continuous within a set s at every point of a compact set k, then it is bounded on some open neighborhood of k in s.

theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {f : β → α} (hk : IsCompact k) (hf : ∀ x ∈ k, ContinuousAt f x) : ∃ (t : Set β), k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)

If a function is continuous at every point of a compact set k, then it is bounded on some open neighborhood of k.

theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {s : Set β} {f : β → α} (hk : IsCompact k) (hks : k ⊆ s) (hf : ContinuousOn f s) : ∃ (t : Set β), k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

If a function is continuous on a set s containing a compact set k, then it is bounded on some open neighborhood of k in s.

theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {s : Set β} {f : β → α} (hk : IsCompact k) (hs : IsOpen s) (hks : k ⊆ s) (hf : ContinuousOn f s) : ∃ (t : Set β), k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)

If a function is continuous on a neighborhood of a compact set k, then it is bounded on some open neighborhood of k.

theorem Metric.isCompact_of_isClosed_isBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (hc : IsClosed s) (hb : Bornology.IsBounded s) : IsCompact s

The Heine–Borel theorem: In a proper space, a closed bounded set is compact.

theorem Bornology.IsBounded.isCompact_closure {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (h : Bornology.IsBounded s) : IsCompact (closure s)

The Heine–Borel theorem: In a proper space, the closure of a bounded set is compact.

theorem Metric.isCompact_iff_isClosed_bounded {α : Type u} [PseudoMetricSpace α] {s : Set α} [T2Space α] [ProperSpace α] : IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s

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

theorem Metric.compactSpace_iff_isBounded_univ {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : CompactSpace α ↔ Bornology.IsBounded Set.univ

theorem Metric.isBounded_Icc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : Bornology.IsBounded (Set.Icc a b)

theorem Metric.isBounded_Ico {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : Bornology.IsBounded (Set.Ico a b)

theorem Metric.isBounded_Ioc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : Bornology.IsBounded (Set.Ioc a b)

theorem Metric.isBounded_Ioo {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : Bornology.IsBounded (Set.Ioo a b)

theorem Metric.isBounded_of_bddAbove_of_bddBelow {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] {s : Set α} (h₁ : BddAbove s) (h₂ : BddBelow s) : Bornology.IsBounded s

In a pseudo metric space with a conditionally complete linear order such that the order and the metric structure give the same topology, any order-bounded set is metric-bounded.

noncomputable def Metric.diam {α : Type u} [PseudoMetricSpace α] (s : 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.diam

Equations

• Metric.diam s = (EMetric.diam s).toReal

theorem Metric.diam_nonneg {α : Type u} [PseudoMetricSpace α] {s : Set α} : 0 ≤ Metric.diam s

The diameter of a set is always nonnegative

theorem Metric.diam_subsingleton {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Set.Subsingleton s) : Metric.diam s = 0

@[simp]

theorem Metric.diam_empty {α : Type u} [PseudoMetricSpace α] : Metric.diam ∅ = 0

The empty set has zero diameter

@[simp]

theorem Metric.diam_singleton {α : Type u} [PseudoMetricSpace α] {x : α} : Metric.diam {x} = 0

A singleton has zero diameter

@[simp]

theorem Metric.diam_zero {α : Type u} [PseudoMetricSpace α] [Zero α] : Metric.diam 0 = 0

@[simp]

theorem Metric.diam_one {α : Type u} [PseudoMetricSpace α] [One α] : Metric.diam 1 = 0

theorem Metric.diam_pair {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} : Metric.diam {x, y} = dist x y

theorem Metric.diam_triple {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {z : α} : Metric.diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)

theorem Metric.ediam_le_of_forall_dist_le {α : Type u} [PseudoMetricSpace α] {s : Set α} {C : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) : EMetric.diam s ≤ ENNReal.ofReal C

If the distance between any two points in a set is bounded by some constant C, then ENNReal.ofReal C bounds the emetric diameter of this set.

theorem Metric.diam_le_of_forall_dist_le {α : Type u} [PseudoMetricSpace α] {s : Set α} {C : ℝ} (h₀ : 0 ≤ C) (h : ∀ x ∈ s, ∀ y ∈ s, 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.

theorem Metric.diam_le_of_forall_dist_le_of_nonempty {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Set.Nonempty s) {C : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, 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.

theorem Metric.dist_le_diam_of_mem' {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (h : EMetric.diam s ≠ ⊤) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ Metric.diam s

The distance between two points in a set is controlled by the diameter of the set.

theorem Metric.isBounded_iff_ediam_ne_top {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s ↔ EMetric.diam s ≠ ⊤

Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.

theorem Bornology.IsBounded.ediam_ne_top {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s → EMetric.diam s ≠ ⊤

Alias of the forward direction of Metric.isBounded_iff_ediam_ne_top.

---

Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.

theorem Metric.ediam_eq_top_iff_unbounded {α : Type u} [PseudoMetricSpace α] {s : Set α} : EMetric.diam s = ⊤ ↔ ¬Bornology.IsBounded s

theorem Metric.ediam_univ_eq_top_iff_noncompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : EMetric.diam Set.univ = ⊤ ↔ NoncompactSpace α

@[simp]

theorem Metric.ediam_univ_of_noncompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] [NoncompactSpace α] : EMetric.diam Set.univ = ⊤

@[simp]

theorem Metric.diam_univ_of_noncompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] [NoncompactSpace α] : Metric.diam Set.univ = 0

theorem Metric.dist_le_diam_of_mem {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (h : Bornology.IsBounded s) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ Metric.diam s

The distance between two points in a set is controlled by the diameter of the set.

theorem Metric.ediam_of_unbounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : ¬Bornology.IsBounded s) : EMetric.diam s = ⊤

theorem Metric.diam_eq_zero_of_unbounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : ¬Bornology.IsBounded 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

theorem Metric.diam_mono {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} (h : s ⊆ t) (ht : Bornology.IsBounded 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.

theorem Metric.diam_union {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} {t : Set α} (xs : x ∈ s) (yt : y ∈ t) : Metric.diam (s ∪ t) ≤ Metric.diam s + 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.

theorem Metric.diam_union' {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} (h : Set.Nonempty (s ∩ t)) : Metric.diam (s ∪ t) ≤ Metric.diam s + Metric.diam t

If two sets intersect, the diameter of the union is bounded by the sum of the diameters.

theorem Metric.diam_le_of_subset_closedBall {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ} (hr : 0 ≤ r) (h : s ⊆ Metric.closedBall x r) : Metric.diam s ≤ 2 * r

theorem Metric.diam_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h : 0 ≤ r) : Metric.diam (Metric.closedBall x r) ≤ 2 * r

The diameter of a closed ball of radius r is at most 2 r.

theorem Metric.diam_ball {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h : 0 ≤ r) : Metric.diam (Metric.ball x r) ≤ 2 * r

The diameter of a ball of radius r is at most 2 r.

theorem IsComplete.nonempty_iInter_of_nonempty_biInter {α : Type u} [PseudoMetricSpace α] {s : ℕ → Set α} (h0 : IsComplete (s 0)) (hs : ∀ (n : ℕ), IsClosed (s n)) (h's : ∀ (n : ℕ), Bornology.IsBounded (s n)) (h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)) (h' : Filter.Tendsto (fun (n : ℕ) => Metric.diam (s n)) Filter.atTop (nhds 0)) : Set.Nonempty (⋂ (n : ℕ), s n)

If a family of complete sets with diameter tending to 0 is such that each finite intersection is nonempty, then the total intersection is also nonempty.

theorem Metric.nonempty_iInter_of_nonempty_biInter {α : Type u} [PseudoMetricSpace α] [CompleteSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), IsClosed (s n)) (h's : ∀ (n : ℕ), Bornology.IsBounded (s n)) (h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)) (h' : Filter.Tendsto (fun (n : ℕ) => Metric.diam (s n)) Filter.atTop (nhds 0)) : Set.Nonempty (⋂ (n : ℕ), s n)

In a complete space, if a family of closed sets with diameter tending to 0 is such that each finite intersection is nonempty, then the total intersection is also nonempty.

def Mathlib.Meta.Positivity.evalDiam : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: the diameter of a set is always nonnegative.

theorem Metric.cobounded_eq_cocompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : Bornology.cobounded α = Filter.cocompact α

theorem tendsto_dist_right_cocompact_atTop {α : Type u} [PseudoMetricSpace α] [ProperSpace α] (x : α) : Filter.Tendsto (fun (x_1 : α) => dist x_1 x) (Filter.cocompact α) Filter.atTop

theorem tendsto_dist_left_cocompact_atTop {α : Type u} [PseudoMetricSpace α] [ProperSpace α] (x : α) : Filter.Tendsto (dist x) (Filter.cocompact α) Filter.atTop

theorem comap_dist_left_atTop_eq_cocompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] (x : α) : Filter.comap (dist x) Filter.atTop = Filter.cocompact α

theorem tendsto_cocompact_of_tendsto_dist_comp_atTop {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {l : Filter β} (x : α) (h : Filter.Tendsto (fun (y : β) => dist (f y) x) l Filter.atTop) : Filter.Tendsto f l (Filter.cocompact α)

theorem Metric.finite_isBounded_inter_isClosed {α : Type u} [PseudoMetricSpace α] [ProperSpace α] {K : Set α} {s : Set α} [DiscreteTopology ↑s] (hK : Bornology.IsBounded K) (hs : IsClosed s) : Set.Finite (K ∩ s)