doc-next-gen

Mathlib.Topology.MetricSpace.Bounded

Module docstring

{"## 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 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 "}

Metric.isBounded_closedBall theorem
: IsBounded (closedBall x r)
Full source 
/-- Closed balls are bounded -/
theorem isBounded_closedBall : IsBounded (closedBall x r) :=
  isBounded_iff.2 ⟨r + r, fun y hy z hz =>
    calc dist y z ≤ dist y x + dist z x := dist_triangle_right _ _ _
    _ ≤ r + r := add_le_add hy hz⟩
Closed Balls are Bounded in Pseudometric Spaces
Informal description
For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $r$, the closed ball $\overline{B}(x, r) = \{ y \mid \text{dist}(y, x) \leq r \}$ is a bounded subset of $\alpha$.
Metric.isBounded_ball theorem
: IsBounded (ball x r)
Full source 
/-- Open balls are bounded -/
theorem isBounded_ball : IsBounded (ball x r) :=
  isBounded_closedBall.subset ball_subset_closedBall
Open Balls are Bounded in Pseudometric Spaces
Informal description
For any point $x$ in a pseudometric space $\alpha$ and any positive real number $r$, the open ball $B(x, r) = \{ y \mid \text{dist}(y, x) < r \}$ is a bounded subset of $\alpha$.
Metric.isBounded_sphere theorem
: IsBounded (sphere x r)
Full source 
/-- Spheres are bounded -/
theorem isBounded_sphere : IsBounded (sphere x r) :=
  isBounded_closedBall.subset sphere_subset_closedBall
Spheres are bounded in pseudometric spaces
Informal description
For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $r$, the sphere $S(x, r) = \{ y \in \alpha \mid \text{dist}(y, x) = r \}$ is a bounded subset of $\alpha$.
Metric.isBounded_iff_subset_closedBall theorem
(c : α) : IsBounded s ↔ ∃ r, s ⊆ closedBall c r
Full source 
/-- Given a point, a bounded subset is included in some ball around this point -/
theorem isBounded_iff_subset_closedBall (c : α) : IsBoundedIsBounded s ↔ ∃ r, s ⊆ closedBall c r :=
  ⟨fun h ↦ (isBounded_iff.1 (h.insert c)).imp fun _r hr _x hx ↦ hr (.inr hx) (mem_insert _ _),
    fun ⟨_r, hr⟩ ↦ isBounded_closedBall.subset hr⟩
Characterization of Bounded Sets via Closed Balls in Pseudometric Spaces
Informal description
A subset $s$ of a pseudometric space $\alpha$ is bounded if and only if there exists a radius $r \geq 0$ such that $s$ is contained in the closed ball $\overline{B}(c, r)$ centered at some point $c \in \alpha$.
Bornology.IsBounded.subset_closedBall theorem
(h : IsBounded s) (c : α) : ∃ r, s ⊆ closedBall c r
Full source 
theorem _root_.Bornology.IsBounded.subset_closedBall (h : IsBounded s) (c : α) :
    ∃ r, s ⊆ closedBall c r :=
  (isBounded_iff_subset_closedBall c).1 h
Bounded Sets are Contained in Closed Balls
Informal description
If a subset $s$ of a pseudometric space $\alpha$ is bounded, then for any point $c \in \alpha$, there exists a radius $r \geq 0$ such that $s$ is contained in the closed ball $\overline{B}(c, r)$ centered at $c$ with radius $r$.
Bornology.IsBounded.subset_ball_lt theorem
(h : IsBounded s) (a : ℝ) (c : α) : ∃ r, a < r ∧ s ⊆ ball c r
Full source 
theorem _root_.Bornology.IsBounded.subset_ball_lt (h : IsBounded s) (a : ℝ) (c : α) :
    ∃ r, a < r ∧ s ⊆ ball c r :=
  let ⟨r, hr⟩ := h.subset_closedBall c
  ⟨max r a + 1, (le_max_right _ _).trans_lt (lt_add_one _), hr.trans <| closedBall_subset_ball <|
    (le_max_left _ _).trans_lt (lt_add_one _)⟩
Bounded Sets are Contained in Open Balls of Arbitrarily Large Radius
Informal description
For any bounded subset $s$ of a pseudometric space $\alpha$, any real number $a$, and any point $c \in \alpha$, there exists a radius $r > a$ such that $s$ is contained in the open ball $B(c, r)$ centered at $c$ with radius $r$.
Bornology.IsBounded.subset_ball theorem
(h : IsBounded s) (c : α) : ∃ r, s ⊆ ball c r
Full source 
theorem _root_.Bornology.IsBounded.subset_ball (h : IsBounded s) (c : α) : ∃ r, s ⊆ ball c r :=
  (h.subset_ball_lt 0 c).imp fun _ ↦ And.right
Bounded Sets are Contained in Open Balls
Informal description
For any bounded subset $s$ of a pseudometric space $\alpha$ and any point $c \in \alpha$, there exists a radius $r \geq 0$ such that $s$ is contained in the open ball $B(c, r)$ centered at $c$ with radius $r$.
Metric.isBounded_iff_subset_ball theorem
(c : α) : IsBounded s ↔ ∃ r, s ⊆ ball c r
Full source 
theorem isBounded_iff_subset_ball (c : α) : IsBoundedIsBounded s ↔ ∃ r, s ⊆ ball c r :=
  ⟨(IsBounded.subset_ball · c), fun ⟨_r, hr⟩ ↦ isBounded_ball.subset hr⟩
Characterization of Bounded Sets via Open Balls in Pseudometric Spaces
Informal description
A subset $s$ of a pseudometric space $\alpha$ is bounded if and only if there exists a radius $r \geq 0$ such that $s$ is contained in the open ball $B(c, r)$ centered at some point $c \in \alpha$.
Bornology.IsBounded.subset_closedBall_lt theorem
(h : IsBounded s) (a : ℝ) (c : α) : ∃ r, a < r ∧ s ⊆ closedBall c r
Full source 
theorem _root_.Bornology.IsBounded.subset_closedBall_lt (h : IsBounded s) (a : ℝ) (c : α) :
    ∃ r, a < r ∧ s ⊆ closedBall c r :=
  let ⟨r, har, hr⟩ := h.subset_ball_lt a c
  ⟨r, har, hr.trans ball_subset_closedBall⟩
Bounded Sets are Contained in Closed Balls of Arbitrarily Large Radius
Informal description
For any bounded subset $s$ of a pseudometric space $\alpha$, any real number $a$, and any point $c \in \alpha$, there exists a radius $r > a$ such that $s$ is contained in the closed ball $\overline{B}(c, r)$ centered at $c$ with radius $r$.
Metric.isBounded_closure_of_isBounded theorem
(h : IsBounded s) : IsBounded (closure s)
Full source 
theorem isBounded_closure_of_isBounded (h : IsBounded s) : IsBounded (closure s) :=
  let ⟨C, h⟩ := isBounded_iff.1 h
  isBounded_iff.2 ⟨C, fun _a ha _b hb => isClosed_Iic.closure_subset <|
    map_mem_closure₂ continuous_dist ha hb h⟩
Closure of a Bounded Set is Bounded in Pseudometric Spaces
Informal description
For any subset $s$ of a pseudometric space $\alpha$, if $s$ is bounded, then its closure $\overline{s}$ is also bounded.
Metric.hasBasis_cobounded_compl_closedBall theorem
(c : α) : (cobounded α).HasBasis (fun _ ↦ True) (fun r ↦ (closedBall c r)ᶜ)
Full source 
theorem hasBasis_cobounded_compl_closedBall (c : α) :
    (cobounded α).HasBasis (fun _ ↦ True) (fun r ↦ (closedBall c r)ᶜ) :=
  ⟨compl_surjective.forall.2 fun _ ↦ (isBounded_iff_subset_closedBall c).trans <| by simp⟩
Cobounded Filter Basis via Complements of Closed Balls
Informal description
For any point $c$ in a pseudometric space $\alpha$, the filter `cobounded α` has a basis consisting of the complements of closed balls centered at $c$ with arbitrary radii $r \geq 0$. That is, the sets $\overline{B}(c, r)^c$ form a basis for the cobounded filter, where $\overline{B}(c, r)$ denotes the closed ball of radius $r$ centered at $c$.
Metric.hasAntitoneBasis_cobounded_compl_closedBall theorem
(c : α) : (cobounded α).HasAntitoneBasis (fun r ↦ (closedBall c r)ᶜ)
Full source 
theorem hasAntitoneBasis_cobounded_compl_closedBall (c : α) :
    (cobounded α).HasAntitoneBasis (fun r ↦ (closedBall c r)ᶜ) :=
  ⟨Metric.hasBasis_cobounded_compl_closedBall _, fun _ _ hr _ ↦ by simpa using hr.trans_lt⟩
