Mathlib.Topology.MetricSpace.Pseudo.Basic

dist_le_Ico_sum_dist theorem

(f : ℕ → α) {m n} (h : m ≤ n) : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))

Full source

/-- The triangle (polygon) inequality for sequences of points; `Finset.Ico` version. -/
theorem dist_le_Ico_sum_dist (f : ℕ → α) {m n} (h : m ≤ n) :
    dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) := by
  induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, dist_self]
  | succ n hle ihn =>
    calc
      dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_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 Finite Sums of Distances in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $f \colon \mathbb{N} \to \alpha$ be a sequence of points in $\alpha$. For any natural numbers $m \leq n$, the distance between $f(m)$ and $f(n)$ is bounded by the sum of the distances between consecutive points in the sequence over the interval $[m, n)$, i.e., \[ \text{dist}(f(m), f(n)) \leq \sum_{i \in [m, n)} \text{dist}(f(i), f(i+1)). \]

dist_le_range_sum_dist theorem

(f : ℕ → α) (n : ℕ) : dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, dist (f i) (f (i + 1))

Full source

/-- The triangle (polygon) inequality for sequences of points; `Finset.range` version. -/
theorem dist_le_range_sum_dist (f : ℕ → α) (n : ℕ) :
    dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, dist (f i) (f (i + 1)) :=
  Nat.Ico_zero_eq_range ▸ dist_le_Ico_sum_dist f (Nat.zero_le n)

Triangle Inequality for Range Sums of Distances in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $f \colon \mathbb{N} \to \alpha$ be a sequence of points in $\alpha$. For any natural number $n$, the distance between $f(0)$ and $f(n)$ is bounded by the sum of the distances between consecutive points in the sequence over the range $\{0, \dots, n-1\}$, i.e., \[ \text{dist}(f(0), f(n)) \leq \sum_{i=0}^{n-1} \text{dist}(f(i), f(i+1)). \]

dist_le_Ico_sum_of_dist_le theorem

 {f : ℕ → α} {m n} (hmn : m ≤ n) {d : ℕ → ℝ} (hd : ∀ {k}, m ≤ k → k < n → dist (f k) (f (k + 1)) ≤ d k) :
  dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i

Full source

/-- A version of `dist_le_Ico_sum_dist` with each intermediate distance replaced
with an upper estimate. -/
theorem dist_le_Ico_sum_of_dist_le {f : ℕ → α} {m n} (hmn : m ≤ n) {d : ℕ → ℝ}
    (hd : ∀ {k}, m ≤ k → k < n → dist (f k) (f (k + 1)) ≤ d k) :
    dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i :=
  le_trans (dist_le_Ico_sum_dist f hmn) <|
    Finset.sum_le_sum fun _k hk => hd (Finset.mem_Ico.1 hk).1 (Finset.mem_Ico.1 hk).2

Generalized Triangle Inequality with Upper Bounds on Intermediate Distances

Informal description

Let $\alpha$ be a pseudometric space and $f \colon \mathbb{N} \to \alpha$ be a sequence of points in $\alpha$. For any natural numbers $m \leq n$ and a sequence of real numbers $d \colon \mathbb{N} \to \mathbb{R}$, if for every $k$ satisfying $m \leq k < n$ we have $\text{dist}(f(k), f(k+1)) \leq d(k)$, then the distance between $f(m)$ and $f(n)$ is bounded by the sum of the $d(i)$ over the interval $[m, n)$, i.e., \[ \text{dist}(f(m), f(n)) \leq \sum_{i \in [m, n)} d(i). \]

dist_le_range_sum_of_dist_le theorem

 {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ} (hd : ∀ {k}, k < n → dist (f k) (f (k + 1)) ≤ d k) :
  dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i

Full source

/-- A version of `dist_le_range_sum_dist` with each intermediate distance replaced
with an upper estimate. -/
theorem dist_le_range_sum_of_dist_le {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ}
    (hd : ∀ {k}, k < n → dist (f k) (f (k + 1)) ≤ d k) :
    dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i :=
  Nat.Ico_zero_eq_range ▸ dist_le_Ico_sum_of_dist_le (zero_le n) fun _ => hd

