doc-next-gen

Mathlib.Topology.EMetricSpace.Basic

Module docstring

{"# Extended metric spaces

Further results about extended metric spaces. ","### Separation quotient "}

edist_le_Ico_sum_edist theorem
(f : ℕ → α) {m n} (h : m ≤ n) : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
Full source 
/-- The triangle (polygon) inequality for sequences of points; `Finset.Ico` version. -/
theorem edist_le_Ico_sum_edist (f : ℕ → α) {m n} (h : m ≤ n) :
    edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) := by
  induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, edist_self]
  | succ n hle ihn =>
    calc
      edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
      _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
      _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
      { rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp }
Triangle Inequality for Extended Distances over Finite Intervals
Informal description
For any sequence of points $(f_n)$ in a pseudo extended metric space $\alpha$ and any natural numbers $m \leq n$, the extended distance between $f_m$ and $f_n$ is bounded by the sum of the extended distances between consecutive points in the sequence over the interval $[m, n)$. That is, $$ \text{edist}(f_m, f_n) \leq \sum_{i \in [m, n)} \text{edist}(f_i, f_{i+1}). $$
edist_le_range_sum_edist theorem
(f : ℕ → α) (n : ℕ) : edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, edist (f i) (f (i + 1))
Full source 
/-- The triangle (polygon) inequality for sequences of points; `Finset.range` version. -/
theorem edist_le_range_sum_edist (f : ℕ → α) (n : ℕ) :
    edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, edist (f i) (f (i + 1)) :=
  Nat.Ico_zero_eq_range ▸ edist_le_Ico_sum_edist f (Nat.zero_le n)
Triangle Inequality for Extended Distances over Initial Segments
Informal description
For any sequence of points $(f_n)$ in a pseudo extended metric space $\alpha$ and any natural number $n$, the extended distance between the initial point $f_0$ and the $n$-th point $f_n$ is bounded by the sum of the extended distances between consecutive points in the sequence up to $n$. That is, $$ \text{edist}(f_0, f_n) \leq \sum_{i=0}^{n-1} \text{edist}(f_i, f_{i+1}). $$
edist_le_Ico_sum_of_edist_le theorem
{f : ℕ → α} {m n} (hmn : m ≤ n) {d : ℕ → ℝ≥0∞} (hd : ∀ {k}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i
Full source 
/-- A version of `edist_le_Ico_sum_edist` with each intermediate distance replaced
with an upper estimate. -/
theorem edist_le_Ico_sum_of_edist_le {f : ℕ → α} {m n} (hmn : m ≤ n) {d : ℕ → ℝ≥0∞}
    (hd : ∀ {k}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) :
    edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i :=
  le_trans (edist_le_Ico_sum_edist f hmn) <|
    Finset.sum_le_sum fun _k hk => hd (Finset.mem_Ico.1 hk).1 (Finset.mem_Ico.1 hk).2
Upper Bound on Extended Distance via Sum of Estimates over Interval $[m, n)$
Informal description
Let $\alpha$ be a pseudo extended metric space and $f : \mathbb{N} \to \alpha$ be a sequence of points in $\alpha$. For any natural numbers $m \leq n$ and a sequence of extended nonnegative real numbers $d : \mathbb{N} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, if for all $k$ with $m \leq k < n$ we have $\text{edist}(f_k, f_{k+1}) \leq d_k$, then the extended distance between $f_m$ and $f_n$ is bounded by the sum of $d_i$ over the interval $[m, n)$. That is, $$ \text{edist}(f_m, f_n) \leq \sum_{i \in [m, n)} d_i. $$
edist_le_range_sum_of_edist_le theorem
{f : ℕ → α} (n : ℕ) {d : ℕ → ℝ≥0∞} (hd : ∀ {k}, k < n → edist (f k) (f (k + 1)) ≤ d k) : edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i
Full source 
/-- A version of `edist_le_range_sum_edist` with each intermediate distance replaced
with an upper estimate. -/
theorem edist_le_range_sum_of_edist_le {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ≥0∞}
    (hd : ∀ {k}, k < n → edist (f k) (f (k + 1)) ≤ d k) :
    edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i :=
  Nat.Ico_zero_eq_range ▸ edist_le_Ico_sum_of_edist_le (zero_le n) fun _ => hd
Upper Bound on Extended Distance via Sum of Estimates over Initial Segment
Informal description
Let $\alpha$ be a pseudo extended metric space and $f : \mathbb{N} \to \alpha$ be a sequence of points in $\alpha$. For any natural number $n$ and a sequence of extended nonnegative real numbers $d : \mathbb{N} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, if for all $k < n$ we have $\text{edist}(f_k, f_{k+1}) \leq d_k$, then the extended distance between $f_0$ and $f_n$ is bounded by the sum of $d_i$ over the range $\{0, \dots, n-1\}$. That is, $$ \text{edist}(f_0, f_n) \leq \sum_{i=0}^{n-1} d_i. $$
EMetric.isUniformInducing_iff theorem
[PseudoEMetricSpace β] {f : α → β} : IsUniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
Full source 
theorem isUniformInducing_iff [PseudoEMetricSpace β] {f : α → β} :
    IsUniformInducingIsUniformInducing f ↔ UniformContinuous f ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ :=
  isUniformInducing_iff'.trans <| Iff.rfl.and <|
    ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).trans <| by
      simp only [subset_def, Prod.forall]; rfl
