Mathlib.Topology.UniformSpace.Cauchy

Cauchy definition

(f : Filter α)

Full source

/-- A filter `f` is Cauchy if for every entourage `r`, there exists an
  `s ∈ f` such that `s × s ⊆ r`. This is a generalization of Cauchy
  sequences, because if `a : ℕ → α` then the filter of sets containing
  cofinitely many of the `a n` is Cauchy iff `a` is a Cauchy sequence. -/
def Cauchy (f : Filter α) :=
  NeBotNeBot f ∧ f ×ˢ f ≤ 𝓤 α

Cauchy filter

Informal description

A filter `f` on a uniform space `α` is called *Cauchy* if it is non-trivial (i.e., does not contain the empty set) and for every entourage `r` in the uniformity of `α`, there exists a set `s ∈ f` such that `s × s ⊆ r`. This generalizes the notion of Cauchy sequences to filters, where a sequence is Cauchy if and only if the corresponding filter of cofinite sets is Cauchy.

IsComplete definition

(s : Set α)

Full source

/-- A set `s` is called *complete*, if any Cauchy filter `f` such that `s ∈ f`
has a limit in `s` (formally, it satisfies `f ≤ 𝓝 x` for some `x ∈ s`). -/
def IsComplete (s : Set α) :=
  ∀ f, Cauchy f → f ≤ 𝓟 s → ∃ x ∈ s, f ≤ 𝓝 x

Complete subset of a uniform space

Informal description

A subset $s$ of a uniform space $\alpha$ is called *complete* if every Cauchy filter $f$ on $\alpha$ that contains $s$ converges to some point $x \in s$ (i.e., $f$ is finer than the neighborhood filter of $x$).

Filter.HasBasis.cauchy_iff theorem

 {ι} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) {f : Filter α} :
  Cauchy f ↔ NeBot f ∧ ∀ i, p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i

Full source

theorem Filter.HasBasis.cauchy_iff {ι} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s)
    {f : Filter α} :
    CauchyCauchy f ↔ NeBot f ∧ ∀ i, p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i :=
  and_congr Iff.rfl <|
    (f.basis_sets.prod_self.le_basis_iff h).trans <| by
      simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]

Characterization of Cauchy Filters via Uniformity Basis

Informal description

Let $\alpha$ be a uniform space with a basis $\{s_i\}_{i \in \iota}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p : \iota \to \mathrm{Prop}$. A filter $f$ on $\alpha$ is Cauchy if and only if it is non-trivial (i.e., $\mathrm{NeBot}\, f$) and for every index $i$ satisfying $p(i)$, there exists a set $t \in f$ such that for all $x, y \in t$, the pair $(x, y)$ belongs to $s_i$.

cauchy_iff' theorem

{f : Filter α} : Cauchy f ↔ NeBot f ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s

Full source

theorem cauchy_iff' {f : Filter α} :
    CauchyCauchy f ↔ NeBot f ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s :=
  (𝓤 α).basis_sets.cauchy_iff

Characterization of Cauchy filters via entourages

Informal description

A filter $f$ on a uniform space $\alpha$ is Cauchy if and only if it is non-trivial (i.e., $f$ does not contain the empty set) and for every entourage $s$ in the uniformity $\mathfrak{U}(\alpha)$, there exists a set $t \in f$ such that for all $x, y \in t$, the pair $(x, y)$ belongs to $s$.

cauchy_iff theorem

{f : Filter α} : Cauchy f ↔ NeBot f ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s

Full source

theorem cauchy_iff {f : Filter α} : CauchyCauchy f ↔ NeBot f ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s :=
  cauchy_iff'.trans <| by
    simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]

Characterization of Cauchy Filters via Cartesian Products of Sets

Informal description

A filter $f$ on a uniform space $\alpha$ is Cauchy if and only if it is non-trivial (i.e., $f$ does not contain the empty set) and for every entourage $s$ in the uniformity $\mathfrak{U}(\alpha)$, there exists a set $t \in f$ such that the Cartesian product $t \times t$ is contained in $s$.

cauchy_iff_le theorem

{l : Filter α} [hl : l.NeBot] : Cauchy l ↔ l ×ˢ l ≤ 𝓤 α

Full source

lemma cauchy_iff_le {l : Filter α} [hl : l.NeBot] :
    CauchyCauchy l ↔ l ×ˢ l ≤ 𝓤 α := by
  simp only [Cauchy, hl, true_and]

Characterization of Cauchy Filters via Uniformity

Informal description

A non-trivial filter $l$ on a uniform space $\alpha$ is Cauchy if and only if the product filter $l \times l$ is contained in the uniformity filter $\mathfrak{U}(\alpha)$ of the space.

Cauchy.ultrafilter_of theorem

{l : Filter α} (h : Cauchy l) : Cauchy (@Ultrafilter.of _ l h.1 : Filter α)

Full source

theorem Cauchy.ultrafilter_of {l : Filter α} (h : Cauchy l) :
    Cauchy (@Ultrafilter.of _ l h.1 : Filter α) := by
  haveI := h.1
  have := Ultrafilter.of_le l
  exact ⟨Ultrafilter.neBot _, (Filter.prod_mono this this).trans h.2⟩

Ultrafilter Generated from Cauchy Filter is Cauchy

Informal description

For any Cauchy filter $l$ on a uniform space $\alpha$, the ultrafilter generated from $l$ (via the `Ultrafilter.of` construction) is also Cauchy.

cauchy_map_iff theorem

 {l : Filter β} {f : β → α} : Cauchy (l.map f) ↔ NeBot l ∧ Tendsto (fun p : β × β => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Full source

theorem cauchy_map_iff {l : Filter β} {f : β → α} :
    CauchyCauchy (l.map f) ↔ NeBot l ∧ Tendsto (fun p : β × β => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α) := by
  rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]

Characterization of Cauchy Image Filter via Uniform Convergence

Informal description

For any filter $l$ on a type $\beta$ and any function $f : \beta \to \alpha$ to a uniform space $\alpha$, the image filter $l.map f$ is Cauchy if and only if $l$ is non-trivial and the map $(p_1, p_2) \mapsto (f(p_1), f(p_2))$ tends to the uniformity $\mathfrak{U}(\alpha)$ along the product filter $l \times l$.

cauchy_map_iff' theorem

 {l : Filter β} [hl : NeBot l] {f : β → α} : Cauchy (l.map f) ↔ Tendsto (fun p : β × β => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Full source

theorem cauchy_map_iff' {l : Filter β} [hl : NeBot l] {f : β → α} :
    CauchyCauchy (l.map f) ↔ Tendsto (fun p : β × β => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α) :=
  cauchy_map_iff.trans <| and_iff_right hl

Cauchy Image Filter Characterization for Non-Trivial Filters

Informal description

Let $l$ be a non-trivial filter on a type $\beta$ and $f : \beta \to \alpha$ a function to a uniform space $\alpha$. Then the image filter $l.map f$ is Cauchy if and only if the map $(p_1, p_2) \mapsto (f(p_1), f(p_2))$ tends to the uniformity $\mathfrak{U}(\alpha)$ along the product filter $l \times l$.

Cauchy.mono theorem

{f g : Filter α} [hg : NeBot g] (h_c : Cauchy f) (h_le : g ≤ f) : Cauchy g

Full source

theorem Cauchy.mono {f g : Filter α} [hg : NeBot g] (h_c : Cauchy f) (h_le : g ≤ f) : Cauchy g :=
  ⟨hg, le_trans (Filter.prod_mono h_le h_le) h_c.right⟩

Cauchy Filter Monotonicity

Informal description

Let $f$ and $g$ be filters on a uniform space $\alpha$ such that $g$ is non-trivial and $g \leq f$. If $f$ is a Cauchy filter, then $g$ is also a Cauchy filter.

Cauchy.mono' theorem

{f g : Filter α} (h_c : Cauchy f) (_ : NeBot g) (h_le : g ≤ f) : Cauchy g

Full source

theorem Cauchy.mono' {f g : Filter α} (h_c : Cauchy f) (_ : NeBot g) (h_le : g ≤ f) : Cauchy g :=
  h_c.mono h_le

Cauchy Filter Monotonicity (Primed Version)

Informal description

Let $f$ and $g$ be filters on a uniform space $\alpha$ such that $g$ is non-trivial and $g \leq f$. If $f$ is a Cauchy filter, then $g$ is also a Cauchy filter.

cauchy_nhds theorem

{a : α} : Cauchy (𝓝 a)

Full source

theorem cauchy_nhds {a : α} : Cauchy (𝓝 a) :=
  ⟨nhds_neBot, nhds_prod_eq.symm.trans_le (nhds_le_uniformity a)⟩

Neighborhood Filter is Cauchy in Uniform Spaces

Informal description

For any point $a$ in a uniform space $\alpha$, the neighborhood filter $\mathcal{N}(a)$ is a Cauchy filter.

cauchy_pure theorem

{a : α} : Cauchy (pure a)

Full source

theorem cauchy_pure {a : α} : Cauchy (pure a) :=
  cauchy_nhds.mono (pure_le_nhds a)

Principal Filter is Cauchy in Uniform Spaces

Informal description

For any point $a$ in a uniform space $\alpha$, the principal filter $\{a\}$ is a Cauchy filter.

Filter.Tendsto.cauchy_map theorem

{l : Filter β} [NeBot l] {f : β → α} {a : α} (h : Tendsto f l (𝓝 a)) : Cauchy (map f l)

Full source

theorem Filter.Tendsto.cauchy_map {l : Filter β} [NeBot l] {f : β → α} {a : α}
    (h : Tendsto f l (𝓝 a)) : Cauchy (map f l) :=
  cauchy_nhds.mono h

Cauchy Property of the Image Filter Under Convergence

Informal description

Let $l$ be a non-trivial filter on a type $\beta$, and let $f : \beta \to \alpha$ be a function mapping into a uniform space $\alpha$. If $f$ tends to a point $a \in \alpha$ along $l$, then the image filter $\text{map } f \ l$ is a Cauchy filter on $\alpha$.

Cauchy.mono_uniformSpace theorem

 {u v : UniformSpace β} {F : Filter β} (huv : u ≤ v) (hF : Cauchy (uniformSpace := u) F) : Cauchy (uniformSpace := v) F

Full source

lemma Cauchy.mono_uniformSpace {u v : UniformSpace β} {F : Filter β} (huv : u ≤ v)
    (hF : Cauchy (uniformSpace := u) F) : Cauchy (uniformSpace := v) F :=
  ⟨hF.1, hF.2.trans huv⟩

Cauchy Filter Preservation Under Coarser Uniformity

Informal description

Let $u$ and $v$ be two uniform space structures on a type $\beta$ such that $u \leq v$ (i.e., the uniformity of $u$ is finer than that of $v$). If a filter $F$ on $\beta$ is Cauchy with respect to $u$, then it is also Cauchy with respect to $v$.

cauchy_inf_uniformSpace theorem

 {u v : UniformSpace β} {F : Filter β} :
  Cauchy (uniformSpace := u ⊓ v) F ↔ Cauchy (uniformSpace := u) F ∧ Cauchy (uniformSpace := v) F

Full source

lemma cauchy_inf_uniformSpace {u v : UniformSpace β} {F : Filter β} :
    CauchyCauchy (uniformSpace := u ⊓ v) F ↔
    Cauchy (uniformSpace := u) F ∧ Cauchy (uniformSpace := v) F := by
  unfold Cauchy
  rw [inf_uniformity (u := u), le_inf_iff, and_and_left]

Cauchy Criterion for Infimum of Uniform Spaces

Informal description

For any two uniform space structures $u$ and $v$ on a type $\beta$, and any filter $F$ on $\beta$, the filter $F$ is Cauchy with respect to the infimum uniform space $u \sqcap v$ if and only if $F$ is Cauchy with respect to both $u$ and $v$ individually.

cauchy_iInf_uniformSpace theorem

 {ι : Sort*} [Nonempty ι] {u : ι → UniformSpace β} {l : Filter β} :
  Cauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l

Full source

lemma cauchy_iInf_uniformSpace {ι : Sort*} [Nonempty ι] {u : ι → UniformSpace β}
    {l : Filter β} :
    CauchyCauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l := by
  unfold Cauchy
  rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]

Cauchy Criterion for Infimum of Uniform Spaces: $l$ is Cauchy in $\bigsqcap_i u_i$ iff $l$ is Cauchy in each $u_i$

Informal description

Let $\beta$ be a type equipped with a nonempty family of uniform space structures $(u_i)_{i \in \iota}$. A filter $l$ on $\beta$ is Cauchy with respect to the infimum uniform space $\bigsqcap_i u_i$ if and only if $l$ is Cauchy with respect to each uniform space $u_i$ individually.

cauchy_iInf_uniformSpace' theorem

 {ι : Sort*} {u : ι → UniformSpace β} {l : Filter β} [l.NeBot] :
  Cauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l

Full source

lemma cauchy_iInf_uniformSpace' {ι : Sort*} {u : ι → UniformSpace β}
    {l : Filter β} [l.NeBot] :
    CauchyCauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l := by
  simp_rw [cauchy_iff_le (uniformSpace := _), iInf_uniformity, le_iInf_iff]

Cauchy Criterion for Infimum Uniform Space: $l$ is Cauchy in $\bigsqcap_i u_i$ iff $l$ is Cauchy in each $u_i$

Informal description

Let $\beta$ be a type, $\iota$ be a non-empty index type, and $(u_i)_{i \in \iota}$ be a family of uniform space structures on $\beta$. For a non-trivial filter $l$ on $\beta$, $l$ is Cauchy with respect to the infimum uniform space $\bigsqcap_{i \in \iota} u_i$ if and only if $l$ is Cauchy with respect to each uniform space $u_i$ for all $i \in \iota$.

cauchy_comap_uniformSpace theorem

{u : UniformSpace β} {α} {f : α → β} {l : Filter α} : Cauchy (uniformSpace := comap f u) l ↔ Cauchy (map f l)

Full source

lemma cauchy_comap_uniformSpace {u : UniformSpace β} {α} {f : α → β} {l : Filter α} :
    CauchyCauchy (uniformSpace := comap f u) l ↔ Cauchy (map f l) := by
  simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap]
  rfl