Triangle Inequality for Range Sums with Upper Bounds on Distances in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $f \colon \mathbb{N} \to \alpha$ be a sequence of points in $\alpha$. For any natural number $n$ and a sequence of real numbers $d \colon \mathbb{N} \to \mathbb{R}$, if for every $k < n$ we have $\text{dist}(f(k), f(k+1)) \leq d(k)$, then the distance between $f(0)$ and $f(n)$ is bounded by the sum of the $d(i)$ over the range $\{0, \dots, n-1\}$, i.e., \[ \text{dist}(f(0), f(n)) \leq \sum_{i=0}^{n-1} d(i). \]

Metric.isUniformInducing_iff theorem

 [PseudoMetricSpace β] {f : α → β} :
  IsUniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Full source

nonrec theorem isUniformInducing_iff [PseudoMetricSpace β] {f : α → β} :
    IsUniformInducingIsUniformInducing f ↔ UniformContinuous f ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ :=
  isUniformInducing_iff'.trans <| Iff.rfl.and <|
    ((uniformity_basis_dist.comap _).le_basis_iff uniformity_basis_dist).trans <| by
      simp only [subset_def, Prod.forall, gt_iff_lt, preimage_setOf_eq, Prod.map_apply, mem_setOf]

Characterization of Uniform Inducing Maps in Pseudometric Spaces via Uniform Continuity and Distance Control

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces. A function $f \colon \alpha \to \beta$ is uniform inducing 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 $\text{dist}(f(a), f(b)) < \varepsilon$, then $\text{dist}(a, b) < \delta$.

Metric.isUniformEmbedding_iff theorem

 [PseudoMetricSpace β] {f : α → β} :
  IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Full source

nonrec theorem isUniformEmbedding_iff [PseudoMetricSpace β] {f : α → β} :
    IsUniformEmbeddingIsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ := by
  rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff]

Characterization of Uniform Embeddings in Pseudometric Spaces via Injectivity, Uniform Continuity, and Distance Control

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces. A function $f \colon \alpha \to \beta$ 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{dist}(f(a), f(b)) < \varepsilon$, then $\text{dist}(a, b) < \delta$.