Antitone Basis for Cobounded Filter via Complements of Closed Balls
Informal description
For any point $c$ in a pseudometric space $\alpha$, the cobounded filter on $\alpha$ has an antitone basis consisting of the complements of closed balls centered at $c$ with radii $r \geq 0$. That is, the family of sets $\overline{B}(c, r)^c$ indexed by $r \in \mathbb{R}_{\geq 0}$ forms an antitone basis for the cobounded filter, where $\overline{B}(c, r)$ denotes the closed ball of radius $r$ centered at $c$.
Metric.hasBasis_cobounded_compl_ball theorem
(c : α) : (cobounded α).HasBasis (fun _ ↦ True) (fun r ↦ (ball c r)ᶜ)
Full source 
theorem hasBasis_cobounded_compl_ball (c : α) :
    (cobounded α).HasBasis (fun _ ↦ True) (fun r ↦ (ball c r)ᶜ) :=
  ⟨compl_surjective.forall.2 fun _ ↦ (isBounded_iff_subset_ball c).trans <| by simp⟩
Cobounded Filter Basis via Complements of Open Balls
Informal description
For any point $c$ in a pseudometric space $\alpha$, the cobounded filter on $\alpha$ has a basis consisting of the complements of open balls centered at $c$ with arbitrary radii $r \geq 0$. That is, the sets $B(c, r)^c$ form a basis for the cobounded filter, where $B(c, r)$ denotes the open ball of radius $r$ centered at $c$.
Metric.hasAntitoneBasis_cobounded_compl_ball theorem
(c : α) : (cobounded α).HasAntitoneBasis (fun r ↦ (ball c r)ᶜ)
Full source 
theorem hasAntitoneBasis_cobounded_compl_ball (c : α) :
    (cobounded α).HasAntitoneBasis (fun r ↦ (ball c r)ᶜ) :=
  ⟨Metric.hasBasis_cobounded_compl_ball _, fun _ _ hr _ ↦ by simpa using hr.trans⟩
Antitone Basis for Cobounded Filter via Complements of Open Balls
Informal description
For any point $c$ in a pseudometric space $\alpha$, the cobounded filter on $\alpha$ has an antitone basis consisting of the complements of open balls centered at $c$ with radii $r \geq 0$. That is, the family of sets $\text{ball}(c, r)^c$ indexed by $r \in \mathbb{R}_{\geq 0}$ forms an antitone basis for the cobounded filter, where $\text{ball}(c, r)$ denotes the open ball of radius $r$ centered at $c$.
Metric.comap_dist_right_atTop theorem
(c : α) : comap (dist · c) atTop = cobounded α
Full source 
@[simp]
theorem comap_dist_right_atTop (c : α) : comap (dist · c) atTop = cobounded α :=
  (atTop_basis.comap _).eq_of_same_basis <| by
    simpa only [compl_def, mem_ball, not_lt] using hasBasis_cobounded_compl_ball c
Preimage of Distance Function to a Point Equals Cobounded Filter
Informal description
For any point $c$ in a pseudometric space $\alpha$, the preimage of the filter at infinity under the distance function $\text{dist}(\cdot, c)$ is equal to the cobounded filter on $\alpha$. In other words, $\text{comap} (\lambda x \mapsto \text{dist}(x, c)) \ \text{atTop} = \text{cobounded} \ \alpha$.
Metric.comap_dist_left_atTop theorem
(c : α) : comap (dist c) atTop = cobounded α
Full source 
@[simp]
theorem comap_dist_left_atTop (c : α) : comap (dist c) atTop = cobounded α := by
  simpa only [dist_comm _ c] using comap_dist_right_atTop c
Preimage of Distance from Fixed Point Equals Cobounded Filter
Informal description
For any point $c$ in a pseudometric space $\alpha$, the preimage of the filter at infinity under the distance function $\text{dist}(c, \cdot)$ is equal to the cobounded filter on $\alpha$. That is, $\text{comap} (\text{dist}(c, \cdot)) \ \text{atTop} = \text{cobounded} \ \alpha$.
Metric.tendsto_dist_right_atTop_iff theorem
(c : α) {f : β → α} {l : Filter β} : Tendsto (fun x ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α)
Full source 
@[simp]
theorem tendsto_dist_right_atTop_iff (c : α) {f : β → α} {l : Filter β} :
    TendstoTendsto (fun x ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α) := by
  rw [← comap_dist_right_atTop c, tendsto_comap_iff, Function.comp_def]
Characterization of Tendency to Infinity via Distance to a Fixed Point
Informal description
Let $\alpha$ be a pseudometric space, $c \in \alpha$ a fixed point, and $f : \beta \to \alpha$ a function. For any filter $l$ on $\beta$, the function $x \mapsto \text{dist}(f(x), c)$ tends to infinity along $l$ if and only if $f$ tends to the cobounded filter of $\alpha$ along $l$.
Metric.tendsto_dist_left_atTop_iff theorem
(c : α) {f : β → α} {l : Filter β} : Tendsto (fun x ↦ dist c (f x)) l atTop ↔ Tendsto f l (cobounded α)
Full source 
@[simp]
theorem tendsto_dist_left_atTop_iff (c : α) {f : β → α} {l : Filter β} :
    TendstoTendsto (fun x ↦ dist c (f x)) l atTop ↔ Tendsto f l (cobounded α) := by
  simp only [dist_comm c, tendsto_dist_right_atTop_iff]
Characterization of Tendency to Infinity via Distance to a Fixed Point
Informal description
Let $\alpha$ be a pseudometric space, $c \in \alpha$ be a point, and $f : \beta \to \alpha$ be a function. For any filter $l$ on $\beta$, the function $x \mapsto \text{dist}(c, f(x))$ tends to infinity along $l$ if and only if $f$ tends to the cobounded filter of $\alpha$ along $l$.
Metric.tendsto_dist_right_cobounded_atTop theorem
(c : α) : Tendsto (dist · c) (cobounded α) atTop
Full source 
theorem tendsto_dist_right_cobounded_atTop (c : α) : Tendsto (dist · c) (cobounded α) atTop :=
  tendsto_iff_comap.2 (comap_dist_right_atTop c).ge
Distance to a Fixed Point Tends to Infinity Along the Cobounded Filter
Informal description
For any point $c$ in a pseudometric space $\alpha$, the function $x \mapsto \text{dist}(x, c)$ tends to infinity along the cobounded filter of $\alpha$.
Metric.tendsto_dist_left_cobounded_atTop theorem
(c : α) : Tendsto (dist c) (cobounded α) atTop
Full source 
theorem tendsto_dist_left_cobounded_atTop (c : α) : Tendsto (dist c) (cobounded α) atTop :=
  tendsto_iff_comap.2 (comap_dist_left_atTop c).ge
Distance from Fixed Point Tends to Infinity Along Cobounded Filter
Informal description
For any point $c$ in a pseudometric space $\alpha$, the function $x \mapsto \text{dist}(c, x)$ tends to infinity along the cobounded filter of $\alpha$.
TotallyBounded.isBounded theorem
{s : Set α} (h : TotallyBounded s) : IsBounded s
Full source 
/-- A totally bounded set is bounded -/
theorem _root_.TotallyBounded.isBounded {s : Set α} (h : TotallyBounded s) : IsBounded s :=
  -- We cover the totally bounded set by finitely many balls of radius 1,
  -- and then argue that a finite union of bounded sets is bounded
  let ⟨_t, fint, subs⟩ := (totallyBounded_iff.mp h) 1 zero_lt_one
  ((isBounded_biUnion fint).2 fun _ _ => isBounded_ball).subset subs
Totally Bounded Subsets are Bounded in Pseudometric Spaces
Informal description
Let $s$ be a subset of a pseudometric space $\alpha$. If $s$ is totally bounded, then $s$ is bounded.
IsCompact.isBounded theorem
{s : Set α} (h : IsCompact s) : IsBounded s
Full source 
/-- A compact set is bounded -/
theorem _root_.IsCompact.isBounded {s : Set α} (h : IsCompact s) : IsBounded s :=
  -- A compact set is totally bounded, thus bounded
  h.totallyBounded.isBounded
Compact subsets are bounded in pseudometric spaces
Informal description
For any subset $s$ of a pseudometric space $\alpha$, if $s$ is compact, then $s$ is bounded.
Metric.cobounded_le_cocompact theorem
: cobounded α ≤ cocompact α
Full source 
theorem cobounded_le_cocompact : cobounded α ≤ cocompact α :=
  hasBasis_cocompact.ge_iff.2 fun _s hs ↦ hs.isBounded