Cauchy Criterion for Pullback Uniform Spaces: $l$ is Cauchy in $\alpha$ iff $f(l)$ is Cauchy in $\beta$

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a uniform space structure, and let $f \colon \alpha \to \beta$ be a function. For any filter $l$ on $\alpha$, the filter $l$ is Cauchy with respect to the pullback uniform structure on $\alpha$ (induced by $f$) if and only if the image filter $f(l)$ is Cauchy in $\beta$.

cauchy_prod_iff theorem

[UniformSpace β] {F : Filter (α × β)} : Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)

Full source

lemma cauchy_prod_iff [UniformSpace β] {F : Filter (α × β)} :
    CauchyCauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F) := by
  simp_rw [instUniformSpaceProd, ← cauchy_comap_uniformSpace, ← cauchy_inf_uniformSpace]

Cauchy Criterion for Product Filters: $F$ is Cauchy in $\alpha \times \beta$ iff $\pi_1(F)$ and $\pi_2(F)$ are Cauchy

Informal description

Let $\alpha$ and $\beta$ be uniform spaces. A filter $F$ on the product space $\alpha \times \beta$ is Cauchy if and only if the pushforward filters $\text{map}(\pi_1, F)$ and $\text{map}(\pi_2, F)$ are Cauchy in $\alpha$ and $\beta$ respectively, where $\pi_1 \colon \alpha \times \beta \to \alpha$ and $\pi_2 \colon \alpha \times \beta \to \beta$ are the projection maps.

Cauchy.prod theorem

[UniformSpace β] {f : Filter α} {g : Filter β} (hf : Cauchy f) (hg : Cauchy g) : Cauchy (f ×ˢ g)

Full source

theorem Cauchy.prod [UniformSpace β] {f : Filter α} {g : Filter β} (hf : Cauchy f) (hg : Cauchy g) :
    Cauchy (f ×ˢ g) := by
  have := hf.1; have := hg.1
  simpa [cauchy_prod_iff, hf.1] using ⟨hf, hg⟩

Product of Cauchy Filters is Cauchy

Informal description

Let $\alpha$ and $\beta$ be uniform spaces. If $f$ is a Cauchy filter on $\alpha$ and $g$ is a Cauchy filter on $\beta$, then the product filter $f \times g$ is a Cauchy filter on $\alpha \times \beta$.

le_nhds_of_cauchy_adhp_aux theorem

 {f : Filter α} {x : α} (adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t) : f ≤ 𝓝 x

Full source

/-- The common part of the proofs of `le_nhds_of_cauchy_adhp` and
`SequentiallyComplete.le_nhds_of_seq_tendsto_nhds`: if for any entourage `s`
one can choose a set `t ∈ f` of diameter `s` such that it contains a point `y`
with `(x, y) ∈ s`, then `f` converges to `x`. -/
theorem le_nhds_of_cauchy_adhp_aux {f : Filter α} {x : α}
    (adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t) : f ≤ 𝓝 x := by
  -- Consider a neighborhood `s` of `x`
  intro s hs
  -- Take an entourage twice smaller than `s`
  rcases comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 hs) with ⟨U, U_mem, hU⟩
  -- Take a set `t ∈ f`, `t × t ⊆ U`, and a point `y ∈ t` such that `(x, y) ∈ U`
  rcases adhs U U_mem with ⟨t, t_mem, ht, y, hxy, hy⟩
  apply mem_of_superset t_mem
  -- Given a point `z ∈ t`, we have `(x, y) ∈ U` and `(y, z) ∈ t × t ⊆ U`, hence `z ∈ s`
  exact fun z hz => hU (prodMk_mem_compRel hxy (ht <| mk_mem_prod hy hz)) rfl

Convergence of Cauchy Filter with Adherent Point via Uniformity Conditions

Informal description

Let $\alpha$ be a uniform space with uniformity filter $\mathfrak{U}(\alpha)$. For any filter $f$ on $\alpha$ and any point $x \in \alpha$, if for every entourage $s \in \mathfrak{U}(\alpha)$ there exists a set $t \in f$ such that: 1. $t \times t \subseteq s$ (i.e., $t$ has diameter at most $s$), and 2. there exists a point $y \in t$ with $(x, y) \in s$, then the filter $f$ converges to $x$ in the topology induced by the uniformity.

le_nhds_of_cauchy_adhp theorem

{f : Filter α} {x : α} (hf : Cauchy f) (adhs : ClusterPt x f) : f ≤ 𝓝 x

Full source

/-- If `x` is an adherent (cluster) point for a Cauchy filter `f`, then it is a limit point
for `f`. -/
theorem le_nhds_of_cauchy_adhp {f : Filter α} {x : α} (hf : Cauchy f) (adhs : ClusterPt x f) :
    f ≤ 𝓝 x :=
  le_nhds_of_cauchy_adhp_aux
    (fun s hs => by
      obtain ⟨t, t_mem, ht⟩ : ∃ t ∈ f, t ×ˢ t ⊆ s := (cauchy_iff.1 hf).2 s hs
      use t, t_mem, ht
      exact forall_mem_nonempty_iff_neBot.2 adhs _ (inter_mem_inf (mem_nhds_left x hs) t_mem))

Convergence of Cauchy Filter at Cluster Point

Informal description

Let $\alpha$ be a uniform space, $f$ a Cauchy filter on $\alpha$, and $x \in \alpha$ a cluster point of $f$. Then $f$ converges to $x$ in the topology induced by the uniformity.

le_nhds_iff_adhp_of_cauchy theorem

{f : Filter α} {x : α} (hf : Cauchy f) : f ≤ 𝓝 x ↔ ClusterPt x f

Full source

theorem le_nhds_iff_adhp_of_cauchy {f : Filter α} {x : α} (hf : Cauchy f) :
    f ≤ 𝓝 x ↔ ClusterPt x f :=
  ⟨fun h => ClusterPt.of_le_nhds' h hf.1, le_nhds_of_cauchy_adhp hf⟩

Convergence of Cauchy Filter is Equivalent to Cluster Point Condition

Informal description

Let $\alpha$ be a uniform space, $f$ a Cauchy filter on $\alpha$, and $x \in \alpha$. Then $f$ converges to $x$ if and only if $x$ is a cluster point of $f$.

Cauchy.map theorem

[UniformSpace β] {f : Filter α} {m : α → β} (hf : Cauchy f) (hm : UniformContinuous m) : Cauchy (map m f)

Full source

nonrec theorem Cauchy.map [UniformSpace β] {f : Filter α} {m : α → β} (hf : Cauchy f)
    (hm : UniformContinuous m) : Cauchy (map m f) :=
  ⟨hf.1.map _,
    calc
      map m f ×ˢ map m f = map (Prod.map m m) (f ×ˢ f) := Filter.prod_map_map_eq
      _ ≤ Filter.map (Prod.map m m) (𝓤 α) := map_mono hf.right
      _ ≤ 𝓤 β := hm⟩

Image of a Cauchy Filter Under a Uniformly Continuous Map is Cauchy

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $f$ a Cauchy filter on $\alpha$, and $m \colon \alpha \to \beta$ a uniformly continuous map. Then the image filter $\text{map}\, m\, f$ is a Cauchy filter on $\beta$.