Metric.controlled_of_isUniformEmbedding theorem

 [PseudoMetricSpace β] {f : α → β} (h : IsUniformEmbedding f) :
  (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Full source

/-- If a map between pseudometric spaces is a uniform embedding then the distance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y`. -/
theorem controlled_of_isUniformEmbedding [PseudoMetricSpace β] {f : α → β}
    (h : IsUniformEmbedding f) :
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ :=
  ⟨uniformContinuous_iff.1 h.uniformContinuous, (isUniformEmbedding_iff.1 h).2.2⟩

Distance Control for Uniform Embeddings in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric 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{dist}(a, b) < \delta$, then $\text{dist}(f(a), f(b)) < \varepsilon$. 2. For every $\delta > 0$, there exists $\varepsilon > 0$ such that for all $a, b \in \alpha$, if $\text{dist}(f(a), f(b)) < \varepsilon$, then $\text{dist}(a, b) < \delta$.

Metric.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 ε :=
  uniformity_basis_dist.totallyBounded_iff

Characterization of Totally Bounded Sets in Pseudometric Spaces via $\varepsilon$-Coverings

Informal description

A subset $s$ of a pseudometric space $\alpha$ is totally bounded if and only if for every $\varepsilon > 0$, there exists a finite subset $t \subseteq \alpha$ such that $s$ is covered by the union of open balls of radius $\varepsilon$ centered at each point in $t$, i.e., $$ s \subseteq \bigcup_{y \in t} B(y, \varepsilon). $$

Metric.totallyBounded_of_finite_discretization theorem

 {s : Set α} (H : ∀ ε > (0 : ℝ), ∃ (β : Type u) (_ : Fintype β) (F : s → β), ∀ x y, F x = F y → dist (x : α) y < ε) :
  TotallyBounded s

Full source

/-- A pseudometric space is totally bounded if one can reconstruct up to any ε>0 any element of the
space from finitely many data. -/
theorem totallyBounded_of_finite_discretization {s : Set α}
    (H : ∀ ε > (0 : ℝ),
        ∃ (β : Type u) (_ : Fintype β) (F : s → β), ∀ x y, F x = F y → dist (x : α) y < ε) :
    TotallyBounded s := by
  rcases s.eq_empty_or_nonempty with hs | hs
  · rw [hs]
    exact totallyBounded_empty
  rcases hs with ⟨x0, hx0⟩
  haveI : Inhabited s := ⟨⟨x0, hx0⟩⟩
  refine totallyBounded_iff.2 fun ε ε0 => ?_
  rcases H ε ε0 with ⟨β, fβ, F, hF⟩
  let Finv := Function.invFun F
  refine ⟨range (Subtype.val ∘ Finv), finite_range _, fun x xs => ?_⟩
  let x' := Finv (F ⟨x, xs⟩)
  have : F x' = F ⟨x, xs⟩ := Function.invFun_eq ⟨⟨x, xs⟩, rfl⟩
  simp only [Set.mem_iUnion, Set.mem_range]
  exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩

Total Boundedness via Finite Discretization in Pseudometric Spaces

Informal description

A subset $s$ of a pseudometric space $\alpha$ is totally bounded if for every $\varepsilon > 0$, there exists a finite type $\beta$ and a function $F \colon s \to \beta$ such that for any $x, y \in s$, if $F(x) = F(y)$ then the distance between $x$ and $y$ is less than $\varepsilon$.

Metric.finite_approx_of_totallyBounded theorem

{s : Set α} (hs : TotallyBounded s) : ∀ ε > 0, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y ε

Full source

theorem finite_approx_of_totallyBounded {s : Set α} (hs : TotallyBounded s) :
    ∀ ε > 0, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y ε := by
  intro ε ε_pos
  rw [totallyBounded_iff_subset] at hs
  exact hs _ (dist_mem_uniformity ε_pos)

Finite $\varepsilon$-Covering of Totally Bounded Sets in Pseudometric Spaces

Informal description

For any totally bounded subset $s$ of a pseudometric space $\alpha$ and for every $\varepsilon > 0$, there exists a finite subset $t \subseteq s$ such that $s$ is covered by the union of open balls of radius $\varepsilon$ centered at each point in $t$, i.e., $$ s \subseteq \bigcup_{y \in t} B(y, \varepsilon). $$

Metric.tendstoUniformlyOnFilter_iff theorem

 {F : ι → β → α} {f : β → α} {p : Filter ι} {p' : Filter β} :
  TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ n : ι × β in p ×ˢ p', dist (f n.snd) (F n.fst n.snd) < ε

Full source

/-- Expressing uniform convergence using `dist` -/
theorem tendstoUniformlyOnFilter_iff {F : ι → β → α} {f : β → α} {p : Filter ι} {p' : Filter β} :
    TendstoUniformlyOnFilterTendstoUniformlyOnFilter F f p p' ↔
      ∀ ε > 0, ∀ᶠ n : ι × β in p ×ˢ p', dist (f n.snd) (F n.fst n.snd) < ε := by
  refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩
  rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩
  exact (H ε εpos).mono fun n hn => hε hn

Characterization of Uniform Convergence on Filter via Distance in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $\beta$ a type, and $F_n : \beta \to \alpha$ a family of functions indexed by $n \in \iota$ converging to a function $f : \beta \to \alpha$ with respect to filters $p$ on $\iota$ and $p'$ on $\beta$. The family $F_n$ converges uniformly to $f$ on the filter $p'$ if and only if for every $\varepsilon > 0$, the set of pairs $(n, x) \in \iota \times \beta$ such that $\text{dist}(f(x), F_n(x)) < \varepsilon$ is eventually in the product filter $p \times p'$.

Metric.tendstoLocallyUniformlyOn_iff theorem

 [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} :
  TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Full source

/-- Expressing locally uniform convergence on a set using `dist`. -/
theorem tendstoLocallyUniformlyOn_iff [TopologicalSpace β] {F : ι → β → α} {f : β → α}
    {p : Filter ι} {s : Set β} :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p s ↔
      ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε := by
  refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu x hx => ?_⟩
  rcases mem_uniformity_dist.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 Distance in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $\beta$ a topological space. A family of functions $F_n \colon \beta \to \alpha$ indexed by $\iota$ converges locally uniformly on a set $s \subseteq \beta$ to a function $f \colon \beta \to \alpha$ with respect to a filter $p$ on $\iota$ if and only if for every $\varepsilon > 0$ and every point $x \in s$, there exists a neighborhood $t$ of $x$ in $s$ such that for all $n$ eventually in $p$, the distance $\text{dist}(f(y), F_n(y)) < \varepsilon$ holds for all $y \in t$.

Metric.tendstoUniformlyOn_iff theorem

 {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} :
  TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, dist (f x) (F n x) < ε

Full source

/-- Expressing uniform convergence on a set using `dist`. -/
theorem tendstoUniformlyOn_iff {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} :
    TendstoUniformlyOnTendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, dist (f x) (F n x) < ε := by
  refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩
  rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩
  exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)

Characterization of Uniform Convergence on a Set via Distance in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $\beta$ a type, $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$ a set. The sequence $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 distance $\text{dist}(f(x), F_n(x)) < \varepsilon$.

Metric.tendstoLocallyUniformly_iff theorem

 [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} :
  TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ x : β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Full source

/-- Expressing locally uniform convergence using `dist`. -/
theorem tendstoLocallyUniformly_iff [TopologicalSpace β] {F : ι → β → α} {f : β → α}
    {p : Filter ι} :
    TendstoLocallyUniformlyTendstoLocallyUniformly F f p ↔
      ∀ ε > 0, ∀ x : β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε := by
  simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, nhdsWithin_univ,
    mem_univ, forall_const, exists_prop]

Characterization of Locally Uniform Convergence via Distance in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $\beta$ 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 $\epsilon > 0$ and every point $x \in \beta$, there exists a neighborhood $t$ of $x$ such that for all $n$ eventually in $p$, the distance between $f(y)$ and $F_n(y)$ is less than $\epsilon$ for all $y \in t$.

Metric.tendstoUniformly_iff theorem

 {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, dist (f x) (F n x) < ε

Full source

/-- Expressing uniform convergence using `dist`. -/
theorem tendstoUniformly_iff {F : ι → β → α} {f : β → α} {p : Filter ι} :
    TendstoUniformlyTendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, dist (f x) (F n x) < ε := by
  rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff]
  simp

Characterization of Uniform Convergence via Distance in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $\beta$ a type, $F_n \colon \beta \to \alpha$ a sequence of functions, $f \colon \beta \to \alpha$ a function, and $p$ a filter on the index set $\iota$. The sequence $F_n$ converges uniformly to $f$ 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 \beta$, the distance $\text{dist}(f(x), F_n(x)) < \varepsilon$.

Metric.cauchy_iff theorem

{f : Filter α} : Cauchy f ↔ NeBot f ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε

Full source

protected theorem cauchy_iff {f : Filter α} :
    CauchyCauchy f ↔ NeBot f ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε :=
  uniformity_basis_dist.cauchy_iff

Characterization of Cauchy Filters in Pseudometric Spaces

Informal description

A filter $f$ on a pseudometric space $\alpha$ is Cauchy if and only if it is non-trivial (i.e., does not contain the empty set) and for every $\varepsilon > 0$, there exists a set $t \in f$ such that for all $x, y \in t$, the distance between $x$ and $y$ is less than $\varepsilon$.

Metric.exists_ball_inter_eq_singleton_of_mem_discrete theorem

[DiscreteTopology s] {x : α} (hx : x ∈ s) : ∃ ε > 0, Metric.ball x ε ∩ s = { x }

Full source

/-- Given a point `x` in a discrete subset `s` of a pseudometric space, there is an open ball
centered at `x` and intersecting `s` only at `x`. -/
theorem exists_ball_inter_eq_singleton_of_mem_discrete [DiscreteTopology s] {x : α} (hx : x ∈ s) :
    ∃ ε > 0, Metric.ball x ε ∩ s = {x} :=
  nhds_basis_ball.exists_inter_eq_singleton_of_mem_discrete hx

Existence of Isolating Ball for Points in Discrete Subsets of Pseudometric Spaces

Informal description

Let $s$ be a discrete subset of a pseudometric space $\alpha$ and let $x \in s$. Then there exists $\varepsilon > 0$ such that the open ball $B(x, \varepsilon)$ centered at $x$ with radius $\varepsilon$ satisfies $B(x, \varepsilon) \cap s = \{x\}$.

Metric.exists_closedBall_inter_eq_singleton_of_discrete theorem

[DiscreteTopology s] {x : α} (hx : x ∈ s) : ∃ ε > 0, Metric.closedBall x ε ∩ s = { x }

Full source

/-- Given a point `x` in a discrete subset `s` of a pseudometric space, there is a closed ball
of positive radius centered at `x` and intersecting `s` only at `x`. -/
theorem exists_closedBall_inter_eq_singleton_of_discrete [DiscreteTopology s] {x : α} (hx : x ∈ s) :
    ∃ ε > 0, Metric.closedBall x ε ∩ s = {x} :=
  nhds_basis_closedBall.exists_inter_eq_singleton_of_mem_discrete hx

Existence of Isolating Closed Ball for Points in Discrete Subsets of Pseudometric Spaces

Informal description

Let $s$ be a subset of a pseudometric space $\alpha$ equipped with the discrete topology, and let $x \in s$. Then there exists a positive real number $\varepsilon > 0$ such that the intersection of the closed ball $\overline{B}(x, \varepsilon)$ with $s$ is exactly the singleton set $\{x\}$.

Metric.inseparable_iff_nndist theorem

{x y : α} : Inseparable x y ↔ nndist x y = 0

Full source

theorem Metric.inseparable_iff_nndist {x y : α} : InseparableInseparable x y ↔ nndist x y = 0 := by
  rw [EMetric.inseparable_iff, edist_nndist, ENNReal.coe_eq_zero]

Topological Inseparability Characterized by Non-negative Distance in Pseudometric Spaces

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the points are topologically inseparable if and only if their non-negative distance is zero, i.e., $\text{nndist}(x, y) = 0$.

Metric.inseparable_iff theorem

{x y : α} : Inseparable x y ↔ dist x y = 0

Full source

theorem Metric.inseparable_iff {x y : α} : InseparableInseparable x y ↔ dist x y = 0 := by
  rw [Metric.inseparable_iff_nndist, dist_nndist, NNReal.coe_eq_zero]

Topological Inseparability Characterized by Distance in Pseudometric Spaces

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the points are topologically inseparable if and only if their distance is zero, i.e., $\text{dist}(x, y) = 0$.

tendsto_nhds_unique_dist theorem

 {f : β → α} {l : Filter β} {x y : α} [NeBot l] (ha : Tendsto f l (𝓝 x)) (hb : Tendsto f l (𝓝 y)) : dist x y = 0

Full source

/-- A weaker version of `tendsto_nhds_unique` for `PseudoMetricSpace`. -/
theorem tendsto_nhds_unique_dist {f : β → α} {l : Filter β} {x y : α} [NeBot l]
    (ha : Tendsto f l (𝓝 x)) (hb : Tendsto f l (𝓝 y)) : dist x y = 0 :=
  (tendsto_nhds_unique_inseparable ha hb).dist_eq_zero

Uniqueness of Limits in Pseudometric Spaces up to Zero Distance

Informal description

Let $\alpha$ be a pseudometric space, $\beta$ a topological space, and $f: \beta \to \alpha$ a function. For any filter $l$ on $\beta$ that is not the trivial filter, if $f$ tends to both $x$ and $y$ in $\alpha$ along $l$, then the distance between $x$ and $y$ is zero, i.e., $\text{dist}(x, y) = 0$.

cauchySeq_iff_tendsto_dist_atTop_0 theorem

 [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ Tendsto (fun n : β × β => dist (u n.1) (u n.2)) atTop (𝓝 0)

Full source

theorem cauchySeq_iff_tendsto_dist_atTop_0 [Nonempty β] [SemilatticeSup β] {u : β → α} :
    CauchySeqCauchySeq u ↔ Tendsto (fun n : β × β => dist (u n.1) (u n.2)) atTop (𝓝 0) := by
  rw [cauchySeq_iff_tendsto, Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff,
    Function.comp_def]
  simp_rw [Prod.map_fst, Prod.map_snd]

Characterization of Cauchy Sequences via Distance Convergence to Zero

Informal description

Let $\beta$ be a nonempty directed set (join-semilattice) and $\alpha$ a pseudometric space. A sequence $u \colon \beta \to \alpha$ is Cauchy if and only if the function $(x, y) \mapsto \text{dist}(u(x), u(y))$ tends to $0$ as $x$ and $y$ tend to infinity in $\beta$.

Topology.IsInducing.isSeparable_preimage theorem

{f : β → α} [TopologicalSpace β] (hf : IsInducing f) {s : Set α} (hs : IsSeparable s) : IsSeparable (f ⁻¹' s)

Full source

/-- The preimage of a separable set by an inducing map is separable. -/
protected lemma IsInducing.isSeparable_preimage {f : β → α} [TopologicalSpace β]
    (hf : IsInducing f) {s : Set α} (hs : IsSeparable s) : IsSeparable (f ⁻¹' s) := by
  have : SeparableSpace s := hs.separableSpace
  have : SecondCountableTopology s := UniformSpace.secondCountable_of_separable _
  have : IsInducing ((mapsTo_preimage f s).restrict _ _ _) :=
    (hf.comp IsInducing.subtypeVal).codRestrict _
  have := this.secondCountableTopology
  exact .of_subtype _

Preimage of a Separable Set under an Inducing Map is Separable

Informal description

Let $f \colon \beta \to \alpha$ be an inducing map between topological spaces. If a subset $s \subseteq \alpha$ is separable, then its preimage $f^{-1}(s) \subseteq \beta$ is also separable.

Topology.IsEmbedding.isSeparable_preimage theorem

{f : β → α} [TopologicalSpace β] (hf : IsEmbedding f) {s : Set α} (hs : IsSeparable s) : IsSeparable (f ⁻¹' s)

Full source

protected theorem IsEmbedding.isSeparable_preimage {f : β → α} [TopologicalSpace β]
    (hf : IsEmbedding f) {s : Set α} (hs : IsSeparable s) : IsSeparable (f ⁻¹' s) :=
  hf.isInducing.isSeparable_preimage hs

Preimage of a Separable Set under an Embedding is Separable

Informal description

Let $f \colon \beta \to \alpha$ be an embedding between topological spaces. If a subset $s \subseteq \alpha$ is separable, then its preimage $f^{-1}(s) \subseteq \beta$ is also separable.

IsCompact.isSeparable theorem

{s : Set α} (hs : IsCompact s) : IsSeparable s

Full source

/-- A compact set is separable. -/
theorem IsCompact.isSeparable {s : Set α} (hs : IsCompact s) : IsSeparable s :=
  haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
  .of_subtype s

Compact subsets of pseudometric spaces are separable

Informal description

For any compact subset $s$ of a pseudometric space $\alpha$, the set $s$ is separable. That is, there exists a countable subset $c \subseteq \alpha$ such that $s$ is contained in the closure of $c$.

Metric.secondCountable_of_almost_dense_set theorem

 (H : ∀ ε > (0 : ℝ), ∃ s : Set α, s.Countable ∧ ∀ x, ∃ y ∈ s, dist x y ≤ ε) : SecondCountableTopology α

Full source

/-- A pseudometric space is second countable if, for every `ε > 0`, there is a countable set which
is `ε`-dense. -/
theorem secondCountable_of_almost_dense_set
    (H : ∀ ε > (0 : ℝ), ∃ s : Set α, s.Countable ∧ ∀ x, ∃ y ∈ s, dist x y ≤ ε) :
    SecondCountableTopology α := by
  refine EMetric.secondCountable_of_almost_dense_set fun ε ε0 => ?_
  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 ε0 with ⟨ε', ε'0, ε'ε⟩
  choose s hsc y hys hyx using H ε' (mod_cast ε'0)
  refine ⟨s, hsc, iUnion₂_eq_univ_iff.2 fun x => ⟨y x, hys _, le_trans ?_ ε'ε.le⟩⟩
  exact mod_cast hyx x

Second-Countability Criterion for Pseudometric Spaces via $\varepsilon$-Dense Sets

Informal description

A pseudometric space $\alpha$ is second-countable if for every $\varepsilon > 0$, there exists a countable subset $s \subseteq \alpha$ such that for every point $x \in \alpha$, there exists $y \in s$ with $\text{dist}(x, y) \leq \varepsilon$.

finite_cover_balls_of_compact theorem

(hs : IsCompact s) {e : ℝ} (he : 0 < e) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x e

Full source

/-- Any compact set in a pseudometric space can be covered by finitely many balls of a given
positive radius -/
theorem finite_cover_balls_of_compact (hs : IsCompact s) {e : ℝ} (he : 0 < e) :
    ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x e :=
  let ⟨t, hts, ht⟩ := hs.elim_nhds_subcover _ (fun x _ => ball_mem_nhds x he)
  ⟨t, hts, t.finite_toSet, ht⟩

Finite Covering of Compact Sets by Balls in Pseudometric Spaces

Informal description

For any compact subset $s$ of a pseudometric space $\alpha$ and any positive real number $\varepsilon > 0$, there exists a finite subset $t \subseteq s$ such that $s$ is covered by the union of open balls $\bigcup_{x \in t} \text{ball}(x, \varepsilon)$ centered at points of $t$ with radius $\varepsilon$.

exists_finite_cover_balls_of_isCompact_closure theorem

(hs : IsCompact (closure s)) (hε : 0 < ε) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε

Full source

/-- Any relatively compact set in a pseudometric space can be covered by finitely many balls of a
given positive radius. -/
lemma exists_finite_cover_balls_of_isCompact_closure (hs : IsCompact (closure s)) (hε : 0 < ε) :
    ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε := by
  obtain ⟨t, hst⟩ := hs.elim_finite_subcover (fun x : s ↦ ball x ε) (fun _ ↦ isOpen_ball) fun x hx ↦
    let ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ hε; mem_iUnion.2 ⟨⟨y, hy⟩, hxy⟩
  refine ⟨t.map ⟨Subtype.val, Subtype.val_injective⟩, by simp, Finset.finite_toSet _, ?_⟩
  simpa using subset_closure.trans hst

Finite $\varepsilon$-ball covering for sets with compact closure in pseudometric spaces

Informal description

Let $\alpha$ be a pseudometric space and $s \subseteq \alpha$ a subset with compact closure. For any $\varepsilon > 0$, there exists a finite subset $t \subseteq s$ such that $s$ is covered by the union of open balls $\bigcup_{x \in t} B(x, \varepsilon)$ of radius $\varepsilon$ centered at points in $t$.

ContinuousOn.isSeparable_image theorem

[TopologicalSpace β] {f : α → β} {s : Set α} (hf : ContinuousOn f s) (hs : IsSeparable s) : IsSeparable (f '' s)

Full source

/-- If a map is continuous on a separable set `s`, then the image of `s` is also separable. -/
theorem ContinuousOn.isSeparable_image [TopologicalSpace β] {f : α → β} {s : Set α}
    (hf : ContinuousOn f s) (hs : IsSeparable s) : IsSeparable (f '' s) := by
  rw [image_eq_range, ← image_univ]
  exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.restrict

Continuous Image of Separable Set is Separable

Informal description

Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a separable subset, and $f \colon X \to Y$ a continuous function on $s$. Then the image $f(s) \subseteq Y$ is separable.