Cobounded Filter is Finer than Cocompact Filter in Pseudometric Spaces
Informal description
In a pseudometric space $\alpha$, the cobounded filter is finer than the cocompact filter. That is, every cocompact set is cobounded.
Metric.isCobounded_iff_closedBall_compl_subset theorem
{s : Set α} (c : α) : IsCobounded s ↔ ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s
Full source 
theorem isCobounded_iff_closedBall_compl_subset {s : Set α} (c : α) :
    IsCoboundedIsCobounded s ↔ ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s := by
  rw [← isBounded_compl_iff, isBounded_iff_subset_closedBall c]
  apply exists_congr
  intro r
  rw [compl_subset_comm]
Characterization of Cobounded Sets via Closed Ball Complements in Pseudometric Spaces
Informal description
For a subset $s$ of a pseudometric space $\alpha$ and a point $c \in \alpha$, the set $s$ is cobounded if and only if there exists a radius $r \geq 0$ such that the complement of the closed ball $\overline{B}(c, r)$ is contained in $s$. That is, $s$ is cobounded if and only if $\exists r \geq 0, \overline{B}(c, r)^c \subseteq s$.
Bornology.IsCobounded.closedBall_compl_subset theorem
{s : Set α} (hs : IsCobounded s) (c : α) : ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s
Full source 
theorem _root_.Bornology.IsCobounded.closedBall_compl_subset {s : Set α} (hs : IsCobounded s)
    (c : α) : ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s :=
  (isCobounded_iff_closedBall_compl_subset c).mp hs
Existence of Closed Ball Complement for Cobounded Sets in Pseudometric Spaces
Informal description
For any cobounded subset $s$ of a pseudometric space $\alpha$ and any point $c \in \alpha$, there exists a radius $r \in \mathbb{R}$ such that the complement of the closed ball $\overline{B}(c, r)$ is contained in $s$.
Metric.closedBall_compl_subset_of_mem_cocompact theorem
{s : Set α} (hs : s ∈ cocompact α) (c : α) : ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s
Full source 
theorem closedBall_compl_subset_of_mem_cocompact {s : Set α} (hs : s ∈ cocompact α) (c : α) :
    ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s :=
  IsCobounded.closedBall_compl_subset (cobounded_le_cocompact hs) c
Existence of Closed Ball Complement for Cocompact Sets in Pseudometric Spaces
Informal description
For any subset $s$ of a pseudometric space $\alpha$ that belongs to the cocompact filter, and for any point $c \in \alpha$, there exists a radius $r \in \mathbb{R}$ such that the complement of the closed ball $\overline{B}(c, r)$ is contained in $s$.
Metric.mem_cocompact_of_closedBall_compl_subset theorem
[ProperSpace α] (c : α) (h : ∃ r, (closedBall c r)ᶜ ⊆ s) : s ∈ cocompact α
Full source 
theorem mem_cocompact_of_closedBall_compl_subset [ProperSpace α] (c : α)
    (h : ∃ r, (closedBall c r)ᶜ ⊆ s) : s ∈ cocompact α := by
  rcases h with ⟨r, h⟩
  rw [Filter.mem_cocompact]
  exact ⟨closedBall c r, isCompact_closedBall c r, h⟩
Cocompactness via Complement of Closed Ball in Proper Spaces
Informal description
Let $\alpha$ be a proper pseudometric space. For any point $c \in \alpha$ and any set $s \subseteq \alpha$, if there exists a radius $r \in \mathbb{R}$ such that the complement of the closed ball $\overline{B}(c, r)$ is contained in $s$, then $s$ belongs to the cocompact filter of $\alpha$.
Metric.mem_cocompact_iff_closedBall_compl_subset theorem
[ProperSpace α] (c : α) : s ∈ cocompact α ↔ ∃ r, (closedBall c r)ᶜ ⊆ s
Full source 
theorem mem_cocompact_iff_closedBall_compl_subset [ProperSpace α] (c : α) :
    s ∈ cocompact αs ∈ cocompact α ↔ ∃ r, (closedBall c r)ᶜ ⊆ s :=
  ⟨(closedBall_compl_subset_of_mem_cocompact · _), mem_cocompact_of_closedBall_compl_subset _⟩
Characterization of Cocompact Sets via Closed Ball Complements in Proper Spaces
Informal description
Let $\alpha$ be a proper pseudometric space and $c \in \alpha$ be a point. A subset $s \subseteq \alpha$ belongs to the cocompact filter if and only if there exists a radius $r \in \mathbb{R}$ such that the complement of the closed ball $\overline{B}(c, r)$ is contained in $s$.
Metric.isBounded_range_iff theorem
{f : β → α} : IsBounded (range f) ↔ ∃ C, ∀ x y, dist (f x) (f y) ≤ C
Full source 
/-- Characterization of the boundedness of the range of a function -/
theorem isBounded_range_iff {f : β → α} : IsBoundedIsBounded (range f) ↔ ∃ C, ∀ x y, dist (f x) (f y) ≤ C :=
  isBounded_iff.trans <| by simp only [forall_mem_range]
Boundedness Criterion for Function Range in Pseudometric Spaces
Informal description
For a function $f : \beta \to \alpha$ where $\alpha$ is a pseudometric space, the range of $f$ is bounded if and only if there exists a real number $C$ such that for all $x, y \in \beta$, the distance between $f(x)$ and $f(y)$ satisfies $\text{dist}(f(x), f(y)) \leq C$.
Metric.isBounded_image_iff theorem
{f : β → α} {s : Set β} : IsBounded (f '' s) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C
Full source 
theorem isBounded_image_iff {f : β → α} {s : Set β} :
    IsBoundedIsBounded (f '' s) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C :=
  isBounded_iff.trans <| by simp only [forall_mem_image]
Boundedness of Function Image in Pseudometric Space
Informal description
For a function $f : \beta \to \alpha$ between a type $\beta$ and a pseudometric space $\alpha$, and a subset $s \subseteq \beta$, the image $f(s)$ is bounded in $\alpha$ if and only if there exists a constant $C \in \mathbb{R}$ such that for all $x, y \in s$, the distance between $f(x)$ and $f(y)$ satisfies $\text{dist}(f(x), f(y)) \leq C$.
Metric.isBounded_range_of_tendsto_cofinite_uniformity theorem
{f : β → α} (hf : Tendsto (Prod.map f f) (.cofinite ×ˢ .cofinite) (𝓤 α)) : IsBounded (range f)
Full source 
theorem isBounded_range_of_tendsto_cofinite_uniformity {f : β → α}
    (hf : Tendsto (Prod.map f f) (.cofinite ×ˢ .cofinite) (𝓤 α)) : IsBounded (range f) := by
  rcases (hasBasis_cofinite.prod_self.tendsto_iff uniformity_basis_dist).1 hf 1 zero_lt_one with
    ⟨s, hsf, hs1⟩
  rw [← image_union_image_compl_eq_range]
  refine (hsf.image f).isBounded.union (isBounded_image_iff.2 ⟨1, fun x hx y hy ↦ ?_⟩)
  exact le_of_lt (hs1 (x, y) ⟨hx, hy⟩)
Boundedness of Range for Functions with Cofinite-Tending Product Map in Pseudometric Spaces
Informal description
Let $f : \beta \to \alpha$ be a function from a type $\beta$ to a pseudometric space $\alpha$. If the product map $f \times f$ tends to the uniformity filter of $\alpha$ along the product of cofinite filters on $\beta$, then the range of $f$ is bounded in $\alpha$.
Metric.isBounded_range_of_cauchy_map_cofinite theorem
{f : β → α} (hf : Cauchy (map f cofinite)) : IsBounded (range f)
Full source 
theorem isBounded_range_of_cauchy_map_cofinite {f : β → α} (hf : Cauchy (map f cofinite)) :
    IsBounded (range f) :=
  isBounded_range_of_tendsto_cofinite_uniformity <| (cauchy_map_iff.1 hf).2
Boundedness of Range for Functions with Cauchy Cofinite Image Filter in Pseudometric Spaces
Informal description
For any function $f : \beta \to \alpha$ from a type $\beta$ to a pseudometric space $\alpha$, if the image filter of the cofinite filter under $f$ is Cauchy, then the range of $f$ is bounded in $\alpha$.
Metric.isBounded_range_of_tendsto_cofinite theorem
{f : β → α} {a : α} (hf : Tendsto f cofinite (𝓝 a)) : IsBounded (range f)
Full source 
theorem isBounded_range_of_tendsto_cofinite {f : β → α} {a : α} (hf : Tendsto f cofinite (𝓝 a)) :
    IsBounded (range f) :=
  isBounded_range_of_tendsto_cofinite_uniformity <|
    (hf.prodMap hf).mono_right <| nhds_prod_eq.symm.trans_le (nhds_le_uniformity a)