Cauchy.comap theorem

 [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f) (hm : comap (fun p : α × α => (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α)
  [NeBot (comap m f)] : Cauchy (comap m f)

Full source

nonrec theorem Cauchy.comap [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f)
    (hm : comap (fun p : α × α => (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α) [NeBot (comap m f)] :
    Cauchy (comap m f) :=
  ⟨‹_›,
    calc
      comap m f ×ˢ comap m f = comap (Prod.map m m) (f ×ˢ f) := prod_comap_comap_eq
      _ ≤ comap (Prod.map m m) (𝓤 β) := comap_mono hf.right
      _ ≤ 𝓤 α := hm⟩

Preimage of a Cauchy Filter Under a Uniformly Continuous Map is Cauchy

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $f$ a Cauchy filter on $\beta$, and $m : \alpha \to \beta$ a map such that: 1. The preimage of the uniformity filter on $\beta$ under the map $(p \mapsto (m(p.1), m(p.2)))$ is contained in the uniformity filter on $\alpha$. 2. The preimage filter $\text{comap}\, m\, f$ is non-trivial (i.e., does not contain the empty set). Then $\text{comap}\, m\, f$ is a Cauchy filter on $\alpha$.

Cauchy.comap' theorem

 [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f)
  (hm : Filter.comap (fun p : α × α => (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α) (_ : NeBot (Filter.comap m f)) :
  Cauchy (Filter.comap m f)

Full source

theorem Cauchy.comap' [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f)
    (hm : Filter.comap (fun p : α × α => (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α)
    (_ : NeBot (Filter.comap m f)) : Cauchy (Filter.comap m f) :=
  hf.comap hm

Preimage of a Cauchy filter under a uniformly continuous map is Cauchy

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $f$ a Cauchy filter on $\beta$, and $m \colon \alpha \to \beta$ a map such that: 1. The preimage of the uniformity filter on $\beta$ under the map $(x, y) \mapsto (m(x), m(y))$ is contained in the uniformity filter on $\alpha$. 2. The preimage filter $\text{comap}\, m\, f$ is non-trivial (i.e., does not contain the empty set). Then $\text{comap}\, m\, f$ is a Cauchy filter on $\alpha$.

CauchySeq definition

[Preorder β] (u : β → α)

Full source

/-- Cauchy sequences. Usually defined on ℕ, but often it is also useful to say that a function
defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it in a type class that
is general enough to cover both ℕ and ℝ, which are the main motivating examples. -/
def CauchySeq [Preorder β] (u : β → α) :=
  Cauchy (atTop.map u)

Cauchy sequence in a uniform space

Informal description

A function $u : \beta \to \alpha$ from a preorder $\beta$ to a uniform space $\alpha$ is called a *Cauchy sequence* if the filter generated by the images of $u$ over the filter of eventually large elements in $\beta$ is a Cauchy filter. This generalizes the notion of Cauchy sequences from $\mathbb{N}$ to arbitrary preorders, allowing for the study of Cauchy behavior in more general contexts such as $\mathbb{R}$ at infinity.

CauchySeq.tendsto_uniformity theorem

[Preorder β] {u : β → α} (h : CauchySeq u) : Tendsto (Prod.map u u) atTop (𝓤 α)

Full source

theorem CauchySeq.tendsto_uniformity [Preorder β] {u : β → α} (h : CauchySeq u) :
    Tendsto (Prod.map u u) atTop (𝓤 α) := by
  simpa only [Tendsto, prod_map_map_eq', prod_atTop_atTop_eq] using h.right

Uniform Convergence of Cauchy Sequences in Uniform Spaces

Informal description

For any Cauchy sequence $u : \beta \to \alpha$ in a uniform space $\alpha$ indexed by a preorder $\beta$, the map $(u \times u) : \beta \times \beta \to \alpha \times \alpha$ tends to the uniformity filter $\mathfrak{U}(\alpha)$ as the index tends to infinity. In other words, for any entourage $V \in \mathfrak{U}(\alpha)$, there exists $k_0 \in \beta$ such that for all $i, j \geq k_0$, the pair $(u(i), u(j))$ belongs to $V$.

CauchySeq.nonempty theorem

[Preorder β] {u : β → α} (hu : CauchySeq u) : Nonempty β

Full source

theorem CauchySeq.nonempty [Preorder β] {u : β → α} (hu : CauchySeq u) : Nonempty β :=
  @nonempty_of_neBot _ _ <| (map_neBot_iff _).1 hu.1

Nonemptiness of the Index Type for Cauchy Sequences

Informal description

For any Cauchy sequence $u : \beta \to \alpha$ in a uniform space $\alpha$ where $\beta$ is a preorder, the index type $\beta$ is nonempty.

CauchySeq.mem_entourage theorem

 {β : Type*} [SemilatticeSup β] {u : β → α} (h : CauchySeq u) {V : Set (α × α)} (hV : V ∈ 𝓤 α) :
  ∃ k₀, ∀ i j, k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Full source

theorem CauchySeq.mem_entourage {β : Type*} [SemilatticeSup β] {u : β → α} (h : CauchySeq u)
    {V : Set (α × α)} (hV : V ∈ 𝓤 α) : ∃ k₀, ∀ i j, k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V := by
  haveI := h.nonempty
  have := h.tendsto_uniformity; rw [← prod_atTop_atTop_eq] at this
  simpa [MapsTo] using atTop_basis.prod_self.tendsto_left_iff.1 this V hV

Cauchy Sequence Uniformity Criterion: $(u_i, u_j) \in V$ for Large Indices

Informal description

Let $\alpha$ be a uniform space and $\beta$ a join-semilattice. For any Cauchy sequence $u : \beta \to \alpha$ and any entourage $V$ in the uniformity of $\alpha$, there exists an index $k_0 \in \beta$ such that for all $i, j \geq k_0$, the pair $(u(i), u(j))$ belongs to $V$.

Filter.Tendsto.cauchySeq theorem

[SemilatticeSup β] [Nonempty β] {f : β → α} {x} (hx : Tendsto f atTop (𝓝 x)) : CauchySeq f

Full source

theorem Filter.Tendsto.cauchySeq [SemilatticeSup β] [Nonempty β] {f : β → α} {x}
    (hx : Tendsto f atTop (𝓝 x)) : CauchySeq f :=
  hx.cauchy_map

Convergent Sequences are Cauchy in Uniform Spaces

Informal description

Let $\beta$ be a nonempty join-semilattice and $\alpha$ a uniform space. For any function $f \colon \beta \to \alpha$ that converges to a point $x \in \alpha$ as the index tends to infinity, the sequence $f$ is a Cauchy sequence.

cauchySeq_const theorem

[SemilatticeSup β] [Nonempty β] (x : α) : CauchySeq fun _ : β => x

Full source

theorem cauchySeq_const [SemilatticeSup β] [Nonempty β] (x : α) : CauchySeq fun _ : β => x :=
  tendsto_const_nhds.cauchySeq

Constant Sequences are Cauchy in Uniform Spaces

Informal description

Let $\beta$ be a nonempty join-semilattice and $\alpha$ a uniform space. For any constant sequence $u : \beta \to \alpha$ defined by $u(n) = x$ for some fixed $x \in \alpha$, the sequence $u$ is Cauchy.

cauchySeq_iff_tendsto theorem

[Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ Tendsto (Prod.map u u) atTop (𝓤 α)

Full source

theorem cauchySeq_iff_tendsto [Nonempty β] [SemilatticeSup β] {u : β → α} :
    CauchySeqCauchySeq u ↔ Tendsto (Prod.map u u) atTop (𝓤 α) :=
  cauchy_map_iff'.trans <| by simp only [prod_atTop_atTop_eq, Prod.map_def]

Characterization of Cauchy Sequences via Uniform Convergence of Pairs

Informal description

Let $\beta$ be a nonempty directed set (join-semilattice) and $\alpha$ a uniform space. A sequence $u \colon \beta \to \alpha$ is Cauchy if and only if the map $(x, y) \mapsto (u(x), u(y))$ tends to the uniformity filter $\mathfrak{U}(\alpha)$ as $x$ and $y$ tend to infinity in $\beta$.

CauchySeq.comp_tendsto theorem

 {γ} [Preorder β] [SemilatticeSup γ] [Nonempty γ] {f : β → α} (hf : CauchySeq f) {g : γ → β}
  (hg : Tendsto g atTop atTop) : CauchySeq (f ∘ g)

Full source

theorem CauchySeq.comp_tendsto {γ} [Preorder β] [SemilatticeSup γ] [Nonempty γ] {f : β → α}
    (hf : CauchySeq f) {g : γ → β} (hg : Tendsto g atTop atTop) : CauchySeq (f ∘ g) :=
  ⟨inferInstance, le_trans (prod_le_prod.mpr ⟨Tendsto.comp le_rfl hg, Tendsto.comp le_rfl hg⟩) hf.2⟩

Composition of a Cauchy Sequence with a Tendsto Function is Cauchy

Informal description

Let $\beta$ be a preorder, $\gamma$ a nonempty join-semilattice, and $\alpha$ a uniform space. Given a Cauchy sequence $f \colon \beta \to \alpha$ and a function $g \colon \gamma \to \beta$ that tends to infinity (i.e., $\text{Tendsto}\, g\, \text{atTop}\, \text{atTop}$), the composition $f \circ g \colon \gamma \to \alpha$ is also a Cauchy sequence.

CauchySeq.comp_injective theorem

 [SemilatticeSup β] [NoMaxOrder β] [Nonempty β] {u : ℕ → α} (hu : CauchySeq u) {f : β → ℕ} (hf : Injective f) :
  CauchySeq (u ∘ f)

Full source

theorem CauchySeq.comp_injective [SemilatticeSup β] [NoMaxOrder β] [Nonempty β] {u : ℕ → α}
    (hu : CauchySeq u) {f : β → ℕ} (hf : Injective f) : CauchySeq (u ∘ f) :=
  hu.comp_tendsto <| Nat.cofinite_eq_atTop ▸ hf.tendsto_cofinite.mono_left atTop_le_cofinite

Injective Subsequence of a Cauchy Sequence is Cauchy

Informal description

Let $\beta$ be a nonempty directed set (join-semilattice) with no maximal elements, and let $\alpha$ be a uniform space. Given a Cauchy sequence $u \colon \mathbb{N} \to \alpha$ and an injective function $f \colon \beta \to \mathbb{N}$, the composition $u \circ f \colon \beta \to \alpha$ is also a Cauchy sequence.

Function.Bijective.cauchySeq_comp_iff theorem

{f : ℕ → ℕ} (hf : Bijective f) (u : ℕ → α) : CauchySeq (u ∘ f) ↔ CauchySeq u

Full source

theorem Function.Bijective.cauchySeq_comp_iff {f : ℕ → ℕ} (hf : Bijective f) (u : ℕ → α) :
    CauchySeqCauchySeq (u ∘ f) ↔ CauchySeq u := by
  refine ⟨fun H => ?_, fun H => H.comp_injective hf.injective⟩
  lift f to ℕℕ ≃ ℕ using hf
  simpa only [Function.comp_def, f.apply_symm_apply] using H.comp_injective f.symm.injective

Bijective Reindexing Preserves Cauchy Sequences

Informal description

Let $\alpha$ be a uniform space and $f \colon \mathbb{N} \to \mathbb{N}$ be a bijective function. For any sequence $u \colon \mathbb{N} \to \alpha$, the composition $u \circ f$ is a Cauchy sequence if and only if $u$ is a Cauchy sequence.

CauchySeq.subseq_subseq_mem theorem

 {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α} (hu : CauchySeq u) {f g : ℕ → ℕ} (hf : Tendsto f atTop atTop)
  (hg : Tendsto g atTop atTop) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Full source

theorem CauchySeq.subseq_subseq_mem {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α}
    (hu : CauchySeq u) {f g : ℕ → ℕ} (hf : Tendsto f atTop atTop) (hg : Tendsto g atTop atTop) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n := by
  rw [cauchySeq_iff_tendsto] at hu
  exact ((hu.comp <| hf.prod_atTop hg).comp tendsto_atTop_diagonal).subseq_mem hV

Existence of a Common Subsequence for Cauchy Sequences under Two Mappings

Informal description

Let $\alpha$ be a uniform space and $u \colon \mathbb{N} \to \alpha$ a Cauchy sequence. Given a sequence of entourages $(V_n)_{n \in \mathbb{N}}$ in the uniformity $\mathfrak{U}(\alpha)$ and two strictly increasing sequences $f, g \colon \mathbb{N} \to \mathbb{N}$, there exists a strictly increasing function $\varphi \colon \mathbb{N} \to \mathbb{N}$ such that for all $n \in \mathbb{N}$, the pair $(u_{f(\varphi(n))}, u_{g(\varphi(n))})$ belongs to $V_n$.

cauchySeq_iff' theorem

{u : ℕ → α} : CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∀ᶠ k in atTop, k ∈ Prod.map u u ⁻¹' V

Full source

theorem cauchySeq_iff' {u : ℕ → α} :
    CauchySeqCauchySeq u ↔ ∀ V ∈ 𝓤 α, ∀ᶠ k in atTop, k ∈ Prod.map u u ⁻¹' V :=
  cauchySeq_iff_tendsto

Characterization of Cauchy Sequences via Preimages of Entourages

Informal description

A sequence $u \colon \mathbb{N} \to \alpha$ in a uniform space $\alpha$ is a Cauchy sequence if and only if for every entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$, the set $\{k \in \mathbb{N} \mid (u_k, u_k) \in V\}$ is eventually true (i.e., contains all sufficiently large $k$).

cauchySeq_iff theorem

{u : ℕ → α} : CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Full source

theorem cauchySeq_iff {u : ℕ → α} :
    CauchySeqCauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V := by
  simp only [cauchySeq_iff', Filter.eventually_atTop_prod_self', mem_preimage, Prod.map_apply]

Characterization of Cauchy Sequences in Uniform Spaces

Informal description

A sequence $u : \mathbb{N} \to \alpha$ in a uniform space $\alpha$ is a Cauchy sequence if and only if for every entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$, there exists a natural number $N$ such that for all $k, l \geq N$, the pair $(u_k, u_l)$ belongs to $V$.

CauchySeq.prodMap theorem

 {γ δ} [UniformSpace β] [Preorder γ] [Preorder δ] {u : γ → α} {v : δ → β} (hu : CauchySeq u) (hv : CauchySeq v) :
  CauchySeq (Prod.map u v)

Full source

theorem CauchySeq.prodMap {γ δ} [UniformSpace β] [Preorder γ] [Preorder δ] {u : γ → α} {v : δ → β}
    (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (Prod.map u v) := by
  simpa only [CauchySeq, prod_map_map_eq', prod_atTop_atTop_eq] using hu.prod hv

Product of Cauchy Sequences is Cauchy

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, and let $\gamma$ and $\delta$ be preorders. Given a Cauchy sequence $u : \gamma \to \alpha$ and a Cauchy sequence $v : \delta \to \beta$, the product sequence $\text{Prod.map } u \, v : \gamma \times \delta \to \alpha \times \beta$ is also a Cauchy sequence.

CauchySeq.prodMk theorem

 {γ} [UniformSpace β] [Preorder γ] {u : γ → α} {v : γ → β} (hu : CauchySeq u) (hv : CauchySeq v) :
  CauchySeq fun x => (u x, v x)

Full source

theorem CauchySeq.prodMk {γ} [UniformSpace β] [Preorder γ] {u : γ → α} {v : γ → β}
    (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq fun x => (u x, v x) :=
  haveI := hu.1.of_map
  (Cauchy.prod hu hv).mono (tendsto_map.prodMk tendsto_map)

Pairwise Cauchy Sequence in Product Uniform Space

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $\gamma$ a preorder, and $u \colon \gamma \to \alpha$, $v \colon \gamma \to \beta$ Cauchy sequences. Then the sequence $\gamma \to \alpha \times \beta$ defined by $x \mapsto (u(x), v(x))$ is a Cauchy sequence in the product uniform space $\alpha \times \beta$.

CauchySeq.eventually_eventually theorem

 [Preorder β] {u : β → α} (hu : CauchySeq u) {V : Set (α × α)} (hV : V ∈ 𝓤 α) :
  ∀ᶠ k in atTop, ∀ᶠ l in atTop, (u k, u l) ∈ V

Full source

theorem CauchySeq.eventually_eventually [Preorder β] {u : β → α} (hu : CauchySeq u)
    {V : Set (α × α)} (hV : V ∈ 𝓤 α) : ∀ᶠ k in atTop, ∀ᶠ l in atTop, (u k, u l) ∈ V :=
  eventually_atTop_curry <| hu.tendsto_uniformity hV

Uniform Closeness of Cauchy Sequences in Uniform Spaces

Informal description

Let $\alpha$ be a uniform space and $\beta$ a preorder. For any Cauchy sequence $u \colon \beta \to \alpha$ and any entourage $V$ in the uniformity of $\alpha$, there exists $k_0 \in \beta$ such that for all $k, l \geq k_0$, the pair $(u(k), u(l))$ belongs to $V$.

UniformContinuous.comp_cauchySeq theorem

 {γ} [UniformSpace β] [Preorder γ] {f : α → β} (hf : UniformContinuous f) {u : γ → α} (hu : CauchySeq u) :
  CauchySeq (f ∘ u)

Full source

theorem UniformContinuous.comp_cauchySeq {γ} [UniformSpace β] [Preorder γ] {f : α → β}
    (hf : UniformContinuous f) {u : γ → α} (hu : CauchySeq u) : CauchySeq (f ∘ u) :=
  hu.map hf

Uniformly Continuous Function Preserves Cauchy Sequences

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $\gamma$ a preorder, $f \colon \alpha \to \beta$ a uniformly continuous function, and $u \colon \gamma \to \alpha$ a Cauchy sequence. Then the composition $f \circ u \colon \gamma \to \beta$ is also a Cauchy sequence.

CauchySeq.subseq_mem theorem

 {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α} (hu : CauchySeq u) :
  ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, (u <| φ (n + 1), u <| φ n) ∈ V n

Full source

theorem CauchySeq.subseq_mem {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α}
    (hu : CauchySeq u) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, (u <| φ (n + 1), u <| φ n) ∈ V n := by
  have : ∀ n, ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n := fun n => by
    rw [cauchySeq_iff] at hu
    rcases hu _ (hV n) with ⟨N, H⟩
    exact ⟨N, fun k hk l hl => H _ (le_trans hk hl) _ hk⟩
  obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ∀ l ≥ φ n, (u l, u <| φ n)(u l, u <| φ n) ∈ V n⟩ :=
    extraction_forall_of_eventually' this
  exact ⟨φ, φ_extr, fun n => hφ _ _ (φ_extr <| Nat.lt_add_one n).le⟩

Existence of Subsequence in Cauchy Sequence Matching Given Entourages

Informal description

Let $\alpha$ be a uniform space and $V : \mathbb{N} \to \mathcal{P}(\alpha \times \alpha)$ be a sequence of entourages in the uniformity $\mathfrak{U}(\alpha)$. For any Cauchy sequence $u : \mathbb{N} \to \alpha$, there exists a strictly increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ such that for all $n \in \mathbb{N}$, the pair $(u_{\varphi(n+1)}, u_{\varphi(n)})$ belongs to $V_n$.

Filter.Tendsto.subseq_mem_entourage theorem

 {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α} {a : α} (hu : Tendsto u atTop (𝓝 a)) :
  ∃ φ : ℕ → ℕ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ n, (u <| φ (n + 1), u <| φ n) ∈ V (n + 1)

Full source

theorem Filter.Tendsto.subseq_mem_entourage {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α}
    {a : α} (hu : Tendsto u atTop (𝓝 a)) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧
      ∀ n, (u <| φ (n + 1), u <| φ n) ∈ V (n + 1) := by
  rcases mem_atTop_sets.1 (hu (ball_mem_nhds a (symm_le_uniformity <| hV 0))) with ⟨n, hn⟩
  rcases (hu.comp (tendsto_add_atTop_nat n)).cauchySeq.subseq_mem fun n => hV (n + 1) with
    ⟨φ, φ_mono, hφV⟩
  exact ⟨fun k => φ k + n, φ_mono.add_const _, hn _ le_add_self, hφV⟩

Existence of Convergent Subsequence Matching Given Entourages

Informal description

Let $\alpha$ be a uniform space and $V : \mathbb{N} \to \mathcal{P}(\alpha \times \alpha)$ a sequence of entourages in the uniformity $\mathfrak{U}(\alpha)$. For any sequence $u : \mathbb{N} \to \alpha$ converging to a point $a \in \alpha$, there exists a strictly increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ such that: 1. $(u_{\varphi(0)}, a) \in V_0$, and 2. for all $n \in \mathbb{N}$, $(u_{\varphi(n+1)}, u_{\varphi(n)}) \in V_{n+1}$.

tendsto_nhds_of_cauchySeq_of_subseq theorem

 [Preorder β] {u : β → α} (hu : CauchySeq u) {ι : Type*} {f : ι → β} {p : Filter ι} [NeBot p] (hf : Tendsto f p atTop)
  {a : α} (ha : Tendsto (u ∘ f) p (𝓝 a)) : Tendsto u atTop (𝓝 a)

Full source

/-- If a Cauchy sequence has a convergent subsequence, then it converges. -/
theorem tendsto_nhds_of_cauchySeq_of_subseq [Preorder β] {u : β → α} (hu : CauchySeq u)
    {ι : Type*} {f : ι → β} {p : Filter ι} [NeBot p] (hf : Tendsto f p atTop) {a : α}
    (ha : Tendsto (u ∘ f) p (𝓝 a)) : Tendsto u atTop (𝓝 a) :=
  le_nhds_of_cauchy_adhp hu (ha.mapClusterPt.of_comp hf)

Convergence of Cauchy Sequence via Convergent Subsequence

Informal description

Let $\alpha$ be a uniform space and $\beta$ a preorder. Given a Cauchy sequence $u \colon \beta \to \alpha$, suppose there exists a non-trivial filter $p$ on some index type $\iota$ and a function $f \colon \iota \to \beta$ such that $f$ tends to infinity along $p$. If the subsequence $u \circ f$ converges to a point $a \in \alpha$ along $p$, then the original sequence $u$ also converges to $a$.

cauchySeq_shift theorem

{u : ℕ → α} (k : ℕ) : CauchySeq (fun n ↦ u (n + k)) ↔ CauchySeq u

Full source

/-- Any shift of a Cauchy sequence is also a Cauchy sequence. -/
theorem cauchySeq_shift {u : ℕ → α} (k : ℕ) : CauchySeqCauchySeq (fun n ↦ u (n + k)) ↔ CauchySeq u := by
  constructor <;> intro h
  · rw [cauchySeq_iff] at h ⊢
    intro V mV
    obtain ⟨N, h⟩ := h V mV
    use N + k
    intro a ha b hb
    convert h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb) <;> omega
  · exact h.comp_tendsto (tendsto_add_atTop_nat k)

Shift Invariance of Cauchy Sequences

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ in a uniform space $\alpha$ and any natural number $k$, the shifted sequence $n \mapsto u(n + k)$ is a Cauchy sequence if and only if the original sequence $u$ is a Cauchy sequence.

Filter.HasBasis.cauchySeq_iff theorem

 {γ} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)} (h : (𝓤 α).HasBasis p s) :
  CauchySeq u ↔ ∀ i, p i → ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → (u m, u n) ∈ s i

Full source

theorem Filter.HasBasis.cauchySeq_iff {γ} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop}
    {s : γ → Set (α × α)} (h : (𝓤 α).HasBasis p s) :
    CauchySeqCauchySeq u ↔ ∀ i, p i → ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → (u m, u n) ∈ s i := by
  rw [cauchySeq_iff_tendsto, ← prod_atTop_atTop_eq]
  refine (atTop_basis.prod_self.tendsto_iff h).trans ?_
  simp only [exists_prop, true_and, MapsTo, preimage, subset_def, Prod.forall, mem_prod_eq,
    mem_setOf_eq, mem_Ici, and_imp, Prod.map, @forall_swap (_ ≤ _) β]

Characterization of Cauchy Sequences via Uniformity Basis

Informal description

Let $\alpha$ be a uniform space, $\beta$ a nonempty directed set (join-semilattice), and $\gamma$ an index type. Suppose the uniformity filter $\mathfrak{U}(\alpha)$ has a basis $\{s(i) \mid p(i)\}$ where $p : \gamma \to \mathrm{Prop}$ and $s : \gamma \to \mathrm{Set}(\alpha \times \alpha)$. Then a sequence $u : \beta \to \alpha$ is Cauchy if and only if for every index $i$ satisfying $p(i)$, there exists $N \in \beta$ such that for all $m, n \geq N$, the pair $(u(m), u(n))$ belongs to $s(i)$.

Filter.HasBasis.cauchySeq_iff' theorem

 {γ} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)} (H : (𝓤 α).HasBasis p s) :
  CauchySeq u ↔ ∀ i, p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i

Full source

theorem Filter.HasBasis.cauchySeq_iff' {γ} [Nonempty β] [SemilatticeSup β] {u : β → α}
    {p : γ → Prop} {s : γ → Set (α × α)} (H : (𝓤 α).HasBasis p s) :
    CauchySeqCauchySeq u ↔ ∀ i, p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i := by
  refine H.cauchySeq_iff.trans ⟨fun h i hi => ?_, fun h i hi => ?_⟩
  · exact (h i hi).imp fun N hN n hn => hN n hn N le_rfl
  · rcases comp_symm_of_uniformity (H.mem_of_mem hi) with ⟨t, ht, ht', hts⟩
    rcases H.mem_iff.1 ht with ⟨j, hj, hjt⟩
    refine (h j hj).imp fun N hN m hm n hn => hts ⟨u N, hjt ?_, ht' <| hjt ?_⟩
    exacts [hN m hm, hN n hn]

Characterization of Cauchy Sequences via Uniformity Basis (One-Sided Version)

Informal description

Let $\alpha$ be a uniform space, $\beta$ a nonempty directed set (join-semilattice), and $\gamma$ an index type. Suppose the uniformity filter $\mathfrak{U}(\alpha)$ has a basis $\{s(i) \mid p(i)\}$ where $p : \gamma \to \mathrm{Prop}$ and $s : \gamma \to \mathrm{Set}(\alpha \times \alpha)$. Then a sequence $u : \beta \to \alpha$ is Cauchy if and only if for every index $i$ satisfying $p(i)$, there exists $N \in \beta$ such that for all $n \geq N$, the pair $(u(n), u(N))$ belongs to $s(i)$.

cauchySeq_of_controlled theorem

 [SemilatticeSup β] [Nonempty β] (U : β → Set (α × α)) (hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s) {f : β → α}
  (hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N) : CauchySeq f

Full source

theorem cauchySeq_of_controlled [SemilatticeSup β] [Nonempty β] (U : β → Set (α × α))
    (hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s) {f : β → α}
    (hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n)(f m, f n) ∈ U N) : CauchySeq f :=
  cauchySeq_iff_tendsto.2
    (by
      intro s hs
      rw [mem_map, mem_atTop_sets]
      obtain ⟨N, hN⟩ := hU s hs
      refine ⟨(N, N), fun mn hmn => ?_⟩
      obtain ⟨m, n⟩ := mn
      exact hN (hf hmn.1 hmn.2))

Controlled Sequences are Cauchy in Uniform Spaces

Informal description

Let $\alpha$ be a uniform space and $\beta$ a nonempty directed set (join-semilattice). Given a family of sets $U_n \subseteq \alpha \times \alpha$ indexed by $\beta$ such that for every entourage $s$ in the uniformity $\mathfrak{U}(\alpha)$, there exists $n$ with $U_n \subseteq s$, and a function $f \colon \beta \to \alpha$ satisfying the control condition that for all $N, m, n \in \beta$ with $N \leq m$ and $N \leq n$, the pair $(f(m), f(n))$ lies in $U_N$, then $f$ is a Cauchy sequence.

isComplete_iff_clusterPt theorem

{s : Set α} : IsComplete s ↔ ∀ l, Cauchy l → l ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x l

Full source

theorem isComplete_iff_clusterPt {s : Set α} :
    IsCompleteIsComplete s ↔ ∀ l, Cauchy l → l ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x l :=
  forall₃_congr fun _ hl _ => exists_congr fun _ => and_congr_right fun _ =>
    le_nhds_iff_adhp_of_cauchy hl

Characterization of Complete Subsets via Cluster Points of Cauchy Filters

Informal description

A subset $s$ of a uniform space $\alpha$ is complete if and only if for every Cauchy filter $l$ on $\alpha$ that is contained in the powerset of $s$, there exists a point $x \in s$ such that $x$ is a cluster point of $l$.

isComplete_iff_ultrafilter theorem

 {s : Set α} : IsComplete s ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x

Full source

theorem isComplete_iff_ultrafilter {s : Set α} :
    IsCompleteIsComplete s ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x := by
  refine ⟨fun h l => h l, fun H => isComplete_iff_clusterPt.2 fun l hl hls => ?_⟩
  haveI := hl.1
  rcases H (Ultrafilter.of l) hl.ultrafilter_of ((Ultrafilter.of_le l).trans hls) with ⟨x, hxs, hxl⟩
  exact ⟨x, hxs, (ClusterPt.of_le_nhds hxl).mono (Ultrafilter.of_le l)⟩

Characterization of Complete Subsets via Ultrafilters

Informal description

A subset $s$ of a uniform space $\alpha$ is complete if and only if for every ultrafilter $l$ on $\alpha$ that is Cauchy and contains $s$ (i.e., $l \leq \mathcal{P}(s)$), there exists a point $x \in s$ such that $l$ converges to $x$ (i.e., $l \leq \mathcal{N}(x)$, where $\mathcal{N}(x)$ is the neighborhood filter of $x$).

IsComplete.union theorem

{s t : Set α} (hs : IsComplete s) (ht : IsComplete t) : IsComplete (s ∪ t)

Full source

protected theorem IsComplete.union {s t : Set α} (hs : IsComplete s) (ht : IsComplete t) :
    IsComplete (s ∪ t) := by
  simp only [isComplete_iff_ultrafilter', Ultrafilter.union_mem_iff, or_imp] at *
  exact fun l hl =>
    ⟨fun hsl => (hs l hl hsl).imp fun x hx => ⟨Or.inl hx.1, hx.2⟩, fun htl =>
      (ht l hl htl).imp fun x hx => ⟨Or.inr hx.1, hx.2⟩⟩

Union of Complete Subsets is Complete

Informal description

Let $s$ and $t$ be subsets of a uniform space $\alpha$. If both $s$ and $t$ are complete (i.e., every Cauchy filter containing $s$ or $t$ converges to a point in $s$ or $t$ respectively), then their union $s \cup t$ is also complete.

isComplete_iUnion_separated theorem

 {ι : Sort*} {s : ι → Set α} (hs : ∀ i, IsComplete (s i)) {U : Set (α × α)} (hU : U ∈ 𝓤 α)
  (hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j) : IsComplete (⋃ i, s i)

Full source

theorem isComplete_iUnion_separated {ι : Sort*} {s : ι → Set α} (hs : ∀ i, IsComplete (s i))
    {U : Set (α × α)} (hU : U ∈ 𝓤 α) (hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j) :
    IsComplete (⋃ i, s i) := by
  set S := ⋃ i, s i
  intro l hl hls
  rw [le_principal_iff] at hls
  obtain ⟨hl_ne, hl'⟩ := cauchy_iff.1 hl
  obtain ⟨t, htS, htl, htU⟩ : ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U := by
    rcases hl' U hU with ⟨t, htl, htU⟩
    refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
    gcongr <;> apply inter_subset_left
  obtain ⟨i, hi⟩ : ∃ i, t ⊆ s i := by
    rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩
    rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩
    refine ⟨i, fun y hy => ?_⟩
    rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩
    rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]
  rcases hs i l hl (le_principal_iff.2 <| mem_of_superset htl hi) with ⟨x, hxs, hlx⟩
  exact ⟨x, mem_iUnion.2 ⟨i, hxs⟩, hlx⟩

Completeness of Separated Union of Complete Sets

Informal description

Let $\alpha$ be a uniform space and $\{s_i\}_{i \in \iota}$ be a family of complete subsets of $\alpha$. Suppose there exists an entourage $U$ in the uniformity of $\alpha$ such that for any two indices $i, j \in \iota$ and any points $x \in s_i$, $y \in s_j$, if $(x, y) \in U$ then $i = j$. Then the union $\bigcup_{i \in \iota} s_i$ is complete.

CompleteSpace structure

(α : Type u) [UniformSpace α]

Full source

/-- A complete space is defined here using uniformities. A uniform space
  is complete if every Cauchy filter converges. -/
class CompleteSpace (α : Type u) [UniformSpace α] : Prop where
  /-- In a complete uniform space, every Cauchy filter converges. -/
  complete : ∀ {f : Filter α}, Cauchy f → ∃ x, f ≤ 𝓝 x

Complete Uniform Space

Informal description

A uniform space $\alpha$ is called *complete* if every Cauchy filter on $\alpha$ converges to some point in $\alpha$. Here, a Cauchy filter is a filter $f$ such that for every entourage $U$ in the uniformity of $\alpha$, there exists a set $s \in f$ with $s \times s \subseteq U$.

complete_univ theorem

{α : Type u} [UniformSpace α] [CompleteSpace α] : IsComplete (univ : Set α)

Full source

theorem complete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] :
    IsComplete (univ : Set α) := fun f hf _ => by
  rcases CompleteSpace.complete hf with ⟨x, hx⟩
  exact ⟨x, mem_univ x, hx⟩

Completeness of the Universal Set in a Complete Uniform Space

Informal description

If $\alpha$ is a complete uniform space, then the universal set $\text{univ} \subseteq \alpha$ is a complete subset.

CompleteSpace.prod instance

[UniformSpace β] [CompleteSpace α] [CompleteSpace β] : CompleteSpace (α × β)

Full source

instance CompleteSpace.prod [UniformSpace β] [CompleteSpace α] [CompleteSpace β] :
    CompleteSpace (α × β) where
  complete hf :=
    let ⟨x1, hx1⟩ := CompleteSpace.complete <| hf.map uniformContinuous_fst
    let ⟨x2, hx2⟩ := CompleteSpace.complete <| hf.map uniformContinuous_snd
    ⟨(x1, x2), by rw [nhds_prod_eq, le_prod]; constructor <;> assumption⟩

Completeness of Product Uniform Spaces

Informal description

The product $\alpha \times \beta$ of two complete uniform spaces $\alpha$ and $\beta$ is itself a complete uniform space.

CompleteSpace.fst_of_prod theorem

[UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty β] : CompleteSpace α

Full source

lemma CompleteSpace.fst_of_prod [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty β] :
    CompleteSpace α where
  complete hf :=
    let ⟨y⟩ := h
    let ⟨(a, b), hab⟩ := CompleteSpace.complete <| hf.prod <| cauchy_pure (a := y)
    ⟨a, by simpa only [map_fst_prod, nhds_prod_eq] using map_mono (m := Prod.fst) hab⟩

Completeness of First Factor in Product Space

Informal description

Let $\alpha$ and $\beta$ be uniform spaces. If the product space $\alpha \times \beta$ is complete and $\beta$ is nonempty, then $\alpha$ is complete.

CompleteSpace.snd_of_prod theorem

[UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty α] : CompleteSpace β

Full source

lemma CompleteSpace.snd_of_prod [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty α] :
    CompleteSpace β where
  complete hf :=
    let ⟨x⟩ := h
    let ⟨(a, b), hab⟩ := CompleteSpace.complete <| (cauchy_pure (a := x)).prod hf
    ⟨b, by simpa only [map_snd_prod, nhds_prod_eq] using map_mono (m := Prod.snd) hab⟩

Completeness of Second Factor in Product Space

Informal description

Let $\alpha$ and $\beta$ be uniform spaces. If the product space $\alpha \times \beta$ is complete and $\alpha$ is nonempty, then $\beta$ is complete.

completeSpace_prod_of_nonempty theorem

[UniformSpace β] [Nonempty α] [Nonempty β] : CompleteSpace (α × β) ↔ CompleteSpace α ∧ CompleteSpace β

Full source

lemma completeSpace_prod_of_nonempty [UniformSpace β] [Nonempty α] [Nonempty β] :
    CompleteSpaceCompleteSpace (α × β) ↔ CompleteSpace α ∧ CompleteSpace β :=
  ⟨fun _ ↦ ⟨.fst_of_prod (β := β), .snd_of_prod (α := α)⟩, fun ⟨_, _⟩ ↦ .prod⟩

Completeness of Product Space for Nonempty Uniform Spaces: $\alpha \times \beta$ Complete $\iff$ $\alpha$ and $\beta$ Complete

Informal description

Let $\alpha$ and $\beta$ be nonempty uniform spaces. The product space $\alpha \times \beta$ is complete if and only if both $\alpha$ and $\beta$ are complete.

CompleteSpace.mulOpposite instance

[CompleteSpace α] : CompleteSpace αᵐᵒᵖ

Full source

@[to_additive]
instance CompleteSpace.mulOpposite [CompleteSpace α] : CompleteSpace αᵐᵒᵖ where
  complete hf :=
    MulOpposite.op_surjective.exists.mpr <|
      let ⟨x, hx⟩ := CompleteSpace.complete (hf.map MulOpposite.uniformContinuous_unop)
      ⟨x, (map_le_iff_le_comap.mp hx).trans_eq <| MulOpposite.comap_unop_nhds _⟩

Completeness of the Multiplicative Opposite Uniform Space

Informal description

For any complete uniform space $\alpha$, the multiplicative opposite $\alpha^{\mathrm{op}}$ is also a complete uniform space.

completeSpace_of_isComplete_univ theorem

(h : IsComplete (univ : Set α)) : CompleteSpace α

Full source

/-- If `univ` is complete, the space is a complete space -/
theorem completeSpace_of_isComplete_univ (h : IsComplete (univ : Set α)) : CompleteSpace α :=
  ⟨fun hf => let ⟨x, _, hx⟩ := h _ hf ((@principal_univ α).symm ▸ le_top); ⟨x, hx⟩⟩

Completeness from Universal Set Completeness

Informal description

If the universal set $\text{univ} = \alpha$ is a complete subset of the uniform space $\alpha$, then $\alpha$ is a complete space. That is, if every Cauchy filter on $\alpha$ converges to some point in $\alpha$, then $\alpha$ is complete.

completeSpace_iff_isComplete_univ theorem

: CompleteSpace α ↔ IsComplete (univ : Set α)

Full source

theorem completeSpace_iff_isComplete_univ : CompleteSpaceCompleteSpace α ↔ IsComplete (univ : Set α) :=
  ⟨@complete_univ α _, completeSpace_of_isComplete_univ⟩

Characterization of Complete Uniform Spaces via Universal Set Completeness

Informal description

A uniform space $\alpha$ is complete if and only if the universal set $\text{univ} \subseteq \alpha$ is a complete subset, meaning every Cauchy filter on $\alpha$ converges to some point in $\alpha$.

completeSpace_iff_ultrafilter theorem

: CompleteSpace α ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ∃ x : α, ↑l ≤ 𝓝 x

Full source

theorem completeSpace_iff_ultrafilter :
    CompleteSpaceCompleteSpace α ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ∃ x : α, ↑l ≤ 𝓝 x := by
  simp [completeSpace_iff_isComplete_univ, isComplete_iff_ultrafilter]

Characterization of Complete Uniform Spaces via Ultrafilters

Informal description

A uniform space $\alpha$ is complete if and only if every ultrafilter $l$ on $\alpha$ that is Cauchy converges to some point $x \in \alpha$ (i.e., $l$ is finer than the neighborhood filter of $x$).

cauchy_iff_exists_le_nhds theorem

[CompleteSpace α] {l : Filter α} [NeBot l] : Cauchy l ↔ ∃ x, l ≤ 𝓝 x

Full source

theorem cauchy_iff_exists_le_nhds [CompleteSpace α] {l : Filter α} [NeBot l] :
    CauchyCauchy l ↔ ∃ x, l ≤ 𝓝 x :=
  ⟨CompleteSpace.complete, fun ⟨_, hx⟩ => cauchy_nhds.mono hx⟩

Characterization of Cauchy Filters in Complete Uniform Spaces via Convergence

Informal description

Let $\alpha$ be a complete uniform space and $l$ be a non-trivial filter on $\alpha$. Then $l$ is a Cauchy filter if and only if there exists a point $x \in \alpha$ such that $l$ is finer than the neighborhood filter of $x$ (i.e., $l$ converges to $x$).

cauchy_map_iff_exists_tendsto theorem

[CompleteSpace α] {l : Filter β} {f : β → α} [NeBot l] : Cauchy (l.map f) ↔ ∃ x, Tendsto f l (𝓝 x)

Full source

theorem cauchy_map_iff_exists_tendsto [CompleteSpace α] {l : Filter β} {f : β → α} [NeBot l] :
    CauchyCauchy (l.map f) ↔ ∃ x, Tendsto f l (𝓝 x) :=
  cauchy_iff_exists_le_nhds

Characterization of Cauchy Filters via Convergence in Complete Uniform Spaces

Informal description

Let $\alpha$ be a complete uniform space, $\beta$ a type, and $l$ a non-trivial filter on $\beta$. For any function $f : \beta \to \alpha$, the filter $l.map(f)$ is Cauchy if and only if there exists a point $x \in \alpha$ such that $f$ tends to $x$ along $l$ (i.e., $\lim_{l} f = x$).

cauchySeq_tendsto_of_complete theorem

[Preorder β] [CompleteSpace α] {u : β → α} (H : CauchySeq u) : ∃ x, Tendsto u atTop (𝓝 x)

Full source

/-- A Cauchy sequence in a complete space converges -/
theorem cauchySeq_tendsto_of_complete [Preorder β] [CompleteSpace α] {u : β → α}
    (H : CauchySeq u) : ∃ x, Tendsto u atTop (𝓝 x) :=
  CompleteSpace.complete H

Convergence of Cauchy Sequences in Complete Uniform Spaces

Informal description

Let $\alpha$ be a complete uniform space and $\beta$ be a preorder. For any Cauchy sequence $u : \beta \to \alpha$, there exists a point $x \in \alpha$ such that $u$ converges to $x$ as the index tends to infinity (i.e., $\lim_{n \to \infty} u(n) = x$).

cauchySeq_tendsto_of_isComplete theorem

 [Preorder β] {K : Set α} (h₁ : IsComplete K) {u : β → α} (h₂ : ∀ n, u n ∈ K) (h₃ : CauchySeq u) :
  ∃ v ∈ K, Tendsto u atTop (𝓝 v)

Full source

/-- If `K` is a complete subset, then any cauchy sequence in `K` converges to a point in `K` -/
theorem cauchySeq_tendsto_of_isComplete [Preorder β] {K : Set α} (h₁ : IsComplete K)
    {u : β → α} (h₂ : ∀ n, u n ∈ K) (h₃ : CauchySeq u) : ∃ v ∈ K, Tendsto u atTop (𝓝 v) :=
  h₁ _ h₃ <| le_principal_iff.2 <| mem_map_iff_exists_image.2
    ⟨univ, univ_mem, by rwa [image_univ, range_subset_iff]⟩

Convergence of Cauchy Sequences in Complete Subsets of Uniform Spaces

Informal description

Let $\alpha$ be a uniform space and $K \subseteq \alpha$ a complete subset. For any Cauchy sequence $u : \beta \to \alpha$ (where $\beta$ is a preorder) such that $u(n) \in K$ for all $n$, there exists a point $v \in K$ such that $u$ converges to $v$ (i.e., $\lim_{n \to \infty} u(n) = v$).

Cauchy.le_nhds_lim theorem

 [CompleteSpace α] {f : Filter α} (hf : Cauchy f) :
  haveI := hf.1.nonempty;
  f ≤ 𝓝 (lim f)

Full source

theorem Cauchy.le_nhds_lim [CompleteSpace α] {f : Filter α} (hf : Cauchy f) :
    haveI := hf.1.nonempty; f ≤ 𝓝 (lim f) :=
  _root_.le_nhds_lim (CompleteSpace.complete hf)

Convergence of Cauchy Filters in Complete Uniform Spaces

Informal description

Let $\alpha$ be a complete uniform space and $f$ a Cauchy filter on $\alpha$. Then $f$ converges to the limit point $\lim f$, i.e., $f \leq \mathcal{N}(\lim f)$, where $\mathcal{N}(x)$ denotes the neighborhood filter of $x$.

CauchySeq.tendsto_limUnder theorem

 [Preorder β] [CompleteSpace α] {u : β → α} (h : CauchySeq u) :
  haveI := h.1.nonempty;
  Tendsto u atTop (𝓝 <| limUnder atTop u)

Full source

theorem CauchySeq.tendsto_limUnder [Preorder β] [CompleteSpace α] {u : β → α} (h : CauchySeq u) :
    haveI := h.1.nonempty; Tendsto u atTop (𝓝 <| limUnder atTop u) :=
  h.le_nhds_lim

Convergence of Cauchy Sequences in Complete Uniform Spaces

Informal description

Let $\alpha$ be a complete uniform space and $\beta$ be a preorder. For any Cauchy sequence $u : \beta \to \alpha$, the sequence converges to its limit under the at-top filter, i.e., $u$ tends to $\lim_{\text{atTop}} u$ in the neighborhood filter of the limit point.

IsClosed.isComplete theorem

[CompleteSpace α] {s : Set α} (h : IsClosed s) : IsComplete s

Full source

theorem IsClosed.isComplete [CompleteSpace α] {s : Set α} (h : IsClosed s) : IsComplete s :=
  fun _ cf fs =>
  let ⟨x, hx⟩ := CompleteSpace.complete cf
  ⟨x, isClosed_iff_clusterPt.mp h x (cf.left.mono (le_inf hx fs)), hx⟩

Closed Subsets of Complete Uniform Spaces are Complete

Informal description

Let $\alpha$ be a complete uniform space and $s$ be a closed subset of $\alpha$. Then $s$ is complete, i.e., every Cauchy filter on $\alpha$ that contains $s$ converges to some point in $s$.

TotallyBounded definition

(s : Set α) : Prop

Full source

/-- A set `s` is totally bounded if for every entourage `d` there is a finite
  set of points `t` such that every element of `s` is `d`-near to some element of `t`. -/
def TotallyBounded (s : Set α) : Prop :=
  ∀ d ∈ 𝓤 α, ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, { x | (x, y) ∈ d }

Totally bounded subset of a uniform space

Informal description

A subset $s$ of a uniform space $\alpha$ is called *totally bounded* if for every entourage $d$ in the uniformity $\mathfrak{U}(\alpha)$, there exists a finite subset $t \subseteq s$ such that every element of $s$ is $d$-close to some element of $t$. In other words, $s$ can be covered by finitely many $d$-balls centered at points in $t$ for any entourage $d$.

TotallyBounded.exists_subset theorem

 {s : Set α} (hs : TotallyBounded s) {U : Set (α × α)} (hU : U ∈ 𝓤 α) :
  ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Full source

theorem TotallyBounded.exists_subset {s : Set α} (hs : TotallyBounded s) {U : Set (α × α)}
    (hU : U ∈ 𝓤 α) : ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, { x | (x, y) ∈ U } := by
  rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩
  rcases hs r hr with ⟨k, fk, ks⟩
  let u := k ∩ { y | ∃ x ∈ s, (x, y) ∈ r }
  choose f hfs hfr using fun x : u => x.coe_prop.2
  refine ⟨range f, ?_, ?_, ?_⟩
  · exact range_subset_iff.2 hfs
  · haveI : Fintype u := (fk.inter_of_left _).fintype
    exact finite_range f
  · intro x xs
    obtain ⟨y, hy, xy⟩ := mem_iUnion₂.1 (ks xs)
    rw [biUnion_range, mem_iUnion]
    set z : ↥u := ⟨y, hy, ⟨x, xs, xy⟩⟩
    exact ⟨z, rU <| mem_compRel.2 ⟨y, xy, rs (hfr z)⟩⟩

Finite Covering Property of Totally Bounded Sets in Uniform Spaces

Informal description

Let $\alpha$ be a uniform space and $s \subseteq \alpha$ a totally bounded subset. For any entourage $U$ in the uniformity $\mathfrak{U}(\alpha)$, there exists a finite subset $t \subseteq s$ such that $s$ is covered by the $U$-neighborhoods of points in $t$, i.e., \[ s \subseteq \bigcup_{y \in t} \{x \mid (x, y) \in U\}. \]

totallyBounded_iff_subset theorem

 {s : Set α} : TotallyBounded s ↔ ∀ d ∈ 𝓤 α, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}

Full source

theorem totallyBounded_iff_subset {s : Set α} :
    TotallyBoundedTotallyBounded s ↔
      ∀ d ∈ 𝓤 α, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, { x | (x, y) ∈ d } :=
  ⟨fun H _ hd ↦ H.exists_subset hd, fun H d hd ↦ let ⟨t, _, ht⟩ := H d hd; ⟨t, ht⟩⟩

Characterization of Totally Bounded Sets via Finite Coverings by Entourage Neighborhoods

Informal description

A subset $s$ of a uniform space $\alpha$ is totally bounded if and only if for every entourage $d$ in the uniformity $\mathfrak{U}(\alpha)$, there exists a finite subset $t \subseteq s$ such that $s$ is covered by the $d$-neighborhoods of points in $t$, i.e., \[ s \subseteq \bigcup_{y \in t} \{x \mid (x, y) \in d\}. \]

Filter.HasBasis.totallyBounded_iff theorem

 {ι} {p : ι → Prop} {U : ι → Set (α × α)} (H : (𝓤 α).HasBasis p U) {s : Set α} :
  TotallyBounded s ↔ ∀ i, p i → ∃ t : Set α, Set.Finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Full source

theorem Filter.HasBasis.totallyBounded_iff {ι} {p : ι → Prop} {U : ι → Set (α × α)}
    (H : (𝓤 α).HasBasis p U) {s : Set α} :
    TotallyBoundedTotallyBounded s ↔ ∀ i, p i → ∃ t : Set α, Set.Finite t ∧ s ⊆ ⋃ y ∈ t, { x | (x, y) ∈ U i } :=
  H.forall_iff fun _ _ hUV h =>
    h.imp fun _ ht => ⟨ht.1, ht.2.trans <| iUnion₂_mono fun _ _ _ hy => hUV hy⟩

Characterization of Totally Bounded Sets via Uniformity Basis

Informal description

Let $\alpha$ be a uniform space with uniformity filter $\mathfrak{U}(\alpha)$. Suppose $\mathfrak{U}(\alpha)$ has a basis $\{U_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then a subset $s \subseteq \alpha$ is totally bounded if and only if for every index $i$ satisfying $p(i)$, there exists a finite subset $t \subseteq \alpha$ such that $s$ is covered by the union of $U_i$-balls centered at points in $t$, i.e., $$ s \subseteq \bigcup_{y \in t} \{x \mid (x, y) \in U_i\}. $$

totallyBounded_of_forall_symm theorem

 {s : Set α} (h : ∀ V ∈ 𝓤 α, IsSymmetricRel V → ∃ t : Set α, Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y V) : TotallyBounded s

Full source

theorem totallyBounded_of_forall_symm {s : Set α}
    (h : ∀ V ∈ 𝓤 α, IsSymmetricRel V → ∃ t : Set α, Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y V) :
    TotallyBounded s :=
  UniformSpace.hasBasis_symmetric.totallyBounded_iff.2 fun V hV => by
    simpa only [ball_eq_of_symmetry hV.2] using h V hV.1 hV.2

Total Boundedness via Symmetric Entourage Coverings

Informal description

A subset $s$ of a uniform space $\alpha$ is totally bounded if for every symmetric entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$, there exists a finite subset $t \subseteq \alpha$ such that $s$ is covered by the union of $V$-balls centered at points in $t$, i.e., $$ s \subseteq \bigcup_{y \in t} \{x \mid (x, y) \in V\}. $$

TotallyBounded.subset theorem

{s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) (h : TotallyBounded s₂) : TotallyBounded s₁

Full source

theorem TotallyBounded.subset {s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) (h : TotallyBounded s₂) :
    TotallyBounded s₁ := fun d hd =>
  let ⟨t, ht₁, ht₂⟩ := h d hd
  ⟨t, ht₁, Subset.trans hs ht₂⟩

Subset of Totally Bounded Set is Totally Bounded

Informal description

For any subsets $s_1$ and $s_2$ of a uniform space $\alpha$, if $s_1$ is a subset of $s_2$ and $s_2$ is totally bounded, then $s_1$ is also totally bounded.

TotallyBounded.closure theorem

{s : Set α} (h : TotallyBounded s) : TotallyBounded (closure s)

Full source

/-- The closure of a totally bounded set is totally bounded. -/
theorem TotallyBounded.closure {s : Set α} (h : TotallyBounded s) : TotallyBounded (closure s) :=
  uniformity_hasBasis_closed.totallyBounded_iff.2 fun V hV =>
    let ⟨t, htf, hst⟩ := h V hV.1
    ⟨t, htf, closure_minimal hst <| htf.isClosed_biUnion fun _ _ => hV.2.preimage (.prodMk_left _)⟩

Closure of Totally Bounded Set is Totally Bounded

Informal description

For any totally bounded subset $s$ of a uniform space $\alpha$, its topological closure $\overline{s}$ is also totally bounded.

totallyBounded_closure theorem

{s : Set α} : TotallyBounded (closure s) ↔ TotallyBounded s

Full source

@[simp]
lemma totallyBounded_closure {s : Set α} : TotallyBoundedTotallyBounded (closure s) ↔ TotallyBounded s :=
  ⟨fun h ↦ h.subset subset_closure, TotallyBounded.closure⟩

Totally Boundedness of Closure $\overline{s}$ iff $s$ is Totally Bounded

Informal description

For any subset $s$ of a uniform space $\alpha$, the closure $\overline{s}$ is totally bounded if and only if $s$ is totally bounded.

totallyBounded_iUnion theorem

{ι : Sort*} [Finite ι] {s : ι → Set α} : TotallyBounded (⋃ i, s i) ↔ ∀ i, TotallyBounded (s i)

Full source

/-- A finite indexed union is totally bounded
if and only if each set of the family is totally bounded. -/
@[simp]
lemma totallyBounded_iUnion {ι : Sort*} [Finite ι] {s : ι → Set α} :
    TotallyBoundedTotallyBounded (⋃ i, s i) ↔ ∀ i, TotallyBounded (s i) := by
  refine ⟨fun h i ↦ h.subset (subset_iUnion _ _), fun h U hU ↦ ?_⟩
  choose t htf ht using (h · U hU)
  refine ⟨⋃ i, t i, finite_iUnion htf, ?_⟩
  rw [biUnion_iUnion]
  gcongr; apply ht

Finite Union is Totally Bounded iff Each Set is Totally Bounded

Informal description

Let $\alpha$ be a uniform space and $\iota$ be a finite index type. For a family of subsets $\{s_i\}_{i \in \iota}$ of $\alpha$, the union $\bigcup_{i \in \iota} s_i$ is totally bounded if and only if each $s_i$ is totally bounded.

totallyBounded_biUnion theorem

 {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set α} : TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

Full source

/-- A union indexed by a finite set is totally bounded
if and only if each set of the family is totally bounded. -/
lemma totallyBounded_biUnion {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set α} :
    TotallyBoundedTotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i) := by
  have := hI.to_subtype
  rw [biUnion_eq_iUnion, totallyBounded_iUnion, Subtype.forall]

Finite Bounded Union is Totally Bounded iff Each Member is Totally Bounded

Informal description

Let $\alpha$ be a uniform space, $\iota$ be a type, and $I \subseteq \iota$ be a finite subset. For a family of subsets $\{s_i\}_{i \in \iota}$ of $\alpha$, the union $\bigcup_{i \in I} s_i$ is totally bounded if and only if each $s_i$ is totally bounded for all $i \in I$.

totallyBounded_sUnion theorem

{S : Set (Set α)} (hS : S.Finite) : TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

Full source

/-- A union of a finite family of sets is totally bounded
if and only if each set of the family is totally bounded. -/
lemma totallyBounded_sUnion {S : Set (Set α)} (hS : S.Finite) :
    TotallyBoundedTotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s := by
  rw [sUnion_eq_biUnion, totallyBounded_biUnion hS]

Finite Union is Totally Bounded iff All Members Are Totally Bounded

Informal description

Let $\alpha$ be a uniform space and $S$ be a finite collection of subsets of $\alpha$. The union $\bigcup_{s \in S} s$ is totally bounded if and only if every subset $s \in S$ is totally bounded.

Set.Finite.totallyBounded theorem

{s : Set α} (hs : s.Finite) : TotallyBounded s

Full source

/-- A finite set is totally bounded. -/
lemma Set.Finite.totallyBounded {s : Set α} (hs : s.Finite) : TotallyBounded s := fun _U hU ↦
  ⟨s, hs, fun _x hx ↦ mem_biUnion hx <| refl_mem_uniformity hU⟩

Finite subsets are totally bounded in uniform spaces

Informal description

For any finite subset $s$ of a uniform space $\alpha$, the set $s$ is totally bounded.

Set.Subsingleton.totallyBounded theorem

{s : Set α} (hs : s.Subsingleton) : TotallyBounded s

Full source

/-- A subsingleton is totally bounded. -/
lemma Set.Subsingleton.totallyBounded {s : Set α} (hs : s.Subsingleton) :
    TotallyBounded s :=
  hs.finite.totallyBounded

Total Boundedness of Subsingleton Sets in Uniform Spaces

Informal description

For any subsingleton subset $s$ of a uniform space $\alpha$, the set $s$ is totally bounded.

totallyBounded_singleton theorem

(a : α) : TotallyBounded { a }

Full source

@[simp]
lemma totallyBounded_singleton (a : α) : TotallyBounded {a} := (finite_singleton a).totallyBounded

Total Boundedness of Singleton Sets in Uniform Spaces

Informal description

For any element $a$ in a uniform space $\alpha$, the singleton set $\{a\}$ is totally bounded.

totallyBounded_empty theorem

: TotallyBounded (∅ : Set α)

Full source

@[simp]
theorem totallyBounded_empty : TotallyBounded (∅ : Set α) := finite_empty.totallyBounded

Total Boundedness of the Empty Set

Informal description

The empty set $\emptyset$ in a uniform space $\alpha$ is totally bounded.

totallyBounded_union theorem

{s t : Set α} : TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

Full source

/-- The union of two sets is totally bounded
if and only if each of the two sets is totally bounded. -/
@[simp]
lemma totallyBounded_union {s t : Set α} :
    TotallyBoundedTotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t := by
  rw [union_eq_iUnion, totallyBounded_iUnion]
  simp [and_comm]

Union is Totally Bounded iff Both Sets Are Totally Bounded

Informal description

For any two subsets $s$ and $t$ of a uniform space $\alpha$, the union $s \cup t$ is totally bounded if and only if both $s$ and $t$ are totally bounded.

TotallyBounded.union theorem

{s t : Set α} (hs : TotallyBounded s) (ht : TotallyBounded t) : TotallyBounded (s ∪ t)

Full source

/-- The union of two totally bounded sets is totally bounded. -/
protected lemma TotallyBounded.union {s t : Set α} (hs : TotallyBounded s) (ht : TotallyBounded t) :
    TotallyBounded (s ∪ t) :=
  totallyBounded_union.2 ⟨hs, ht⟩

Union of Totally Bounded Sets is Totally Bounded

Informal description

Let $s$ and $t$ be subsets of a uniform space $\alpha$. If both $s$ and $t$ are totally bounded, then their union $s \cup t$ is also totally bounded.

totallyBounded_insert theorem

(a : α) {s : Set α} : TotallyBounded (insert a s) ↔ TotallyBounded s

Full source

@[simp]
lemma totallyBounded_insert (a : α) {s : Set α} :
    TotallyBoundedTotallyBounded (insert a s) ↔ TotallyBounded s := by
  simp_rw [← singleton_union, totallyBounded_union, totallyBounded_singleton, true_and]

Total Boundedness of Insertion of a Point into a Set

Informal description

For any element $a$ in a uniform space $\alpha$ and any subset $s \subseteq \alpha$, the set $\{a\} \cup s$ is totally bounded if and only if $s$ is totally bounded.

TotallyBounded.image theorem

 [UniformSpace β] {f : α → β} {s : Set α} (hs : TotallyBounded s) (hf : UniformContinuous f) : TotallyBounded (f '' s)

Full source

/-- The image of a totally bounded set under a uniformly continuous map is totally bounded. -/
theorem TotallyBounded.image [UniformSpace β] {f : α → β} {s : Set α} (hs : TotallyBounded s)
    (hf : UniformContinuous f) : TotallyBounded (f '' s) := fun t ht =>
  have : { p : α × α | (f p.1, f p.2) ∈ t }{ p : α × α | (f p.1, f p.2) ∈ t } ∈ 𝓤 α := hf ht
  let ⟨c, hfc, hct⟩ := hs _ this
  ⟨f '' c, hfc.image f, by
    simp only [mem_image, iUnion_exists, biUnion_and', iUnion_iUnion_eq_right, image_subset_iff,
      preimage_iUnion, preimage_setOf_eq]
    simp? [subset_def] at hct says
      simp only [mem_setOf_eq, subset_def, mem_iUnion, exists_prop] at hct
    intro x hx
    simpa using hct x hx⟩

Uniformly Continuous Image of a Totally Bounded Set is Totally Bounded

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $f \colon \alpha \to \beta$ a uniformly continuous function, and $s \subseteq \alpha$ a totally bounded subset. Then the image $f(s) \subseteq \beta$ is totally bounded.

Ultrafilter.cauchy_of_totallyBounded theorem

{s : Set α} (f : Ultrafilter α) (hs : TotallyBounded s) (h : ↑f ≤ 𝓟 s) : Cauchy (f : Filter α)

Full source

theorem Ultrafilter.cauchy_of_totallyBounded {s : Set α} (f : Ultrafilter α) (hs : TotallyBounded s)
    (h : ↑f ≤ 𝓟 s) : Cauchy (f : Filter α) :=
  ⟨f.neBot', fun _ ht =>
    let ⟨t', ht'₁, ht'_symm, ht'_t⟩ := comp_symm_of_uniformity ht
    let ⟨i, hi, hs_union⟩ := hs t' ht'₁
    have : (⋃ y ∈ i, { x | (x, y) ∈ t' }) ∈ f := mem_of_superset (le_principal_iff.mp h) hs_union
    have : ∃ y ∈ i, { x | (x, y) ∈ t' } ∈ f := (Ultrafilter.finite_biUnion_mem_iff hi).1 this
    let ⟨y, _, hif⟩ := this
    have : { x | (x, y) ∈ t' } ×ˢ { x | (x, y) ∈ t' } ⊆ compRel t' t' :=
      fun ⟨_, _⟩ ⟨(h₁ : (_, y) ∈ t'), (h₂ : (_, y) ∈ t')⟩ => ⟨y, h₁, ht'_symm h₂⟩
    mem_of_superset (prod_mem_prod hif hif) (Subset.trans this ht'_t)⟩

Ultrafilter on a Totally Bounded Set is Cauchy

Informal description

Let $\alpha$ be a uniform space, $s \subseteq \alpha$ a totally bounded subset, and $f$ an ultrafilter on $\alpha$ such that $f$ contains the principal filter generated by $s$. Then $f$ is a Cauchy filter.

totallyBounded_iff_filter theorem

{s : Set α} : TotallyBounded s ↔ ∀ f, NeBot f → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c

Full source

theorem totallyBounded_iff_filter {s : Set α} :
    TotallyBoundedTotallyBounded s ↔ ∀ f, NeBot f → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c := by
  constructor
  · exact fun H f hf hfs => ⟨Ultrafilter.of f, Ultrafilter.of_le f,
      (Ultrafilter.of f).cauchy_of_totallyBounded H ((Ultrafilter.of_le f).trans hfs)⟩
  · intro H d hd
    contrapose! H with hd_cover
    set f := ⨅ t : Finset α, 𝓟 (s \ ⋃ y ∈ t, { x | (x, y) ∈ d })
    have hb : HasAntitoneBasis f fun t : Finset α ↦ s \ ⋃ y ∈ t, { x | (x, y) ∈ d } :=
      .iInf_principal fun _ _ ↦ diff_subset_diff_rightdiff_subset_diff_right ∘ biUnion_subset_biUnion_left
    have : Filter.NeBot f := hb.1.neBot_iff.2 fun _ ↦
      diff_nonempty.2 <| hd_cover _ (Finset.finite_toSet _)
    have : f ≤ 𝓟 s := iInf_le_of_le ∅ (by simp)
    refine ⟨f, ‹_›, ‹_›, fun c hcf hc => ?_⟩
    rcases mem_prod_same_iff.1 (hc.2 hd) with ⟨m, hm, hmd⟩
    rcases hc.1.nonempty_of_mem hm with ⟨y, hym⟩
    have : s \ {x | (x, y) ∈ d}s \ {x | (x, y) ∈ d} ∈ c := by simpa using hcf (hb.mem {y})
    rcases hc.1.nonempty_of_mem (inter_mem hm this) with ⟨z, hzm, -, hyz⟩
    exact hyz (hmd ⟨hzm, hym⟩)

Characterization of Totally Bounded Sets via Filters: $s$ is totally bounded iff every non-trivial filter containing $s$ has a Cauchy refinement

Informal description

A subset $s$ of a uniform space $\alpha$ is totally bounded if and only if for every non-trivial filter $f$ on $\alpha$ that contains the principal filter generated by $s$, there exists a Cauchy filter $c$ such that $c \leq f$.

totallyBounded_iff_ultrafilter theorem

{s : Set α} : TotallyBounded s ↔ ∀ f : Ultrafilter α, ↑f ≤ 𝓟 s → Cauchy (f : Filter α)

Full source

theorem totallyBounded_iff_ultrafilter {s : Set α} :
    TotallyBoundedTotallyBounded s ↔ ∀ f : Ultrafilter α, ↑f ≤ 𝓟 s → Cauchy (f : Filter α) := by
  refine ⟨fun hs f => f.cauchy_of_totallyBounded hs, fun H => totallyBounded_iff_filter.2 ?_⟩
  intro f hf hfs
  exact ⟨Ultrafilter.of f, Ultrafilter.of_le f, H _ ((Ultrafilter.of_le f).trans hfs)⟩

Characterization of Totally Bounded Sets via Ultrafilters: $s$ is totally bounded iff all ultrafilters containing $s$ are Cauchy

Informal description

A subset $s$ of a uniform space $\alpha$ is totally bounded if and only if every ultrafilter $f$ on $\alpha$ containing the principal filter generated by $s$ is a Cauchy filter.

isCompact_iff_totallyBounded_isComplete theorem

{s : Set α} : IsCompact s ↔ TotallyBounded s ∧ IsComplete s

Full source

theorem isCompact_iff_totallyBounded_isComplete {s : Set α} :
    IsCompactIsCompact s ↔ TotallyBounded s ∧ IsComplete s :=
  ⟨fun hs =>
    ⟨totallyBounded_iff_ultrafilter.2 fun f hf =>
        let ⟨_, _, fx⟩ := isCompact_iff_ultrafilter_le_nhds.1 hs f hf
        cauchy_nhds.mono fx,
      fun f fc fs =>
      let ⟨a, as, fa⟩ := @hs f fc.1 fs
      ⟨a, as, le_nhds_of_cauchy_adhp fc fa⟩⟩,
    fun ⟨ht, hc⟩ =>
    isCompact_iff_ultrafilter_le_nhds.2 fun f hf =>
      hc _ (totallyBounded_iff_ultrafilter.1 ht f hf) hf⟩

Compactness Characterization via Total Boundedness and Completeness in Uniform Spaces

Informal description

A subset $s$ of a uniform space $\alpha$ is compact if and only if it is totally bounded and complete.

IsCompact.totallyBounded theorem

{s : Set α} (h : IsCompact s) : TotallyBounded s

Full source

protected theorem IsCompact.totallyBounded {s : Set α} (h : IsCompact s) : TotallyBounded s :=
  (isCompact_iff_totallyBounded_isComplete.1 h).1

Compact subsets are totally bounded in uniform spaces

Informal description

For any subset $s$ of a uniform space $\alpha$, if $s$ is compact, then $s$ is totally bounded.

IsCompact.isComplete theorem

{s : Set α} (h : IsCompact s) : IsComplete s

Full source

protected theorem IsCompact.isComplete {s : Set α} (h : IsCompact s) : IsComplete s :=
  (isCompact_iff_totallyBounded_isComplete.1 h).2

Compact subsets are complete in uniform spaces

Informal description

For any subset $s$ of a uniform space $\alpha$, if $s$ is compact, then $s$ is complete. That is, every Cauchy filter on $\alpha$ containing $s$ converges to some point in $s$.

complete_of_compact instance

{α : Type u} [UniformSpace α] [CompactSpace α] : CompleteSpace α

Full source

instance (priority := 100) complete_of_compact {α : Type u} [UniformSpace α] [CompactSpace α] :
    CompleteSpace α :=
  ⟨fun hf => by simpa using (isCompact_iff_totallyBounded_isComplete.1 isCompact_univ).2 _ hf⟩

Compact Uniform Spaces are Complete

Informal description

Every compact uniform space is complete. That is, if a uniform space $\alpha$ is compact, then every Cauchy filter on $\alpha$ converges to some point in $\alpha$.

isCompact_of_totallyBounded_isClosed theorem

[CompleteSpace α] {s : Set α} (ht : TotallyBounded s) (hc : IsClosed s) : IsCompact s

Full source

theorem isCompact_of_totallyBounded_isClosed [CompleteSpace α] {s : Set α} (ht : TotallyBounded s)
    (hc : IsClosed s) : IsCompact s :=
  (@isCompact_iff_totallyBounded_isComplete α _ s).2 ⟨ht, hc.isComplete⟩

Compactness via Total Boundedness and Closedness in Complete Uniform Spaces

Informal description

Let $\alpha$ be a complete uniform space and $s$ be a subset of $\alpha$. If $s$ is totally bounded and closed, then $s$ is compact.

CauchySeq.totallyBounded_range theorem

{s : ℕ → α} (hs : CauchySeq s) : TotallyBounded (range s)

Full source

/-- Every Cauchy sequence over `ℕ` is totally bounded. -/
theorem CauchySeq.totallyBounded_range {s : ℕ → α} (hs : CauchySeq s) :
    TotallyBounded (range s) := by
  intro a ha
  obtain ⟨n, hn⟩ := cauchySeq_iff.1 hs a ha
  refine ⟨s '' { k | k ≤ n }, (finite_le_nat _).image _, ?_⟩
  rw [range_subset_iff, biUnion_image]
  intro m
  rw [mem_iUnion₂]
  rcases le_total m n with hm | hm
  exacts [⟨m, hm, refl_mem_uniformity ha⟩, ⟨n, le_refl n, hn m hm n le_rfl⟩]

Total Boundedness of the Range of a Cauchy Sequence in a Uniform Space

Informal description

For any Cauchy sequence $s : \mathbb{N} \to \alpha$ in a uniform space $\alpha$, the range of $s$ is totally bounded. That is, for every entourage $V$ in the uniformity of $\alpha$, there exists a finite subset $t \subseteq \text{range}(s)$ such that every element in the range of $s$ is $V$-close to some element of $t$.

interUnionBalls definition

(xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α

Full source

/-- Given a family of points `xs n`, a family of entourages `V n` of the diagonal and a family of
natural numbers `u n`, the intersection over `n` of the `V n`-neighborhood of `xs 1, ..., xs (u n)`.
Designed to be relatively compact when `V n` tends to the diagonal. -/
def interUnionBalls (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α :=
  ⋂ n, ⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)

Intersection of unions of uniform balls indexed by entourages

Informal description

Given a sequence of points $ (x_n)_{n \in \mathbb{N}} $ in a uniform space $ \alpha $, a sequence of natural numbers $ (u_n)_{n \in \mathbb{N}} $, and a sequence of entourages $ (V_n)_{n \in \mathbb{N}} $ of the diagonal, the set $ \bigcap_{n \in \mathbb{N}} \bigcup_{m \leq u_n} B_{V_n}(x_m) $ consists of all points $ y \in \alpha $ such that for every $ n $, there exists $ m \leq u_n $ with $ (x_m, y) \in V_n $. Here, $ B_{V_n}(x_m) $ denotes the $ V_n $-ball centered at $ x_m $.

totallyBounded_interUnionBalls theorem

 {p : ℕ → Prop} {U : ℕ → Set (α × α)} (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
  TotallyBounded (interUnionBalls xs u U)

Full source

lemma totallyBounded_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
    (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
    TotallyBounded (interUnionBalls xs u U) := by
  rw [Filter.HasBasis.totallyBounded_iff H]
  intro i _
  have h_subset : interUnionBallsinterUnionBalls xs u U
      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
    fun x hx ↦ Set.mem_iInter.1 hx i
  classical
  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
  exact h_subset hx

Total Boundedness of the Intersection of Unions of Uniform Balls

Informal description

Let $\alpha$ be a uniform space with a basis $\{U_n\}_{n \in \mathbb{N}}$ for its uniformity filter, indexed by natural numbers with a predicate $p$. Given a sequence of points $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ and a sequence of natural numbers $(u_n)_{n \in \mathbb{N}}$, the set $\bigcap_{n \in \mathbb{N}} \bigcup_{m \leq u_n} B_{U_n}(x_m)$ is totally bounded. Here, $B_{U_n}(x_m)$ denotes the $U_n$-ball centered at $x_m$.

isCompact_closure_interUnionBalls theorem

 {p : ℕ → Prop} {U : ℕ → Set (α × α)} (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
  IsCompact (closure (interUnionBalls xs u U))

Full source

/-- The construction `interUnionBalls` is used to have a relatively compact set. -/
theorem isCompact_closure_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
    (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
    IsCompact (closure (interUnionBalls xs u U)) := by
  rw [isCompact_iff_totallyBounded_isComplete]
  refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
  exact totallyBounded_interUnionBalls H xs u

Compactness of the Closure of Intersection of Unions of Uniform Balls in Complete Uniform Spaces

Informal description

Let $\alpha$ be a complete uniform space with a basis $\{U_n\}_{n \in \mathbb{N}}$ for its uniformity filter, indexed by natural numbers with a predicate $p$. Given a sequence of points $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ and a sequence of natural numbers $(u_n)_{n \in \mathbb{N}}$, the topological closure of the set $\bigcap_{n \in \mathbb{N}} \bigcup_{m \leq u_n} B_{U_n}(x_m)$ is compact. Here, $B_{U_n}(x_m)$ denotes the $U_n$-ball centered at $x_m$.

SequentiallyComplete.setSeqAux definition

(n : ℕ) : { s : Set α // s ∈ f ∧ s ×ˢ s ⊆ U n }

Full source

/-- An auxiliary sequence of sets approximating a Cauchy filter. -/
def setSeqAux (n : ℕ) : { s : Set α // s ∈ f ∧ s ×ˢ s ⊆ U n } :=
  Classical.indefiniteDescription _ <| (cauchy_iff.1 hf).2 (U n) (U_mem n)

Auxiliary sequence of sets approximating a Cauchy filter

Informal description

For a given natural number $ n $, the function `setSeqAux` selects a set $ s $ from a Cauchy filter $ f $ on a uniform space $ \alpha $ such that $ s $ is in $ f $ and the Cartesian product $ s \times s $ is contained in the entourage $ U_n $ from a given sequence of entourages $ (U_n) $ generating the uniformity.

SequentiallyComplete.setSeq definition

(n : ℕ) : Set α

Full source

/-- Given a Cauchy filter `f` and a sequence `U` of entourages, `set_seq` provides
an antitone sequence of sets `s n ∈ f` such that `s n ×ˢ s n ⊆ U`. -/
def setSeq (n : ℕ) : Set α :=
  ⋂ m ∈ Set.Iic n, (setSeqAux hf U_mem m).val

Antitone sequence of sets approximating a Cauchy filter

Informal description

Given a Cauchy filter $ f $ on a uniform space $ \alpha $ and a sequence of entourages $ (U_n) $ generating the uniformity, the function `setSeq` constructs an antitone sequence of sets $ (s_n) $ where each $ s_n $ is the intersection of the auxiliary sets $ \text{setSeqAux } m $ for all $ m \leq n $. Each $ s_n $ satisfies $ s_n \in f $ and $ s_n \times s_n \subseteq U_n $.

SequentiallyComplete.setSeq_mem theorem

(n : ℕ) : setSeq hf U_mem n ∈ f

Full source

theorem setSeq_mem (n : ℕ) : setSeqsetSeq hf U_mem n ∈ f :=
  (biInter_mem (finite_le_nat n)).2 fun m _ => (setSeqAux hf U_mem m).2.1

Membership of Approximating Sets in Cauchy Filter

Informal description

For any natural number $n$, the set $\text{setSeq}(n)$ constructed from a Cauchy filter $f$ and a sequence of entourages $(U_n)$ belongs to $f$.

SequentiallyComplete.setSeq_mono theorem

⦃m n : ℕ⦄ (h : m ≤ n) : setSeq hf U_mem n ⊆ setSeq hf U_mem m

Full source

theorem setSeq_mono ⦃m n : ℕ⦄ (h : m ≤ n) : setSeqsetSeq hf U_mem n ⊆ setSeq hf U_mem m :=
  biInter_subset_biInter_left <| Iic_subset_Iic.2 h

Monotonicity of the Approximating Sequence for a Cauchy Filter

Informal description

For any natural numbers $m$ and $n$ with $m \leq n$, the set $\text{setSeq}(n)$ is a subset of $\text{setSeq}(m)$, where $\text{setSeq}$ is an antitone sequence of sets approximating a Cauchy filter in a uniform space.

SequentiallyComplete.setSeq_sub_aux theorem

(n : ℕ) : setSeq hf U_mem n ⊆ setSeqAux hf U_mem n

Full source

theorem setSeq_sub_aux (n : ℕ) : setSeqsetSeq hf U_mem n ⊆ setSeqAux hf U_mem n :=
  biInter_subset_of_mem right_mem_Iic

Subset Relation between $\text{setSeq}(n)$ and $\text{setSeqAux}(n)$ in a Sequentially Complete Uniform Space

Informal description

For any natural number $n$, the set $\text{setSeq}(n)$ is a subset of the auxiliary set $\text{setSeqAux}(n)$, where both sets are constructed from a Cauchy filter $f$ and a sequence of entourages $(U_n)$ generating the uniformity of a uniform space $\alpha$.

SequentiallyComplete.setSeq_prod_subset theorem

{N m n} (hm : N ≤ m) (hn : N ≤ n) : setSeq hf U_mem m ×ˢ setSeq hf U_mem n ⊆ U N

Full source

theorem setSeq_prod_subset {N m n} (hm : N ≤ m) (hn : N ≤ n) :
    setSeqsetSeq hf U_mem m ×ˢ setSeq hf U_mem n ⊆ U N := fun p hp => by
  refine (setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩ <;> apply setSeq_sub_aux
  · exact setSeq_mono hf U_mem hm hp.1
  · exact setSeq_mono hf U_mem hn hp.2

Product of Approximating Sets in Cauchy Filter is Contained in Entourage

Informal description

For any natural numbers $N$, $m$, and $n$ such that $N \leq m$ and $N \leq n$, the Cartesian product of the sets $\text{setSeq}(m)$ and $\text{setSeq}(n)$ is contained in the entourage $U_N$. Here, $\text{setSeq}$ is an antitone sequence of sets approximating a Cauchy filter $f$ in a uniform space $\alpha$, and $(U_n)$ is a sequence of entourages generating the uniformity of $\alpha$.

SequentiallyComplete.seq definition

(n : ℕ) : α

Full source

/-- A sequence of points such that `seq n ∈ setSeq n`. Here `setSeq` is an antitone
sequence of sets `setSeq n ∈ f` with diameters controlled by a given sequence
of entourages. -/
def seq (n : ℕ) : α :=
  (hf.1.nonempty_of_mem (setSeq_mem hf U_mem n)).choose

Cauchy sequence approximating a Cauchy filter

Informal description

Given a Cauchy filter $ f $ on a uniform space $ \alpha $ and a sequence of entourages $ (U_n) $ generating the uniformity, the sequence $ \text{seq} $ is constructed such that for each $ n $, the $ n $-th term $ \text{seq } n $ belongs to the $ n $-th set $ \text{setSeq } n $ in the antitone sequence approximating $ f $. This sequence is chosen to satisfy the condition that for any $ N $, if $ m, n \geq N $, then the pair $ (\text{seq } m, \text{seq } n) $ belongs to the entourage $ U_N $, ensuring it is a Cauchy sequence with respect to the uniformity.

SequentiallyComplete.seq_mem theorem

(n : ℕ) : seq hf U_mem n ∈ setSeq hf U_mem n

Full source

theorem seq_mem (n : ℕ) : seqseq hf U_mem n ∈ setSeq hf U_mem n :=
  (hf.1.nonempty_of_mem (setSeq_mem hf U_mem n)).choose_spec

Membership of Sequence Terms in Approximating Sets

Informal description

For any natural number $n$, the $n$-th term of the Cauchy sequence $\text{seq}$ constructed from a Cauchy filter $f$ and a sequence of entourages $(U_n)$ belongs to the $n$-th approximating set $\text{setSeq}(n)$.

SequentiallyComplete.seq_pair_mem theorem

⦃N m n : ℕ⦄ (hm : N ≤ m) (hn : N ≤ n) : (seq hf U_mem m, seq hf U_mem n) ∈ U N

Full source

theorem seq_pair_mem ⦃N m n : ℕ⦄ (hm : N ≤ m) (hn : N ≤ n) :
    (seq hf U_mem m, seq hf U_mem n)(seq hf U_mem m, seq hf U_mem n) ∈ U N :=
  setSeq_prod_subset hf U_mem hm hn ⟨seq_mem hf U_mem m, seq_mem hf U_mem n⟩

Cauchy Sequence Pairs Belong to Corresponding Entourages

Informal description

For any natural numbers $N$, $m$, and $n$ such that $N \leq m$ and $N \leq n$, the pair $(x_m, x_n)$ belongs to the entourage $U_N$, where $(x_k)$ is the Cauchy sequence constructed from the Cauchy filter $f$ and the sequence of entourages $(U_k)$.

SequentiallyComplete.seq_is_cauchySeq theorem

(U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s) : CauchySeq <| seq hf U_mem

Full source

theorem seq_is_cauchySeq (U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s) : CauchySeq <| seq hf U_mem :=
  cauchySeq_of_controlled U U_le <| seq_pair_mem hf U_mem

Constructed Sequence from Cauchy Filter is Cauchy

Informal description

Let $\alpha$ be a uniform space with a sequence of entourages $(U_n)$ such that for any entourage $s$ in the uniformity $\mathfrak{U}(\alpha)$, there exists $n$ with $U_n \subseteq s$. Given a Cauchy filter $f$ on $\alpha$, the sequence $\text{seq}$ constructed from $f$ and $(U_n)$ is a Cauchy sequence.

SequentiallyComplete.le_nhds_of_seq_tendsto_nhds theorem

(U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s) ⦃a : α⦄ (ha : Tendsto (seq hf U_mem) atTop (𝓝 a)) : f ≤ 𝓝 a

Full source

/-- If the sequence `SequentiallyComplete.seq` converges to `a`, then `f ≤ 𝓝 a`. -/
theorem le_nhds_of_seq_tendsto_nhds (U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s)
    ⦃a : α⦄ (ha : Tendsto (seq hf U_mem) atTop (𝓝 a)) : f ≤ 𝓝 a :=
  le_nhds_of_cauchy_adhp_aux
    (fun s hs => by
      rcases U_le s hs with ⟨m, hm⟩
      rcases tendsto_atTop'.1 ha _ (mem_nhds_left a (U_mem m)) with ⟨n, hn⟩
      refine
        ⟨setSeq hf U_mem (max m n), setSeq_mem hf U_mem _, ?_, seq hf U_mem (max m n), ?_,
          seq_mem hf U_mem _⟩
      · have := le_max_left m n
        exact Set.Subset.trans (setSeq_prod_subset hf U_mem this this) hm
      · exact hm (hn _ <| le_max_right m n))

Convergence of Cauchy Filter via Associated Cauchy Sequence

Informal description

Let $\alpha$ be a uniform space with a sequence of entourages $(U_n)$ such that for any entourage $s \in \mathfrak{U}(\alpha)$, there exists $n$ with $U_n \subseteq s$. Let $f$ be a Cauchy filter on $\alpha$ and let $\text{seq}$ be the associated Cauchy sequence constructed from $f$ and $(U_n)$. If $\text{seq}$ converges to a point $a \in \alpha$, then the filter $f$ converges to $a$.

UniformSpace.complete_of_convergent_controlled_sequences theorem

 (U : ℕ → Set (α × α)) (U_mem : ∀ n, U n ∈ 𝓤 α)
  (HU : ∀ u : ℕ → α, (∀ N m n, N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)) : CompleteSpace α

Full source

/-- A uniform space is complete provided that (a) its uniformity filter has a countable basis;
(b) any sequence satisfying a "controlled" version of the Cauchy condition converges. -/
theorem complete_of_convergent_controlled_sequences (U : ℕ → Set (α × α)) (U_mem : ∀ n, U n ∈ 𝓤 α)
    (HU : ∀ u : ℕ → α, (∀ N m n, N ≤ m → N ≤ n → (u m, u n)(u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)) :
    CompleteSpace α := by
  obtain ⟨U', -, hU'⟩ := (𝓤 α).exists_antitone_seq
  have Hmem : ∀ n, U n ∩ U' nU n ∩ U' n ∈ 𝓤 α := fun n => inter_mem (U_mem n) (hU'.2 ⟨n, Subset.refl _⟩)
  refine ⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <|
    le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩
  · exact inter_subset_left (seq_pair_mem hf Hmem hm hn)
  · rcases hU'.1 hs with ⟨N, hN⟩
    exact ⟨N, Subset.trans inter_subset_right hN⟩

Completeness via Controlled Cauchy Sequences in Uniform Spaces

Informal description

Let $\alpha$ be a uniform space equipped with a sequence of entourages $(U_n)_{n \in \mathbb{N}}$ such that each $U_n$ belongs to the uniformity $\mathfrak{U}(\alpha)$. Suppose that every sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ satisfying the controlled Cauchy condition \[ \forall N\ m\ n,\ N \leq m \land N \leq n \implies (u_m, u_n) \in U_N \] converges to some point in $\alpha$. Then $\alpha$ is a complete uniform space.

UniformSpace.complete_of_cauchySeq_tendsto theorem

(H' : ∀ u : ℕ → α, CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)) : CompleteSpace α

Full source

/-- A sequentially complete uniform space with a countable basis of the uniformity filter is
complete. -/
theorem complete_of_cauchySeq_tendsto (H' : ∀ u : ℕ → α, CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)) :
    CompleteSpace α :=
  let ⟨U', _, hU'⟩ := (𝓤 α).exists_antitone_seq
  complete_of_convergent_controlled_sequences U' (fun n => hU'.2 ⟨n, Subset.refl _⟩) fun u hu =>
    H' u <| cauchySeq_of_controlled U' (fun _ hs => hU'.1 hs) hu

Completeness via convergent Cauchy sequences in uniform spaces

Informal description

A uniform space $\alpha$ is complete if every Cauchy sequence in $\alpha$ converges to some point in $\alpha$.

UniformSpace.firstCountableTopology instance

: FirstCountableTopology α

Full source

instance (priority := 100) firstCountableTopology : FirstCountableTopology α :=
  ⟨fun a => by rw [nhds_eq_comap_uniformity]; infer_instance⟩

First-Countability of Uniform Spaces

Informal description

Every uniform space $\alpha$ has a first-countable topology, meaning that every point has a countable neighborhood basis.

UniformSpace.secondCountable_of_separable theorem

[SeparableSpace α] : SecondCountableTopology α

Full source

/-- A separable uniform space with countably generated uniformity filter is second countable:
one obtains a countable basis by taking the balls centered at points in a dense subset,
and with rational "radii" from a countable open symmetric antitone basis of `𝓤 α`. We do not
register this as an instance, as there is already an instance going in the other direction
from second countable spaces to separable spaces, and we want to avoid loops. -/
theorem secondCountable_of_separable [SeparableSpace α] : SecondCountableTopology α := by
  rcases exists_countable_dense α with ⟨s, hsc, hsd⟩
  obtain
    ⟨t : ℕ → Set (α × α), hto : ∀ i : ℕ, t i ∈ (𝓤 α).setst i ∈ (𝓤 α).sets ∧ IsOpen (t i) ∧ IsSymmetricRel (t i),
      h_basis : (𝓤 α).HasAntitoneBasis t⟩ :=
    (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
  choose ht_mem hto hts using hto
  refine ⟨⟨⋃ x ∈ s, range fun k => ball x (t k), hsc.biUnion fun x _ => countable_range _, ?_⟩⟩
  refine (isTopologicalBasis_of_isOpen_of_nhds ?_ ?_).eq_generateFrom
  · simp only [mem_iUnion₂, mem_range]
    rintro _ ⟨x, _, k, rfl⟩
    exact isOpen_ball x (hto k)
  · intro x V hxV hVo
    simp only [mem_iUnion₂, mem_range, exists_prop]
    rcases UniformSpace.mem_nhds_iff.1 (IsOpen.mem_nhds hVo hxV) with ⟨U, hU, hUV⟩
    rcases comp_symm_of_uniformity hU with ⟨U', hU', _, hUU'⟩
    rcases h_basis.toHasBasis.mem_iff.1 hU' with ⟨k, -, hk⟩
    rcases hsd.inter_open_nonempty (ball x <| t k) (isOpen_ball x (hto k))
        ⟨x, UniformSpace.mem_ball_self _ (ht_mem k)⟩ with
      ⟨y, hxy, hys⟩
    refine ⟨_, ⟨y, hys, k, rfl⟩, (hts k).subset hxy, fun z hz => ?_⟩
    exact hUV (ball_subset_of_comp_subset (hk hxy) hUU' (hk hz))

Second-Countability of Separable Uniform Spaces

Informal description

Every separable uniform space $\alpha$ is second-countable. That is, if $\alpha$ has a countable dense subset, then its topology admits a countable basis.