Characterization of Uniform Inducing Maps in Pseudo Extended Metric Spaces via Uniform Continuity and Distance Control
Informal description
Let $\alpha$ and $\beta$ be pseudo extended metric spaces, and let $f \colon \alpha \to \beta$ be a function. Then $f$ is a uniform inducing map if and only if $f$ is uniformly continuous and for every $\delta > 0$, there exists $\varepsilon > 0$ such that for all $a, b \in \alpha$, if the extended distance $\text{edist}(f(a), f(b)) < \varepsilon$, then $\text{edist}(a, b) < \delta$.
EMetric.isUniformEmbedding_iff theorem
[PseudoEMetricSpace β] {f : α → β} : IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
Full source 
/-- ε-δ characterization of uniform embeddings on pseudoemetric spaces -/
nonrec theorem isUniformEmbedding_iff [PseudoEMetricSpace β] {f : α → β} :
    IsUniformEmbeddingIsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ :=
  (isUniformEmbedding_iff _).trans <| and_comm.trans <| Iff.rfl.and isUniformInducing_iff
$\varepsilon$-$\delta$ Characterization of Uniform Embeddings in Pseudo Extended Metric Spaces
Informal description
Let $\alpha$ and $\beta$ be pseudo extended metric spaces, and let $f \colon \alpha \to \beta$ be a function. Then $f$ is a uniform embedding if and only if the following conditions hold: 1. $f$ is injective, 2. $f$ is uniformly continuous, and 3. For every $\delta > 0$, there exists $\varepsilon > 0$ such that for all $a, b \in \alpha$, if $\text{edist}(f(a), f(b)) < \varepsilon$, then $\text{edist}(a, b) < \delta$.
EMetric.controlled_of_isUniformEmbedding theorem
[PseudoEMetricSpace β] {f : α → β} (h : IsUniformEmbedding f) : (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
Full source 
/-- If a map between pseudoemetric spaces is a uniform embedding then the edistance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y`.

In fact, this lemma holds for a `IsUniformInducing` map.
TODO: generalize? -/
theorem controlled_of_isUniformEmbedding [PseudoEMetricSpace β] {f : α → β}
    (h : IsUniformEmbedding f) :
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ :=
  ⟨uniformContinuous_iff.1 h.uniformContinuous, (isUniformEmbedding_iff.1 h).2.2⟩
$\varepsilon$-$\delta$ Control of Extended Distances under Uniform Embeddings
Informal description
Let $\alpha$ and $\beta$ be pseudo extended metric spaces, and let $f \colon \alpha \to \beta$ be a uniform embedding. Then: 1. For every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $a, b \in \alpha$, if $\text{edist}(a, b) < \delta$, then $\text{edist}(f(a), f(b)) < \varepsilon$. 2. For every $\delta > 0$, there exists $\varepsilon > 0$ such that for all $a, b \in \alpha$, if $\text{edist}(f(a), f(b)) < \varepsilon$, then $\text{edist}(a, b) < \delta$.
EMetric.cauchy_iff theorem
{f : Filter α} : Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x, x ∈ t → ∀ y, y ∈ t → edist x y < ε
Full source 
/-- ε-δ characterization of Cauchy sequences on pseudoemetric spaces -/
protected theorem cauchy_iff {f : Filter α} :
    CauchyCauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x, x ∈ t → ∀ y, y ∈ t → edist x y < ε := by
  rw [← neBot_iff]; exact uniformity_basis_edist.cauchy_iff
$\varepsilon$-$\delta$ Characterization of Cauchy Filters in Pseudo Extended Metric Spaces
Informal description
A filter $f$ on a pseudo extended metric space $\alpha$ is Cauchy if and only if $f$ is non-trivial (i.e., $f \neq \bot$) and for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists a set $t \in f$ such that for all $x, y \in t$, the extended distance between $x$ and $y$ satisfies $\text{edist}(x, y) < \varepsilon$.
EMetric.complete_of_convergent_controlled_sequences theorem
(B : ℕ → ℝ≥0∞) (hB : ∀ n, 0 < B n) (H : ∀ u : ℕ → α, (∀ N n m : ℕ, N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃ x, Tendsto u atTop (𝓝 x)) : CompleteSpace α
Full source 
/-- A very useful criterion to show that a space is complete is to show that all sequences
which satisfy a bound of the form `edist (u n) (u m) < B N` for all `n m ≥ N` are
converging. This is often applied for `B N = 2^{-N}`, i.e., with a very fast convergence to
`0`, which makes it possible to use arguments of converging series, while this is impossible
to do in general for arbitrary Cauchy sequences. -/
theorem complete_of_convergent_controlled_sequences (B : ℕ → ℝ≥0∞) (hB : ∀ n, 0 < B n)
    (H : ∀ u : ℕ → α, (∀ N n m : ℕ, N ≤ n → N ≤ m → edist (u n) (u m) < B N) →
      ∃ x, Tendsto u atTop (𝓝 x)) :
    CompleteSpace α :=
  UniformSpace.complete_of_convergent_controlled_sequences
    (fun n => { p : α × α | edist p.1 p.2 < B n }) (fun n => edist_mem_uniformity <| hB n) H
Completeness Criterion via Controlled Cauchy Sequences in Pseudo Extended Metric Spaces
Informal description
Let $\alpha$ be a pseudo extended metric space and let $B \colon \mathbb{N} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ be a sequence of positive extended real numbers. Suppose that for every sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ satisfying the controlled Cauchy condition \[ \forall N\ n\ m,\ N \leq n \land N \leq m \implies \text{edist}(u_n, u_m) < B_N, \] there exists a point $x \in \alpha$ such that $u_n$ converges to $x$ as $n \to \infty$. Then $\alpha$ is a complete space.
EMetric.complete_of_cauchySeq_tendsto theorem
: (∀ u : ℕ → α, CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)) → CompleteSpace α
Full source 
/-- A sequentially complete pseudoemetric space is complete. -/
theorem complete_of_cauchySeq_tendsto :
    (∀ u : ℕ → α, CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)) → CompleteSpace α :=
  UniformSpace.complete_of_cauchySeq_tendsto
Completeness via convergent Cauchy sequences in pseudo extended metric spaces
Informal description
A pseudo extended metric space $\alpha$ is complete if every Cauchy sequence $u : \mathbb{N} \to \alpha$ converges to some point in $\alpha$.
EMetric.tendstoLocallyUniformlyOn_iff theorem
{ι : Type*} [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} : TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε
Full source 
/-- Expressing locally uniform convergence on a set using `edist`. -/
theorem tendstoLocallyUniformlyOn_iff {ι : Type*} [TopologicalSpace β] {F : ι → β → α} {f : β → α}
    {p : Filter ι} {s : Set β} :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p s ↔
      ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε := by
  refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu x hx => ?_⟩
  rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩
  rcases H ε εpos x hx with ⟨t, ht, Ht⟩
  exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩
Characterization of Locally Uniform Convergence on a Set via Extended Distance
Informal description
Let $\alpha$ be a pseudo extended metric space, $\beta$ a topological space, $F_n \colon \beta \to \alpha$ a sequence of functions, $f \colon \beta \to \alpha$ a function, $p$ a filter on the index set $\iota$, and $s \subseteq \beta$. The sequence $F_n$ converges locally uniformly on $s$ to $f$ with respect to $p$ if and only if for every $\varepsilon > 0$ and every $x \in s$, there exists a neighborhood $t$ of $x$ in $s$ such that for all $n$ eventually in $p$, the extended distance satisfies $\text{edist}(f(y), F_n(y)) < \varepsilon$ for all $y \in t$.
EMetric.tendstoUniformlyOn_iff theorem
{ι : Type*} {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} : TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, edist (f x) (F n x) < ε
Full source 
/-- Expressing uniform convergence on a set using `edist`. -/
theorem tendstoUniformlyOn_iff {ι : Type*} {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} :
    TendstoUniformlyOnTendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, edist (f x) (F n x) < ε := by
  refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu => ?_⟩
  rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩
  exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)
Uniform Convergence on a Set via Extended Distance Criterion
Informal description
Let $\alpha$ be a pseudo extended metric space, $\beta$ be a type, $\iota$ be an index type, $F_n \colon \beta \to \alpha$ be a family of functions indexed by $n \in \iota$, $f \colon \beta \to \alpha$ be a function, $p$ be a filter on $\iota$, and $s \subseteq \beta$ be a set. The family $F_n$ converges uniformly to $f$ on $s$ with respect to $p$ if and only if for every $\varepsilon > 0$, there exists an event in $p$ such that for all $n$ in this event and all $x \in s$, the extended distance satisfies $\text{edist}(f(x), F_n(x)) < \varepsilon$.
EMetric.tendstoLocallyUniformly_iff theorem
{ι : Type*} [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ x : β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε
Full source 
/-- Expressing locally uniform convergence using `edist`. -/
theorem tendstoLocallyUniformly_iff {ι : Type*} [TopologicalSpace β] {F : ι → β → α} {f : β → α}
    {p : Filter ι} :
    TendstoLocallyUniformlyTendstoLocallyUniformly F f p ↔
      ∀ ε > 0, ∀ x : β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε := by
  simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, mem_univ,
    forall_const, exists_prop, nhdsWithin_univ]
Characterization of Locally Uniform Convergence via Extended Distance
Informal description
Let $\alpha$ be a pseudo extended metric space and $\beta$ be a topological space. A sequence of functions $F_n \colon \beta \to \alpha$ converges locally uniformly to a function $f \colon \beta \to \alpha$ with respect to a filter $p$ on the index set if and only if for every $\varepsilon > 0$ and every point $x \in \beta$, there exists a neighborhood $t$ of $x$ such that for all $n$ eventually in $p$, the extended distance $\text{edist}(f(y), F_n(y)) < \varepsilon$ holds for all $y \in t$.
EMetric.tendstoUniformly_iff theorem
{ι : Type*} {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, edist (f x) (F n x) < ε
Full source 
/-- Expressing uniform convergence using `edist`. -/
theorem tendstoUniformly_iff {ι : Type*} {F : ι → β → α} {f : β → α} {p : Filter ι} :
    TendstoUniformlyTendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, edist (f x) (F n x) < ε := by
  simp only [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff, mem_univ, forall_const]
Uniform Convergence Criterion via Extended Distance
Informal description
Let $\alpha$ be a pseudo extended metric space, $\beta$ be a type, and $\iota$ be an index type. A family of functions $F_n : \beta \to \alpha$ indexed by $n \in \iota$ converges uniformly to a function $f : \beta \to \alpha$ with respect to a filter $p$ on $\iota$ if and only if for every $\varepsilon > 0$, there exists an event in $p$ such that for all $n$ in this event and all $x \in \beta$, the extended distance between $f(x)$ and $F_n(x)$ is less than $\varepsilon$, i.e., $\text{edist}(f(x), F_n(x)) < \varepsilon$.
EMetric.cauchySeq_iff theorem
[Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → edist (u m) (u n) < ε
Full source 
/-- In a pseudoemetric space, Cauchy sequences are characterized by the fact that, eventually,
the pseudoedistance between its elements is arbitrarily small -/
theorem cauchySeq_iff [Nonempty β] [SemilatticeSup β] {u : β → α} :
    CauchySeqCauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → edist (u m) (u n) < ε :=
  uniformity_basis_edist.cauchySeq_iff
Cauchy Sequence Criterion in Pseudo Extended Metric Spaces: $\forall \varepsilon > 0, \exists N, \forall m, n \geq N, \text{edist}(u(m), u(n)) < \varepsilon$
Informal description
Let $\alpha$ be a pseudo extended metric space, $\beta$ be a nonempty directed set (join-semilattice), and $u : \beta \to \alpha$ be a sequence. Then $u$ is a Cauchy sequence if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists $N \in \beta$ such that for all $m, n \geq N$, the extended distance between $u(m)$ and $u(n)$ satisfies $\text{edist}(u(m), u(n)) < \varepsilon$.
EMetric.cauchySeq_iff' theorem
[Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ ε > (0 : ℝ≥0∞), ∃ N, ∀ n ≥ N, edist (u n) (u N) < ε
Full source 
/-- A variation around the emetric characterization of Cauchy sequences -/
theorem cauchySeq_iff' [Nonempty β] [SemilatticeSup β] {u : β → α} :
    CauchySeqCauchySeq u ↔ ∀ ε > (0 : ℝ≥0∞), ∃ N, ∀ n ≥ N, edist (u n) (u N) < ε :=
  uniformity_basis_edist.cauchySeq_iff'
Characterization of Cauchy Sequences in Pseudo Extended Metric Spaces via Extended Distance
Informal description
Let $\beta$ be a nonempty directed set (specifically, a nonempty join-semilattice) and let $u : \beta \to \alpha$ be a sequence in a pseudo extended metric space $\alpha$. Then $u$ is a Cauchy sequence if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists an index $N \in \beta$ such that for all $n \geq N$, the extended distance between $u(n)$ and $u(N)$ is less than $\varepsilon$, i.e., $\text{edist}(u(n), u(N)) < \varepsilon$.
EMetric.cauchySeq_iff_NNReal theorem
[Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ ε : ℝ≥0, 0 < ε → ∃ N, ∀ n, N ≤ n → edist (u n) (u N) < ε
Full source 
/-- A variation of the emetric characterization of Cauchy sequences that deals with
`ℝ≥0` upper bounds. -/
theorem cauchySeq_iff_NNReal [Nonempty β] [SemilatticeSup β] {u : β → α} :
    CauchySeqCauchySeq u ↔ ∀ ε : ℝ≥0, 0 < ε → ∃ N, ∀ n, N ≤ n → edist (u n) (u N) < ε :=
  uniformity_basis_edist_nnreal.cauchySeq_iff'
Cauchy Sequence Criterion in Pseudo Extended Metric Spaces via Real Upper Bounds
Informal description
Let $\alpha$ be a pseudo extended metric space, $\beta$ be a nonempty directed set (join-semilattice), and $u : \beta \to \alpha$ be a sequence. Then $u$ is a Cauchy sequence if and only if for every positive real number $\varepsilon \in \mathbb{R}_{\geq 0}$, there exists $N \in \beta$ such that for all $n \geq N$, the extended distance between $u(n)$ and $u(N)$ satisfies $\text{edist}(u(n), u(N)) < \varepsilon$.
EMetric.totallyBounded_iff theorem
{s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
Full source 
theorem totallyBounded_iff {s : Set α} :
    TotallyBoundedTotallyBounded s ↔ ∀ ε > 0, ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε :=
  ⟨fun H _ε ε0 => H _ (edist_mem_uniformity ε0), fun H _r ru =>
    let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru
    let ⟨t, ft, h⟩ := H ε ε0
    ⟨t, ft, h.trans <| iUnion₂_mono fun _ _ _ => hε⟩⟩
Characterization of Totally Bounded Sets in Pseudo Extended Metric Spaces via Finite Coverings
Informal description
A subset $s$ of a pseudo extended metric space $\alpha$ is totally bounded if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists a finite subset $t \subseteq \alpha$ such that $s$ is covered by the union of extended metric balls of radius $\varepsilon$ centered at each point of $t$, i.e., $s \subseteq \bigcup_{y \in t} \text{ball}(y, \varepsilon)$.
EMetric.totallyBounded_iff' theorem
{s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y ε
Full source 
theorem totallyBounded_iff' {s : Set α} :
    TotallyBoundedTotallyBounded s ↔ ∀ ε > 0, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y ε :=
  ⟨fun H _ε ε0 => (totallyBounded_iff_subset.1 H) _ (edist_mem_uniformity ε0), fun H _r ru =>
    let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru
    let ⟨t, _, ft, h⟩ := H ε ε0
    ⟨t, ft, h.trans <| iUnion₂_mono fun _ _ _ => hε⟩⟩
Characterization of totally bounded sets via finite $\varepsilon$-coverings in extended metric spaces
Informal description
A subset $s$ of a pseudo extended metric space $\alpha$ is totally bounded if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists a finite subset $t \subseteq s$ such that $s$ is covered by the extended metric balls of radius $\varepsilon$ centered at points in $t$, i.e., \[ s \subseteq \bigcup_{y \in t} \{x \mid \text{edist}(x, y) < \varepsilon\}. \]
EMetric.subset_countable_closure_of_compact theorem
{s : Set α} (hs : IsCompact s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t
Full source 
/-- A compact set in a pseudo emetric space is separable, i.e., it is a subset of the closure of a
countable set. -/
theorem subset_countable_closure_of_compact {s : Set α} (hs : IsCompact s) :
    ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t := by
  refine subset_countable_closure_of_almost_dense_set s fun ε hε => ?_
  rcases totallyBounded_iff'.1 hs.totallyBounded ε hε with ⟨t, -, htf, hst⟩
  exact ⟨t, htf.countable, hst.trans <| iUnion₂_mono fun _ _ => ball_subset_closedBall⟩
Compact Sets in Pseudo Extended Metric Spaces Have Countable Dense Subsets
Informal description
For any compact subset $s$ of a pseudo extended metric space $\alpha$, there exists a countable subset $t \subseteq s$ such that $s$ is contained in the closure of $t$.
EMetric.secondCountable_of_sigmaCompact instance
[SigmaCompactSpace α] : SecondCountableTopology α
Full source 
/-- A sigma compact pseudo emetric space has second countable topology. -/
instance (priority := 90) secondCountable_of_sigmaCompact [SigmaCompactSpace α] :
    SecondCountableTopology α := by
  suffices SeparableSpace α by exact UniformSpace.secondCountable_of_separable α
  choose T _ hTc hsubT using fun n =>
    subset_countable_closure_of_compact (isCompact_compactCovering α n)
  refine ⟨⟨⋃ n, T n, countable_iUnion hTc, fun x => ?_⟩⟩
  rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering α) x with ⟨n, hn⟩
  exact closure_mono (subset_iUnion _ n) (hsubT _ hn)
Second-Countability of σ-Compact Pseudo Extended Metric Spaces
Informal description
Every σ-compact pseudo extended metric space is second-countable.
EMetric.secondCountable_of_almost_dense_set theorem
(hs : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ) : SecondCountableTopology α
Full source 
theorem secondCountable_of_almost_dense_set
    (hs : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ ⋃ x ∈ t, closedBall x ε = univ) :
    SecondCountableTopology α := by
  suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
  have : ∀ ε > 0, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε := by
    simpa only [univ_subset_iff] using hs
  rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩
  exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩
Second-Countability from $\varepsilon$-Dense Condition in Pseudo Extended Metric Spaces
Informal description
Let $\alpha$ be a pseudo extended metric space. If for every $\varepsilon > 0$ there exists a countable subset $t \subseteq \alpha$ such that the union of closed balls of radius $\varepsilon$ centered at points of $t$ covers the entire space $\alpha$, then $\alpha$ is second-countable.
EMetricSpace.instT0Space instance
: T0Space γ
Full source 
/-- An emetric space is separated -/
instance (priority := 100) EMetricSpace.instT0Space : T0Space γ where
  t0 _ _ h := eq_of_edist_eq_zero <| inseparable_iff.1 h
Extended Metric Spaces are T₀ Spaces
Informal description
Every extended metric space is a T₀ space.
EMetric.isUniformEmbedding_iff' theorem
[PseudoEMetricSpace β] {f : γ → β} : IsUniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
Full source 
/-- A map between emetric spaces is a uniform embedding if and only if the edistance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/
theorem EMetric.isUniformEmbedding_iff' [PseudoEMetricSpace β] {f : γ → β} :
    IsUniformEmbeddingIsUniformEmbedding f ↔
      (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
        ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ := by
  rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]
Characterization of Uniform Embeddings in Pseudo Extended Metric Spaces via $\varepsilon$-$\delta$ Conditions
Informal description
Let $\gamma$ and $\beta$ be pseudo extended metric spaces. A map $f \colon \gamma \to \beta$ is a uniform embedding if and only if the following two conditions hold: 1. (Uniform continuity) For every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $a, b \in \gamma$ with $\text{edist}(a, b) < \delta$, we have $\text{edist}(f(a), f(b)) < \varepsilon$. 2. (Distance control) For every $\delta > 0$, there exists $\varepsilon > 0$ such that for all $a, b \in \gamma$ with $\text{edist}(f(a), f(b)) < \varepsilon$, we have $\text{edist}(a, b) < \delta$.
EMetricSpace.ofT0PseudoEMetricSpace abbrev
(α : Type*) [PseudoEMetricSpace α] [T0Space α] : EMetricSpace α
Full source 
/-- If a `PseudoEMetricSpace` is a T₀ space, then it is an `EMetricSpace`. -/
-- TODO: make it an instance?
abbrev EMetricSpace.ofT0PseudoEMetricSpace (α : Type*) [PseudoEMetricSpace α] [T0Space α] :
    EMetricSpace α :=
  { ‹PseudoEMetricSpace α› with
    eq_of_edist_eq_zero := fun h => (EMetric.inseparable_iff.2 h).eq }
Promotion from Pseudo Extended Metric Space to Extended Metric Space via T₀ Condition
Informal description
Given a pseudo extended metric space $\alpha$ that is also a T₀ space, the space $\alpha$ can be promoted to an extended metric space.
Prod.emetricSpaceMax instance
[EMetricSpace β] : EMetricSpace (γ × β)
Full source 
/-- The product of two emetric spaces, with the max distance, is an extended
metric spaces. We make sure that the uniform structure thus constructed is the one
corresponding to the product of uniform spaces, to avoid diamond problems. -/
instance Prod.emetricSpaceMax [EMetricSpace β] : EMetricSpace (γ × β) :=
  .ofT0PseudoEMetricSpace _
Extended Metric Space Structure on Product Spaces via Maximum Distance
Informal description
The product $\gamma \times \beta$ of two extended metric spaces $\gamma$ and $\beta$ is an extended metric space, where the distance between $(x_1, y_1)$ and $(x_2, y_2)$ is defined as the maximum of the distances $\text{edist}(x_1, x_2)$ and $\text{edist}(y_1, y_2)$. This construction ensures that the induced uniform structure matches the product uniform structure.
EMetric.countable_closure_of_compact theorem
{s : Set γ} (hs : IsCompact s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s = closure t
Full source 
/-- A compact set in an emetric space is separable, i.e., it is the closure of a countable set. -/
theorem countable_closure_of_compact {s : Set γ} (hs : IsCompact s) :
    ∃ t, t ⊆ s ∧ t.Countable ∧ s = closure t := by
  rcases subset_countable_closure_of_compact hs with ⟨t, hts, htc, hsub⟩
  exact ⟨t, hts, htc, hsub.antisymm (closure_minimal hts hs.isClosed)⟩
Compact Sets in Extended Metric Spaces Have Countable Dense Subsets
Informal description
For any compact subset $s$ of an extended metric space $\gamma$, there exists a countable subset $t \subseteq s$ such that $s$ is equal to the closure of $t$.
instEDistSeparationQuotient instance
[PseudoEMetricSpace X] : EDist (SeparationQuotient X)
Full source 
instance [PseudoEMetricSpace X] : EDist (SeparationQuotient X) where
  edist := SeparationQuotient.lift₂ edist fun _ _ _ _ hx hy =>
    edist_congr (EMetric.inseparable_iff.1 hx) (EMetric.inseparable_iff.1 hy)
Extended Distance on Separation Quotient
Informal description
For any pseudo extended metric space $X$, the separation quotient of $X$ is equipped with an extended distance function $\text{edist} : \text{SeparationQuotient}\, X \times \text{SeparationQuotient}\, X \to \mathbb{R}_{\geq 0} \cup \{\infty\}$.
SeparationQuotient.edist_mk theorem
[PseudoEMetricSpace X] (x y : X) : edist (mk x) (mk y) = edist x y
Full source 
@[simp] theorem SeparationQuotient.edist_mk [PseudoEMetricSpace X] (x y : X) :
    edist (mk x) (mk y) = edist x y :=
  rfl
Extended Distance is Preserved by Separation Quotient Projection
Informal description
For any pseudo extended metric space $X$ and any two points $x, y \in X$, the extended distance between their images in the separation quotient of $X$ is equal to the extended distance between $x$ and $y$ in $X$. That is, $\text{edist}(\text{mk}\, x, \text{mk}\, y) = \text{edist}(x, y)$, where $\text{mk} : X \to \text{SeparationQuotient}\, X$ is the canonical projection map.
instEMetricSpaceSeparationQuotient instance
[PseudoEMetricSpace X] : EMetricSpace (SeparationQuotient X)
Full source 
instance [PseudoEMetricSpace X] : EMetricSpace (SeparationQuotient X) :=
  @EMetricSpace.ofT0PseudoEMetricSpace (SeparationQuotient X)
    { edist_self := surjective_mk.forall.2 edist_self,
      edist_comm := surjective_mk.forall₂.2 edist_comm,
      edist_triangle := surjective_mk.forall₃.2 edist_triangle,
      toUniformSpace := inferInstance,
      uniformity_edist := comap_injective (surjective_mk.prodMap surjective_mk) <| by
        simp [comap_mk_uniformity, PseudoEMetricSpace.uniformity_edist] } _
Extended Metric Space Structure on the Separation Quotient of a Pseudo Extended Metric Space
Informal description
For any pseudo extended metric space $X$, the separation quotient $\text{SeparationQuotient}\, X$ is an extended metric space. The extended distance function on the quotient is induced by the extended distance function on $X$, and it satisfies the non-degeneracy condition $\text{edist}(x, y) = 0$ if and only if $x = y$ for all $x, y \in \text{SeparationQuotient}\, X$.
TopologicalSpace.IsSeparable.exists_countable_dense_subset theorem
{s : Set α} (hs : IsSeparable s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t
Full source 
/-- If a set `s` is separable in a (pseudo extended) metric space, then it admits a countable dense
subset. This is not obvious, as the countable set whose closure covers `s` given by the definition
of separability does not need in general to be contained in `s`. -/
theorem IsSeparable.exists_countable_dense_subset
    {s : Set α} (hs : IsSeparable s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t := by
  have : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε := fun ε ε0 => by
    rcases hs with ⟨t, htc, hst⟩
    refine ⟨t, htc, hst.trans fun x hx => ?_⟩
    rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩
    exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩
  exact subset_countable_closure_of_almost_dense_set _ this
Existence of Countable Dense Subset in Separable Sets
Informal description
Let $s$ be a separable subset of a topological space $\alpha$. Then there exists a countable subset $t \subseteq s$ such that $s$ is contained in the closure of $t$.
TopologicalSpace.IsSeparable.separableSpace theorem
{s : Set α} (hs : IsSeparable s) : SeparableSpace s
Full source 
/-- If a set `s` is separable, then the corresponding subtype is separable in a (pseudo extended)
metric space.  This is not obvious, as the countable set whose closure covers `s` does not need in
general to be contained in `s`. -/
theorem IsSeparable.separableSpace {s : Set α} (hs : IsSeparable s) :
    SeparableSpace s := by
  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, hst⟩
  lift t to Set s using hts
  refine ⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩
  rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]
Subspace of a Separable Set is Separable
Informal description
Let $s$ be a separable subset of a topological space $\alpha$. Then the subspace topology on $s$ is separable, i.e., there exists a countable subset of $s$ that is dense in $s$.
lebesgue_number_lemma_of_emetric theorem
{ι : Sort*} {c : ι → Set α} (hs : IsCompact s) (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i, c i) : ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i
Full source 
theorem lebesgue_number_lemma_of_emetric {ι : Sort*} {c : ι → Set α} (hs : IsCompact s)
    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i, c i) : ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i := by
  simpa only [ball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma hs hc₁ hc₂
Lebesgue Number Lemma for Extended Metric Spaces
Informal description
Let $\alpha$ be a pseudo extended metric space, $s$ a compact subset of $\alpha$, and $\{c_i\}_{i \in \iota}$ a family of open sets covering $s$. Then there exists a positive extended real number $\delta > 0$ such that for every point $x \in s$, there exists an index $i$ for which the extended metric ball $B(x, \delta)$ is entirely contained in $c_i$.
lebesgue_number_lemma_of_emetric_nhds' theorem
{c : (x : α) → x ∈ s → Set α} (hs : IsCompact s) (hc : ∀ x hx, c x hx ∈ 𝓝 x) : ∃ δ > 0, ∀ x ∈ s, ∃ y : s, ball x δ ⊆ c y y.2
Full source 
theorem lebesgue_number_lemma_of_emetric_nhds' {c : (x : α) → x ∈ s → Set α} (hs : IsCompact s)
    (hc : ∀ x hx, c x hx ∈ 𝓝 x) : ∃ δ > 0, ∀ x ∈ s, ∃ y : s, ball x δ ⊆ c y y.2 := by
  simpa only [ball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhds' hs hc
Lebesgue Number Lemma for Extended Metric Spaces with Pointwise Neighborhoods
Informal description
Let $\alpha$ be a pseudo extended metric space, $s$ a compact subset of $\alpha$, and for each $x \in s$, let $U_x$ be a neighborhood of $x$ in $\alpha$. Then there exists a positive extended real number $\delta > 0$ such that for every $x \in s$, there exists $y \in s$ with the extended metric ball $B(x, \delta)$ entirely contained in $U_y$.
lebesgue_number_lemma_of_emetric_nhds theorem
{c : α → Set α} (hs : IsCompact s) (hc : ∀ x ∈ s, c x ∈ 𝓝 x) : ∃ δ > 0, ∀ x ∈ s, ∃ y, ball x δ ⊆ c y
Full source 
theorem lebesgue_number_lemma_of_emetric_nhds {c : α → Set α} (hs : IsCompact s)
    (hc : ∀ x ∈ s, c x ∈ 𝓝 x) : ∃ δ > 0, ∀ x ∈ s, ∃ y, ball x δ ⊆ c y := by
  simpa only [ball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhds hs hc
Lebesgue Number Lemma for Extended Metric Spaces with Neighborhoods
Informal description
Let $\alpha$ be a pseudo extended metric space, $s$ a compact subset of $\alpha$, and for each $x \in s$, let $c(x)$ be a neighborhood of $x$. Then there exists a positive extended real number $\delta > 0$ such that for every $x \in s$, there exists a point $y$ for which the extended metric ball $B(x, \delta)$ is entirely contained in $c(y)$.
lebesgue_number_lemma_of_emetric_nhdsWithin' theorem
{c : (x : α) → x ∈ s → Set α} (hs : IsCompact s) (hc : ∀ x hx, c x hx ∈ 𝓝[s] x) : ∃ δ > 0, ∀ x ∈ s, ∃ y : s, ball x δ ∩ s ⊆ c y y.2
Full source 
theorem lebesgue_number_lemma_of_emetric_nhdsWithin' {c : (x : α) → x ∈ s → Set α}
    (hs : IsCompact s) (hc : ∀ x hx, c x hx ∈ 𝓝[s] x) :
    ∃ δ > 0, ∀ x ∈ s, ∃ y : s, ball x δ ∩ s ⊆ c y y.2 := by
  simpa only [ball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhdsWithin' hs hc
Lebesgue Number Lemma for Relative Neighborhoods in Extended Metric Spaces
Informal description
Let $\alpha$ be a pseudo extended metric space and $s$ a compact subset of $\alpha$. For each $x \in s$, let $U_x$ be a neighborhood of $x$ relative to $s$. Then there exists $\delta > 0$ such that for every $x \in s$, there exists $y \in s$ with the intersection of the extended metric ball $B(x, \delta)$ and $s$ contained in $U_y$.
lebesgue_number_lemma_of_emetric_nhdsWithin theorem
{c : α → Set α} (hs : IsCompact s) (hc : ∀ x ∈ s, c x ∈ 𝓝[s] x) : ∃ δ > 0, ∀ x ∈ s, ∃ y, ball x δ ∩ s ⊆ c y
Full source 
theorem lebesgue_number_lemma_of_emetric_nhdsWithin {c : α → Set α} (hs : IsCompact s)
    (hc : ∀ x ∈ s, c x ∈ 𝓝[s] x) : ∃ δ > 0, ∀ x ∈ s, ∃ y, ball x δ ∩ s ⊆ c y := by
  simpa only [ball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhdsWithin hs hc
Lebesgue Number Lemma for Relative Neighborhoods in Compact Extended Metric Spaces
Informal description
Let $\alpha$ be a pseudo extended metric space, $s$ a compact subset of $\alpha$, and for each $x \in s$, let $c(x)$ be a neighborhood of $x$ relative to $s$. Then there exists a positive extended real number $\delta > 0$ such that for every $x \in s$, there exists a point $y$ for which the intersection of the extended metric ball $B(x, \delta)$ with $s$ is entirely contained in $c(y)$.
lebesgue_number_lemma_of_emetric_sUnion theorem
{c : Set (Set α)} (hs : IsCompact s) (hc₁ : ∀ t ∈ c, IsOpen t) (hc₂ : s ⊆ ⋃₀ c) : ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t
Full source 
theorem lebesgue_number_lemma_of_emetric_sUnion {c : Set (Set α)} (hs : IsCompact s)
    (hc₁ : ∀ t ∈ c, IsOpen t) (hc₂ : s ⊆ ⋃₀ c) : ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t := by
  rw [sUnion_eq_iUnion] at hc₂; simpa using lebesgue_number_lemma_of_emetric hs (by simpa) hc₂
Lebesgue Number Lemma for Extended Metric Spaces with Set Union Cover
Informal description
Let $\alpha$ be a pseudo extended metric space, $s$ a compact subset of $\alpha$, and $c$ a family of open sets covering $s$ (i.e., $s \subseteq \bigcup_{t \in c} t$). Then there exists a positive extended real number $\delta > 0$ such that for every point $x \in s$, there exists a set $t \in c$ for which the extended metric ball $B(x, \delta)$ is entirely contained in $t$.