Boundedness of Range for Cofinite-Tending Functions in Pseudometric Spaces
Informal description
Let $f : \beta \to \alpha$ be a function from a type $\beta$ to a pseudometric space $\alpha$. If $f$ tends to a point $a \in \alpha$ along the cofinite filter on $\beta$, then the range of $f$ is bounded in $\alpha$.
Metric.isBounded_range_of_tendsto theorem
(u : ℕ → α) {x : α} (hu : Tendsto u atTop (𝓝 x)) : IsBounded (range u)
Full source 
theorem isBounded_range_of_tendsto (u : ℕ → α) {x : α} (hu : Tendsto u atTop (𝓝 x)) :
    IsBounded (range u) :=
  hu.cauchySeq.isBounded_range
Boundedness of the Range of a Convergent Sequence in a Pseudometric Space
Informal description
For any sequence $u \colon \mathbb{N} \to \alpha$ in a pseudometric space $\alpha$ that converges to a point $x \in \alpha$, the range of $u$ is bounded.
Metric.disjoint_nhds_cobounded theorem
(x : α) : Disjoint (𝓝 x) (cobounded α)
Full source 
theorem disjoint_nhds_cobounded (x : α) : Disjoint (𝓝 x) (cobounded α) :=
  disjoint_of_disjoint_of_mem disjoint_compl_right (ball_mem_nhds _ one_pos) isBounded_ball
Disjointness of Neighborhood and Cobounded Filters in Pseudometric Spaces
Informal description
For any point $x$ in a pseudometric space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ of $x$ is disjoint from the filter of cobounded sets in $\alpha$.
Metric.disjoint_cobounded_nhds theorem
(x : α) : Disjoint (cobounded α) (𝓝 x)
Full source 
theorem disjoint_cobounded_nhds (x : α) : Disjoint (cobounded α) (𝓝 x) :=
  (disjoint_nhds_cobounded x).symm
Disjointness of Cobounded and Neighborhood Filters in Pseudometric Spaces
Informal description
For any point $x$ in a pseudometric space $\alpha$, the filter of cobounded sets in $\alpha$ is disjoint from the neighborhood filter $\mathcal{N}(x)$ of $x$.
Metric.disjoint_nhdsSet_cobounded theorem
{s : Set α} (hs : IsCompact s) : Disjoint (𝓝ˢ s) (cobounded α)
Full source 
theorem disjoint_nhdsSet_cobounded {s : Set α} (hs : IsCompact s) : Disjoint (𝓝ˢ s) (cobounded α) :=
  hs.disjoint_nhdsSet_left.2 fun _ _ ↦ disjoint_nhds_cobounded _
Disjointness of Neighborhood Filter of Compact Set and Cobounded Filter in Pseudometric Spaces
Informal description
For any compact subset $s$ of a pseudometric space $\alpha$, the neighborhood filter of $s$ is disjoint from the filter of cobounded sets in $\alpha$.
Metric.disjoint_cobounded_nhdsSet theorem
{s : Set α} (hs : IsCompact s) : Disjoint (cobounded α) (𝓝ˢ s)
Full source 
theorem disjoint_cobounded_nhdsSet {s : Set α} (hs : IsCompact s) : Disjoint (cobounded α) (𝓝ˢ s) :=
  (disjoint_nhdsSet_cobounded hs).symm
Disjointness of Cobounded and Neighborhood Filters for Compact Sets in Pseudometric Spaces
Informal description
For any compact subset $s$ of a pseudometric space $\alpha$, the filter of cobounded sets in $\alpha$ is disjoint from the neighborhood filter of $s$.
Metric.exists_isBounded_image_of_tendsto theorem
{α β : Type*} [PseudoMetricSpace β] {l : Filter α} {f : α → β} {x : β} (hf : Tendsto f l (𝓝 x)) : ∃ s ∈ l, IsBounded (f '' s)
Full source 
theorem exists_isBounded_image_of_tendsto {α β : Type*} [PseudoMetricSpace β]
    {l : Filter α} {f : α → β} {x : β} (hf : Tendsto f l (𝓝 x)) :
    ∃ s ∈ l, IsBounded (f '' s) :=
  (l.basis_sets.map f).disjoint_iff_left.mp <| (disjoint_nhds_cobounded x).mono_left hf
Existence of Bounded Image for Functions Converging to a Point in Pseudometric Spaces
Informal description
Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a pseudometric space structure. Given a filter $l$ on $\alpha$, a function $f : \alpha \to \beta$, and a point $x \in \beta$, if $f$ tends to $x$ along the filter $l$, then there exists a set $s \in l$ such that the image $f(s)$ is bounded in $\beta$.
Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt theorem
[TopologicalSpace β] {k s : Set β} {f : β → α} (hk : IsCompact k) (hf : ∀ x ∈ k, ContinuousWithinAt f s x) : ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' (t ∩ s))
Full source 
/-- 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 exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt
    [TopologicalSpace β] {k s : Set β} {f : β → α} (hk : IsCompact k)
    (hf : ∀ x ∈ k, ContinuousWithinAt f s x) :
    ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' (t ∩ s)) := by
  have : Disjoint (𝓝ˢ𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α)) := by
    rw [disjoint_assoc, inf_comm, hk.disjoint_nhdsSet_left]
    exact fun x hx ↦ disjoint_left_comm.2 <|
      tendsto_comap.disjoint (disjoint_cobounded_nhds _) (hf x hx)
  rcases ((((hasBasis_nhdsSet _).inf_principal _)).disjoint_iff ((basis_sets _).comap _)).1 this
    with ⟨U, ⟨hUo, hkU⟩, t, ht, hd⟩
  refine ⟨U, hkU, hUo, (isBounded_compl_iff.2 ht).subset ?_⟩
  rwa [image_subset_iff, preimage_compl, subset_compl_iff_disjoint_right]
Boundedness of Continuous Images Near Compact Sets in Pseudometric Spaces
Informal description
Let $β$ be a topological space and $α$ a pseudometric space. Given a compact set $k \subseteq β$, a set $s \subseteq β$, and a function $f : β \to α$ that is continuous within $s$ at every point of $k$, there exists an open set $t \subseteq β$ containing $k$ such that the image $f(t \cap s)$ is bounded in $α$.
Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt theorem
[TopologicalSpace β] {k : Set β} {f : β → α} (hk : IsCompact k) (hf : ∀ x ∈ k, ContinuousAt f x) : ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' t)
Full source 
/-- If a function is continuous at every point of a compact set `k`, then it is bounded on
some open neighborhood of `k`. -/
theorem exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt [TopologicalSpace β]
    {k : Set β} {f : β → α} (hk : IsCompact k) (hf : ∀ x ∈ k, ContinuousAt f x) :
    ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' t) := by
  simp_rw [← continuousWithinAt_univ] at hf
  simpa only [inter_univ] using
    exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt hk hf
Boundedness of Continuous Images Near Compact Sets in Pseudometric Spaces
Informal description
Let $\beta$ be a topological space and $\alpha$ a pseudometric space. Given a compact set $k \subseteq \beta$ and a function $f : \beta \to \alpha$ that is continuous at every point of $k$, there exists an open set $t \subseteq \beta$ containing $k$ such that the image $f(t)$ is bounded in $\alpha$.
Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn theorem
[TopologicalSpace β] {k s : Set β} {f : β → α} (hk : IsCompact k) (hks : k ⊆ s) (hf : ContinuousOn f s) : ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' (t ∩ s))
Full source 
/-- 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 exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn [TopologicalSpace β]
    {k s : Set β} {f : β → α} (hk : IsCompact k) (hks : k ⊆ s) (hf : ContinuousOn f s) :
    ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' (t ∩ s)) :=
  exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt hk fun x hx =>
    hf x (hks hx)
Boundedness of Continuous Images Near Compact Sets in Pseudometric Spaces
Informal description
Let $\beta$ be a topological space and $\alpha$ a pseudometric space. Given a compact set $k \subseteq \beta$ with $k \subseteq s$, and a function $f : \beta \to \alpha$ that is continuous on $s$, there exists an open set $t \subseteq \beta$ containing $k$ such that the image $f(t \cap s)$ is bounded in $\alpha$.
Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn theorem
[TopologicalSpace β] {k s : Set β} {f : β → α} (hk : IsCompact k) (hs : IsOpen s) (hks : k ⊆ s) (hf : ContinuousOn f s) : ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' t)
Full source 
/-- If a function is continuous on a neighborhood of a compact set `k`, then it is bounded on
some open neighborhood of `k`. -/
theorem exists_isOpen_isBounded_image_of_isCompact_of_continuousOn [TopologicalSpace β]
    {k s : Set β} {f : β → α} (hk : IsCompact k) (hs : IsOpen s) (hks : k ⊆ s)
    (hf : ContinuousOn f s) : ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' t) :=
  exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt hk fun _x hx =>
    hf.continuousAt (hs.mem_nhds (hks hx))
Boundedness of Continuous Images Near Compact Sets in Pseudometric Spaces
Informal description
Let $\beta$ be a topological space and $\alpha$ a pseudometric space. Given a compact set $k \subseteq \beta$, an open set $s \subseteq \beta$ containing $k$, and a function $f \colon \beta \to \alpha$ that is continuous on $s$, there exists an open set $t \subseteq \beta$ such that $k \subseteq t$, $t$ is open, and the image $f(t)$ is bounded in $\alpha$.
Metric.isCompact_of_isClosed_isBounded theorem
[ProperSpace α] (hc : IsClosed s) (hb : IsBounded s) : IsCompact s
Full source 
/-- The **Heine–Borel theorem**: In a proper space, a closed bounded set is compact. -/
theorem isCompact_of_isClosed_isBounded [ProperSpace α] (hc : IsClosed s) (hb : IsBounded s) :
    IsCompact s := by
  rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)
  · exact isCompact_empty
  · rcases hb.subset_closedBall x with ⟨r, hr⟩
    exact (isCompact_closedBall x r).of_isClosed_subset hc hr
Heine–Borel Theorem for Proper Pseudometric Spaces
Informal description
In a proper pseudometric space $\alpha$, a subset $s \subseteq \alpha$ is compact if it is closed and bounded.
Bornology.IsBounded.isCompact_closure theorem
[ProperSpace α] (h : IsBounded s) : IsCompact (closure s)
Full source 
/-- The **Heine–Borel theorem**: In a proper space, the closure of a bounded set is compact. -/
theorem _root_.Bornology.IsBounded.isCompact_closure [ProperSpace α] (h : IsBounded s) :
    IsCompact (closure s) :=
  isCompact_of_isClosed_isBounded isClosed_closure h.closure
Closure of Bounded Sets is Compact in Proper Spaces (Heine–Borel)
Informal description
In a proper pseudometric space $\alpha$, the closure $\overline{s}$ of any bounded subset $s \subseteq \alpha$ is compact.
Metric.isCompact_iff_isClosed_bounded theorem
[T2Space α] [ProperSpace α] : IsCompact s ↔ IsClosed s ∧ IsBounded s
Full source 
/-- The **Heine–Borel theorem**:
In a proper Hausdorff space, a set is compact if and only if it is closed and bounded. -/
theorem isCompact_iff_isClosed_bounded [T2Space α] [ProperSpace α] :
    IsCompactIsCompact s ↔ IsClosed s ∧ IsBounded s :=
  ⟨fun h => ⟨h.isClosed, h.isBounded⟩, fun h => isCompact_of_isClosed_isBounded h.1 h.2⟩
Heine–Borel Theorem for Proper Hausdorff Pseudometric Spaces
Informal description
In a proper Hausdorff pseudometric space $\alpha$, a subset $s \subseteq \alpha$ is compact if and only if it is closed and bounded.
Metric.compactSpace_iff_isBounded_univ theorem
[ProperSpace α] : CompactSpace α ↔ IsBounded (univ : Set α)
Full source 
theorem compactSpace_iff_isBounded_univ [ProperSpace α] :
    CompactSpaceCompactSpace α ↔ IsBounded (univ : Set α) :=
  ⟨@isBounded_of_compactSpace α _ _, fun hb => ⟨isCompact_of_isClosed_isBounded isClosed_univ hb⟩⟩
Compactness Equivalence for Proper Spaces: $\alpha$ is compact if and only if $\alpha$ is bounded
Informal description
For a proper pseudometric space $\alpha$, the space $\alpha$ is compact if and only if the universal set (the entire space) is bounded.
totallyBounded_Icc theorem
(a b : α) : TotallyBounded (Icc a b)
Full source 
theorem _root_.totallyBounded_Icc (a b : α) : TotallyBounded (Icc a b) :=
  isCompact_Icc.totallyBounded
Total Boundedness of Closed Intervals in Pseudometric Spaces
Informal description
For any two elements $a$ and $b$ in a pseudometric space $\alpha$, the closed interval $[a, b]$ is totally bounded.
totallyBounded_Ico theorem
(a b : α) : TotallyBounded (Ico a b)
Full source 
theorem _root_.totallyBounded_Ico (a b : α) : TotallyBounded (Ico a b) :=
  (totallyBounded_Icc a b).subset Ico_subset_Icc_self
Total Boundedness of Left-Closed Right-Open Intervals in Pseudometric Spaces
Informal description
For any two elements $a$ and $b$ in a pseudometric space $\alpha$, the left-closed right-open interval $[a, b) = \{x \mid a \leq x < b\}$ is totally bounded.
totallyBounded_Ioc theorem
(a b : α) : TotallyBounded (Ioc a b)
Full source 
theorem _root_.totallyBounded_Ioc (a b : α) : TotallyBounded (Ioc a b) :=
  (totallyBounded_Icc a b).subset Ioc_subset_Icc_self
Total Boundedness of Left-Open Right-Closed Intervals in Pseudometric Spaces
Informal description
For any two elements $a$ and $b$ in a pseudometric space $\alpha$, the left-open right-closed interval $(a, b]$ is totally bounded.
Metric.isBounded_Icc theorem
(a b : α) : IsBounded (Icc a b)
Full source 
theorem isBounded_Icc (a b : α) : IsBounded (Icc a b) :=
  (totallyBounded_Icc a b).isBounded
Boundedness of Closed Intervals in Pseudometric Spaces
Informal description
For any two elements $a$ and $b$ in a pseudometric space $\alpha$, the closed interval $[a, b]$ is bounded.
Metric.isBounded_Ico theorem
(a b : α) : IsBounded (Ico a b)
Full source 
theorem isBounded_Ico (a b : α) : IsBounded (Ico a b) :=
  (totallyBounded_Ico a b).isBounded
Boundedness of Left-Closed Right-Open Intervals in Pseudometric Spaces
Informal description
For any two elements $a$ and $b$ in a pseudometric space $\alpha$, the left-closed right-open interval $[a, b) = \{x \mid a \leq x < b\}$ is bounded.
Metric.isBounded_Ioc theorem
(a b : α) : IsBounded (Ioc a b)
Full source 
theorem isBounded_Ioc (a b : α) : IsBounded (Ioc a b) :=
  (totallyBounded_Ioc a b).isBounded
Boundedness of Left-Open Right-Closed Intervals in Pseudometric Spaces
Informal description
For any two elements $a$ and $b$ in a pseudometric space $\alpha$, the left-open right-closed interval $(a, b]$ is bounded.
Metric.isBounded_Ioo theorem
(a b : α) : IsBounded (Ioo a b)
Full source 
theorem isBounded_Ioo (a b : α) : IsBounded (Ioo a b) :=
  (totallyBounded_Ioo a b).isBounded
Boundedness of Open Intervals in Pseudometric Spaces
Informal description
For any two elements $a$ and $b$ in a pseudometric space $\alpha$, the open interval $(a, b)$ is bounded.
Metric.isBounded_of_bddAbove_of_bddBelow theorem
{s : Set α} (h₁ : BddAbove s) (h₂ : BddBelow s) : IsBounded s
Full source 
/-- 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. -/
theorem isBounded_of_bddAbove_of_bddBelow {s : Set α} (h₁ : BddAbove s) (h₂ : BddBelow s) :
    IsBounded s :=
  let ⟨u, hu⟩ := h₁
  let ⟨l, hl⟩ := h₂
  (isBounded_Icc l u).subset (fun _x hx => mem_Icc.mpr ⟨hl hx, hu hx⟩)
Order-Bounded Implies Metric-Bounded in Pseudometric Spaces
Informal description
Let $\alpha$ be a pseudometric space with a conditionally complete linear order such that the order topology coincides with the metric topology. For any subset $s \subseteq \alpha$, if $s$ is both bounded above and bounded below (i.e., there exist $a, b \in \alpha$ such that $a \leq x \leq b$ for all $x \in s$), then $s$ is bounded in the metric sense.
Metric.diam definition
(s : Set α) : ℝ
Full source 
/-- 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` -/
noncomputable def diam (s : Set α) : ℝ :=
  ENNReal.toReal (EMetric.diam s)
Diameter of a set in a metric space
Informal description
The diameter of a set $s$ in a metric space is the supremum of the distances between any two points in $s$, expressed as a real number. If the set is unbounded, the diameter is defined to be $\infty$ (but represented as a real number via conversion).
Metric.diam_nonneg theorem
: 0 ≤ diam s
Full source 
/-- The diameter of a set is always nonnegative -/
theorem diam_nonneg : 0 ≤ diam s :=
  ENNReal.toReal_nonneg
Nonnegativity of Diameter in Pseudometric Spaces
Informal description
For any set $s$ in a pseudometric space, the diameter of $s$ is nonnegative, i.e., $\text{diam}(s) \geq 0$.
Metric.diam_empty theorem
: diam (∅ : Set α) = 0
Full source 
/-- The empty set has zero diameter -/
@[simp]
theorem diam_empty : diam (∅ : Set α) = 0 :=
  diam_subsingleton subsingleton_empty
Diameter of the Empty Set is Zero
Informal description
The diameter of the empty set in a pseudometric space is zero, i.e., $\text{diam}(\emptyset) = 0$.
Metric.diam_singleton theorem
: diam ({ x } : Set α) = 0
Full source 
/-- A singleton has zero diameter -/
@[simp]
theorem diam_singleton : diam ({x} : Set α) = 0 :=
  diam_subsingleton subsingleton_singleton
Zero Diameter of Singleton Sets in Pseudometric Spaces
Informal description
In any pseudometric space $\alpha$, the diameter of a singleton set $\{x\}$ is zero, i.e., $\text{diam}(\{x\}) = 0$.
Metric.diam_one theorem
[One α] : diam (1 : Set α) = 0
Full source 
@[to_additive (attr := simp)]
theorem diam_one [One α] : diam (1 : Set α) = 0 :=
  diam_singleton
Zero Diameter of the Multiplicative Identity Singleton in Pseudometric Spaces
Informal description
In a pseudometric space $\alpha$ with a multiplicative identity element $1$, the diameter of the singleton set $\{1\}$ is zero, i.e., $\text{diam}(\{1\}) = 0$.
Metric.diam_pair theorem
: diam ({ x, y } : Set α) = dist x y
Full source 
theorem diam_pair : diam ({x, y} : Set α) = dist x y := by
  simp only [diam, EMetric.diam_pair, dist_edist]
Diameter of Two-Point Set Equals Their Distance
Informal description
For any two points $x$ and $y$ in a pseudometric space $\alpha$, the diameter of the set $\{x, y\}$ is equal to the distance between $x$ and $y$, i.e., $\text{diam}(\{x, y\}) = \text{dist}(x, y)$.
Metric.diam_triple theorem
: Metric.diam ({ x, y, z } : Set α) = max (max (dist x y) (dist x z)) (dist y z)
Full source 
theorem diam_triple :
    Metric.diam ({x, y, z} : Set α) = max (max (dist x y) (dist x z)) (dist y z) := by
  simp only [Metric.diam, EMetric.diam_triple, dist_edist]
  rw [ENNReal.toReal_max, ENNReal.toReal_max] <;> apply_rules [ne_of_lt, edist_lt_top, max_lt]
Diameter of a Triple in a Pseudometric Space Equals Maximum Pairwise Distance
Informal description
Let $\alpha$ be a pseudometric space and $x, y, z \in \alpha$. The diameter of the set $\{x, y, z\}$ is equal to the maximum of the pairwise distances between $x$, $y$, and $z$, i.e., \[ \text{diam}(\{x, y, z\}) = \max(\max(\text{dist}(x, y), \text{dist}(x, z)), \text{dist}(y, z)). \]
Metric.ediam_le_of_forall_dist_le theorem
{C : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) : EMetric.diam s ≤ ENNReal.ofReal C
Full source 
/-- 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 ediam_le_of_forall_dist_le {C : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) :
    EMetric.diam s ≤ ENNReal.ofReal C :=
  EMetric.diam_le fun x hx y hy => (edist_dist x y).symm ▸ ENNReal.ofReal_le_ofReal (h x hx y hy)
Extended Diameter Bound from Uniform Distance Bound
Informal description
Let $s$ be a subset of a pseudometric space $\alpha$. If there exists a real number $C$ such that for any two points $x, y \in s$, the distance $\text{dist}(x, y) \leq C$, then the extended metric diameter of $s$ satisfies $\text{EMetric.diam}(s) \leq \text{ENNReal.ofReal}(C)$.
Metric.diam_le_of_forall_dist_le theorem
{C : ℝ} (h₀ : 0 ≤ C) (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) : diam s ≤ C
Full source 
/-- If the distance between any two points in a set is bounded by some non-negative constant,
this constant bounds the diameter. -/
theorem diam_le_of_forall_dist_le {C : ℝ} (h₀ : 0 ≤ C) (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) :
    diam s ≤ C :=
  ENNReal.toReal_le_of_le_ofReal h₀ (ediam_le_of_forall_dist_le h)
Diameter Bound from Uniform Distance Bound
Informal description
Let $s$ be a subset of a pseudometric space $\alpha$ and $C \geq 0$ a real number. If for any two points $x, y \in s$ we have $\text{dist}(x, y) \leq C$, then the diameter of $s$ satisfies $\text{diam}(s) \leq C$.
Metric.diam_le_of_forall_dist_le_of_nonempty theorem
(hs : s.Nonempty) {C : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) : diam s ≤ C
Full source 
/-- If the distance between any two points in a nonempty set is bounded by some constant,
this constant bounds the diameter. -/
theorem diam_le_of_forall_dist_le_of_nonempty (hs : s.Nonempty) {C : ℝ}
    (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) : diam s ≤ C :=
  have h₀ : 0 ≤ C :=
    let ⟨x, hx⟩ := hs
    le_trans dist_nonneg (h x hx x hx)
  diam_le_of_forall_dist_le h₀ h
Diameter Bound from Uniform Distance Bound for Nonempty Sets
Informal description
Let $s$ be a nonempty subset of a pseudometric space $\alpha$. If there exists a real number $C$ such that for any two points $x, y \in s$, the distance $\text{dist}(x, y) \leq C$, then the diameter of $s$ satisfies $\text{diam}(s) \leq C$.
Metric.dist_le_diam_of_mem' theorem
(h : EMetric.diam s ≠ ⊤) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ diam s
Full source 
/-- The distance between two points in a set is controlled by the diameter of the set. -/
theorem dist_le_diam_of_mem' (h : EMetric.diamEMetric.diam s ≠ ⊤) (hx : x ∈ s) (hy : y ∈ s) :
    dist x y ≤ diam s := by
  rw [diam, dist_edist]
  exact ENNReal.toReal_mono h <| EMetric.edist_le_diam_of_mem hx hy
Distance Bound by Diameter for Points in a Set with Finite Diameter
Informal description
For any subset $s$ of a pseudometric space $\alpha$ with finite extended diameter (i.e., $\text{EMetric.diam}(s) \neq \infty$), and for any two points $x, y \in s$, the distance between $x$ and $y$ is bounded by the diameter of $s$, i.e., $\text{dist}(x, y) \leq \text{diam}(s)$.
Metric.isBounded_iff_ediam_ne_top theorem
: IsBounded s ↔ EMetric.diam s ≠ ⊤
Full source 
/-- Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter. -/
theorem isBounded_iff_ediam_ne_top : IsBoundedIsBounded s ↔ EMetric.diam s ≠ ⊤ :=
  isBounded_iff.trans <| Iff.intro
    (fun ⟨_C, hC⟩ => ne_top_of_le_ne_top ENNReal.ofReal_ne_top <| ediam_le_of_forall_dist_le hC)
    fun h => ⟨diam s, fun _x hx _y hy => dist_le_diam_of_mem' h hx hy⟩
Boundedness Criterion via Finite Extended Diameter
Informal description
A subset $s$ of a pseudometric space is bounded if and only if its extended metric diameter $\text{EMetric.diam}(s)$ is finite (i.e., not equal to $\infty$).
Metric.ediam_eq_top_iff_unbounded theorem
: EMetric.diam s = ⊤ ↔ ¬IsBounded s
Full source 
theorem ediam_eq_top_iff_unbounded : EMetric.diamEMetric.diam s = ⊤ ↔ ¬IsBounded s :=
  isBounded_iff_ediam_ne_top.not_left.symm
Extended Diameter Equals Infinity if and only if Unbounded
Informal description
For any subset $s$ of a pseudometric space, the extended metric diameter of $s$ is equal to infinity if and only if $s$ is not bounded, i.e., $\text{EMetric.diam}(s) = \infty \leftrightarrow \neg \text{IsBounded}(s)$.
Metric.ediam_univ_eq_top_iff_noncompact theorem
[ProperSpace α] : EMetric.diam (univ : Set α) = ∞ ↔ NoncompactSpace α
Full source 
theorem ediam_univ_eq_top_iff_noncompact [ProperSpace α] :
    EMetric.diamEMetric.diam (univ : Set α) = ∞ ↔ NoncompactSpace α := by
  rw [← not_compactSpace_iff, compactSpace_iff_isBounded_univ, isBounded_iff_ediam_ne_top,
    Classical.not_not]
Extended Diameter of Universal Set Equals Infinity if and only if Space is Noncompact in Proper Pseudometric Spaces
Informal description
For a proper pseudometric space $\alpha$, the extended diameter of the universal set $\text{EMetric.diam}(\text{univ})$ is equal to infinity if and only if $\alpha$ is noncompact.
Metric.ediam_univ_of_noncompact theorem
[ProperSpace α] [NoncompactSpace α] : EMetric.diam (univ : Set α) = ∞
Full source 
@[simp]
theorem ediam_univ_of_noncompact [ProperSpace α] [NoncompactSpace α] :
    EMetric.diam (univ : Set α) = ∞ :=
  ediam_univ_eq_top_iff_noncompact.mpr ‹_›
Infinite Extended Diameter of Universal Set in Noncompact Proper Pseudometric Spaces
Informal description
In a proper pseudometric space $\alpha$, if $\alpha$ is noncompact, then the extended diameter of the universal set is infinite, i.e., $\text{EMetric.diam}(\text{univ}) = \infty$.
Metric.diam_univ_of_noncompact theorem
[ProperSpace α] [NoncompactSpace α] : diam (univ : Set α) = 0
Full source 
@[simp]
theorem diam_univ_of_noncompact [ProperSpace α] [NoncompactSpace α] : diam (univ : Set α) = 0 := by
  simp [diam]
Zero Diameter of Universal Set in Noncompact Proper Pseudometric Spaces
Informal description
In a proper pseudometric space $\alpha$, if $\alpha$ is noncompact, then the diameter of the universal set is zero, i.e., $\text{diam}(\text{univ}) = 0$.
Metric.dist_le_diam_of_mem theorem
(h : IsBounded s) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ diam s
Full source 
/-- The distance between two points in a set is controlled by the diameter of the set. -/
theorem dist_le_diam_of_mem (h : IsBounded s) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ diam s :=
  dist_le_diam_of_mem' h.ediam_ne_top hx hy
Distance Bound by Diameter for Points in a Bounded Set
Informal description
For any bounded subset $s$ of a pseudometric space $\alpha$, and for any two points $x, y \in s$, the distance between $x$ and $y$ is bounded by the diameter of $s$, i.e., $\text{dist}(x, y) \leq \text{diam}(s)$.
Metric.ediam_of_unbounded theorem
(h : ¬IsBounded s) : EMetric.diam s = ∞
Full source 
theorem ediam_of_unbounded (h : ¬IsBounded s) : EMetric.diam s = ∞ := ediam_eq_top_iff_unbounded.2 h
Extended Diameter is Infinite for Unbounded Sets
Informal description
For any subset $s$ of a pseudometric space, if $s$ is not bounded, then the extended metric diameter of $s$ is infinite, i.e., $\text{EMetric.diam}(s) = \infty$.
Metric.diam_eq_zero_of_unbounded theorem
(h : ¬IsBounded s) : diam s = 0
Full source 
/-- 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 diam_eq_zero_of_unbounded (h : ¬IsBounded s) : diam s = 0 := by
  rw [diam, ediam_of_unbounded h, ENNReal.toReal_top]
Unbounded Sets Have Zero Diameter
Informal description
For any subset $s$ of a pseudometric space, if $s$ is not bounded, then the diameter of $s$ is zero, i.e., $\text{diam}(s) = 0$.
Metric.diam_mono theorem
{s t : Set α} (h : s ⊆ t) (ht : IsBounded t) : diam s ≤ diam t
Full source 
/-- If `s ⊆ t`, then the diameter of `s` is bounded by that of `t`, provided `t` is bounded. -/
theorem diam_mono {s t : Set α} (h : s ⊆ t) (ht : IsBounded t) : diam s ≤ diam t :=
  ENNReal.toReal_mono ht.ediam_ne_top <| EMetric.diam_mono h
Monotonicity of Diameter under Subset Inclusion in Bounded Sets
Informal description
For any subsets $s$ and $t$ of a pseudometric space $\alpha$, if $s$ is contained in $t$ and $t$ is bounded, then the diameter of $s$ is less than or equal to the diameter of $t$, i.e., $\text{diam}(s) \leq \text{diam}(t)$.
Metric.diam_union theorem
{t : Set α} (xs : x ∈ s) (yt : y ∈ t) : diam (s ∪ t) ≤ diam s + dist x y + diam t
Full source 
/-- 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 diam_union {t : Set α} (xs : x ∈ s) (yt : y ∈ t) :
    diam (s ∪ t) ≤ diam s + dist x y + diam t := by
  simp only [diam, dist_edist]
  refine (ENNReal.toReal_le_add' (EMetric.diam_union xs yt) ?_ ?_).trans
    (add_le_add_right ENNReal.toReal_add_le _)
  · simp only [ENNReal.add_eq_top, edist_ne_top, or_false]
    exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono subset_union_left
  · exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono subset_union_right
Diameter Bound for Union of Two Sets in a Pseudometric Space
Informal description
Let $s$ and $t$ be subsets of a pseudometric space $\alpha$, and let $x \in s$ and $y \in t$ be points in these sets. Then the diameter of the union $s \cup t$ satisfies the inequality: \[ \text{diam}(s \cup t) \leq \text{diam}(s) + \text{dist}(x, y) + \text{diam}(t). \]
Metric.diam_union' theorem
{t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t
Full source 
/-- If two sets intersect, the diameter of the union is bounded by the sum of the diameters. -/
theorem diam_union' {t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t := by
  rcases h with ⟨x, ⟨xs, xt⟩⟩
  simpa using diam_union xs xt
Diameter Bound for Union of Intersecting Sets in Pseudometric Spaces
Informal description
Let $s$ and $t$ be subsets of a pseudometric space $\alpha$ such that their intersection $s \cap t$ is nonempty. Then the diameter of their union satisfies: \[ \text{diam}(s \cup t) \leq \text{diam}(s) + \text{diam}(t). \]
Metric.diam_le_of_subset_closedBall theorem
{r : ℝ} (hr : 0 ≤ r) (h : s ⊆ closedBall x r) : diam s ≤ 2 * r
Full source 
theorem diam_le_of_subset_closedBall {r : ℝ} (hr : 0 ≤ r) (h : s ⊆ closedBall x r) :
    diam s ≤ 2 * r :=
  diam_le_of_forall_dist_le (mul_nonneg zero_le_two hr) fun a ha b hb =>
    calc
      dist a b ≤ dist a x + dist b x := dist_triangle_right _ _ _
      _ ≤ r + r := add_le_add (h ha) (h hb)
      _ = 2 * r := by simp [mul_two, mul_comm]
Diameter Bound for Subset of Closed Ball: $\text{diam}(s) \leq 2r$
Informal description
Let $s$ be a subset of a pseudometric space $\alpha$, and let $x \in \alpha$ and $r \geq 0$ be a real number. If $s$ is contained in the closed ball $\overline{B}(x, r)$, then the diameter of $s$ satisfies $\text{diam}(s) \leq 2r$.
Metric.diam_closedBall theorem
{r : ℝ} (h : 0 ≤ r) : diam (closedBall x r) ≤ 2 * r
Full source 
/-- The diameter of a closed ball of radius `r` is at most `2 r`. -/
theorem diam_closedBall {r : ℝ} (h : 0 ≤ r) : diam (closedBall x r) ≤ 2 * r :=
  diam_le_of_subset_closedBall h Subset.rfl
Diameter Bound for Closed Ball: $\text{diam}(\overline{B}(x, r)) \leq 2r$
Informal description
For any non-negative real number $r \geq 0$, the diameter of the closed ball $\overline{B}(x, r)$ in a pseudometric space is at most $2r$, i.e., \[ \text{diam}(\overline{B}(x, r)) \leq 2r. \]
Metric.diam_ball theorem
{r : ℝ} (h : 0 ≤ r) : diam (ball x r) ≤ 2 * r
Full source 
/-- The diameter of a ball of radius `r` is at most `2 r`. -/
theorem diam_ball {r : ℝ} (h : 0 ≤ r) : diam (ball x r) ≤ 2 * r :=
  diam_le_of_subset_closedBall h ball_subset_closedBall
Diameter Bound for Open Ball: $\text{diam}(B(x, r)) \leq 2r$
Informal description
For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $r$, the diameter of the open ball $\text{ball}(x, r)$ is at most $2r$. That is, $\text{diam}(\text{ball}(x, r)) \leq 2r$.
IsComplete.nonempty_iInter_of_nonempty_biInter theorem
{s : ℕ → Set α} (h0 : IsComplete (s 0)) (hs : ∀ n, IsClosed (s n)) (h's : ∀ n, IsBounded (s n)) (h : ∀ N, (⋂ n ≤ N, s n).Nonempty) (h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)) : (⋂ n, s n).Nonempty
Full source 
/-- 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 _root_.IsComplete.nonempty_iInter_of_nonempty_biInter {s : ℕ → Set α}
    (h0 : IsComplete (s 0)) (hs : ∀ n, IsClosed (s n)) (h's : ∀ n, IsBounded (s n))
    (h : ∀ N, (⋂ n ≤ N, s n).Nonempty) (h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)) :
    (⋂ n, s n).Nonempty := by
  let u N := (h N).some
  have I : ∀ n N, n ≤ N → u N ∈ s n := by
    intro n N hn
    apply mem_of_subset_of_mem _ (h N).choose_spec
    intro x hx
    simp only [mem_iInter] at hx
    exact hx n hn
  have : CauchySeq u := by
    apply cauchySeq_of_le_tendsto_0 _ _ h'
    intro m n N hm hn
    exact dist_le_diam_of_mem (h's N) (I _ _ hm) (I _ _ hn)
  obtain ⟨x, -, xlim⟩ : ∃ x ∈ s 0, Tendsto (fun n : ℕ => u n) atTop (𝓝 x) :=
    cauchySeq_tendsto_of_isComplete h0 (fun n => I 0 n (zero_le _)) this
  refine ⟨x, mem_iInter.2 fun n => ?_⟩
  apply (hs n).mem_of_tendsto xlim
  filter_upwards [Ici_mem_atTop n] with p hp
  exact I n p hp
Cantor's Intersection Theorem for Complete Pseudometric Spaces
Informal description
Let $\alpha$ be a pseudometric space and $(s_n)_{n \in \mathbb{N}}$ a sequence of subsets of $\alpha$ satisfying: 1. The first set $s_0$ is complete; 2. Each $s_n$ is closed; 3. Each $s_n$ is bounded; 4. For every $N \in \mathbb{N}$, the finite intersection $\bigcap_{n \leq N} s_n$ is nonempty; 5. The diameters of $s_n$ tend to $0$ as $n \to \infty$. Then the infinite intersection $\bigcap_{n \in \mathbb{N}} s_n$ is nonempty.
Metric.nonempty_iInter_of_nonempty_biInter theorem
[CompleteSpace α] {s : ℕ → Set α} (hs : ∀ n, IsClosed (s n)) (h's : ∀ n, IsBounded (s n)) (h : ∀ N, (⋂ n ≤ N, s n).Nonempty) (h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)) : (⋂ n, s n).Nonempty
Full source 
/-- 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. -/
theorem nonempty_iInter_of_nonempty_biInter [CompleteSpace α] {s : ℕ → Set α}
    (hs : ∀ n, IsClosed (s n)) (h's : ∀ n, IsBounded (s n)) (h : ∀ N, (⋂ n ≤ N, s n).Nonempty)
    (h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)) : (⋂ n, s n).Nonempty :=
  (hs 0).isComplete.nonempty_iInter_of_nonempty_biInter hs h's h h'
Cantor's Intersection Theorem for Complete Pseudometric Spaces
Informal description
Let $\alpha$ be a complete pseudometric space and $(s_n)_{n \in \mathbb{N}}$ be a sequence of subsets of $\alpha$ such that: 1. Each $s_n$ is closed; 2. Each $s_n$ is bounded; 3. For every $N \in \mathbb{N}$, the finite intersection $\bigcap_{n \leq N} s_n$ is nonempty; 4. The diameters of $s_n$ tend to $0$ as $n \to \infty$. Then the infinite intersection $\bigcap_{n \in \mathbb{N}} s_n$ is nonempty.
Mathlib.Meta.Positivity.evalDiam definition
: PositivityExt
Full source 
/-- Extension for the `positivity` tactic: the diameter of a set is always nonnegative. -/
@[positivity Metric.diam _]
def evalDiam : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(@Metric.diam _ $inst $s) =>
    assertInstancesCommute
    pure (.nonnegative q(Metric.diam_nonneg))
  | _, _, _ => throwError "not ‖ · ‖"
Nonnegativity of metric diameter
Informal description
The diameter of a subset in a metric space is always nonnegative. This is an extension for the `positivity` tactic, which automatically proves nonnegativity of the diameter.
Metric.cobounded_eq_cocompact theorem
[ProperSpace α] : cobounded α = cocompact α
Full source 
theorem Metric.cobounded_eq_cocompact [ProperSpace α] : cobounded α = cocompact α := by
  nontriviality α; inhabit α
  exact cobounded_le_cocompact.antisymm <| (hasBasis_cobounded_compl_closedBall default).ge_iff.2
    fun _ _ ↦ (isCompact_closedBall _ _).compl_mem_cocompact
Cobounded and Cocompact Filters Coincide in Proper Spaces
Informal description
In a proper pseudometric space $\alpha$, the cobounded filter coincides with the cocompact filter. That is, a subset of $\alpha$ is cobounded if and only if it is cocompact.
tendsto_dist_right_cocompact_atTop theorem
[ProperSpace α] (x : α) : Tendsto (dist · x) (cocompact α) atTop
Full source 
theorem tendsto_dist_right_cocompact_atTop [ProperSpace α] (x : α) :
    Tendsto (dist · x) (cocompact α) atTop :=
  (tendsto_dist_right_cobounded_atTop x).mono_left cobounded_eq_cocompact.ge
Distance to a Fixed Point Tends to Infinity Along the Cocompact Filter in Proper Spaces
Informal description
In a proper pseudometric space $\alpha$, for any point $x \in \alpha$, the function $y \mapsto \text{dist}(y, x)$ tends to infinity along the cocompact filter of $\alpha$.
tendsto_dist_left_cocompact_atTop theorem
[ProperSpace α] (x : α) : Tendsto (dist x) (cocompact α) atTop
Full source 
theorem tendsto_dist_left_cocompact_atTop [ProperSpace α] (x : α) :
    Tendsto (dist x) (cocompact α) atTop :=
  (tendsto_dist_left_cobounded_atTop x).mono_left cobounded_eq_cocompact.ge
Distance from Fixed Point Tends to Infinity Along Cocompact Filter in Proper Spaces
Informal description
In a proper pseudometric space $\alpha$, for any point $x \in \alpha$, the function $y \mapsto \text{dist}(x, y)$ tends to infinity along the cocompact filter of $\alpha$.
comap_dist_left_atTop_eq_cocompact theorem
[ProperSpace α] (x : α) : comap (dist x) atTop = cocompact α
Full source 
theorem comap_dist_left_atTop_eq_cocompact [ProperSpace α] (x : α) :
    comap (dist x) atTop = cocompact α := by simp [cobounded_eq_cocompact]
Preimage of Distance Function Equals Cocompact Filter in Proper Spaces
Informal description
In a proper pseudometric space $\alpha$, for any point $x \in \alpha$, the preimage of the filter at infinity under the distance function $y \mapsto \text{dist}(x, y)$ is equal to the cocompact filter on $\alpha$. That is, $\text{comap} (\text{dist}(x, \cdot)) \ \text{atTop} = \text{cocompact} \ \alpha$.
tendsto_cocompact_of_tendsto_dist_comp_atTop theorem
{f : β → α} {l : Filter β} (x : α) (h : Tendsto (fun y => dist (f y) x) l atTop) : Tendsto f l (cocompact α)
Full source 
theorem tendsto_cocompact_of_tendsto_dist_comp_atTop {f : β → α} {l : Filter β} (x : α)
    (h : Tendsto (fun y => dist (f y) x) l atTop) : Tendsto f l (cocompact α) :=
  ((tendsto_dist_right_atTop_iff _).1 h).mono_right cobounded_le_cocompact
Convergence to Cocompact Filter via Divergent Distance Function
Informal description
Let $\alpha$ be a pseudometric space, $x \in \alpha$ a fixed point, and $f : \beta \to \alpha$ a function. If the function $y \mapsto \text{dist}(f(y), x)$ tends to infinity along a filter $l$ on $\beta$, then $f$ tends to the cocompact filter of $\alpha$ along $l$.
Metric.finite_isBounded_inter_isClosed theorem
[ProperSpace α] {K s : Set α} [DiscreteTopology s] (hK : IsBounded K) (hs : IsClosed s) : Set.Finite (K ∩ s)
Full source 
theorem Metric.finite_isBounded_inter_isClosed [ProperSpace α] {K s : Set α} [DiscreteTopology s]
    (hK : IsBounded K) (hs : IsClosed s) : Set.Finite (K ∩ s) := by
  refine Set.Finite.subset (IsCompact.finite ?_ ?_) (Set.inter_subset_inter_left s subset_closure)
  · exact hK.isCompact_closure.inter_right hs
  · exact DiscreteTopology.of_subset inferInstance Set.inter_subset_right
Finite Intersection of Bounded and Closed Discrete Sets in Proper Spaces
Informal description
Let $\alpha$ be a proper pseudometric space, and let $K, s \subseteq \alpha$ be subsets such that: 1. $K$ is bounded, 2. $s$ is closed and has the discrete topology (as a subspace). Then the intersection $K \cap s$ is finite.