# Theory of Cauchy filters in uniform spaces. Complete uniform spaces. Totally bounded subsets. #

source
def Cauchy {α : Type u} [uniformSpace : UniformSpace α] (f : Filter α) :
Prop

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.

Equations

- Cauchy f = (f.NeBot ∧ f ×ˢ f ≤ uniformity α)

Instances For

source
def IsComplete {α : Type u} [uniformSpace : UniformSpace α] (s : Set α) :
Prop

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`).

Equations

- IsComplete s = ∀ (f : Filter α), Cauchy f → f ≤ Filter.principal s → ∃ x ∈ s, f ≤ nhds x

Instances For

source
theorem Filter.HasBasis.cauchy_iff {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → SetRel α α} (h : (uniformity α).HasBasis p s) {f : Filter α} :
Cauchy f ↔ f.NeBot ∧ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i
source
theorem cauchy_iff' {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} :
Cauchy f ↔ f.NeBot ∧ ∀ s ∈ uniformity α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s
source
theorem cauchy_iff {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} :
Cauchy f ↔ f.NeBot ∧ ∀ s ∈ uniformity α, ∃ t ∈ f, t ×ˢ t ⊆ s
source
theorem cauchy_iff_le {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} [hl : l.NeBot] :
Cauchy l ↔ l ×ˢ l ≤ uniformity α
source
theorem Cauchy.ultrafilter_of {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} (h : Cauchy l) :
Cauchy ↑(Ultrafilter.of l)
source
theorem cauchy_map_iff {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} {f : β → α} :
Cauchy (Filter.map f l) ↔ l.NeBot ∧ Filter.Tendsto (fun (p : β × β) => (f p.1, f p.2)) (l ×ˢ l) (uniformity α)
source
theorem cauchy_map_iff' {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [hl : l.NeBot] {f : β → α} :
Cauchy (Filter.map f l) ↔ Filter.Tendsto (fun (p : β × β) => (f p.1, f p.2)) (l ×ˢ l) (uniformity α)
source
theorem Cauchy.mono {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α} [hg : g.NeBot] (h_c : Cauchy f) (h_le : g ≤ f) :
Cauchy g
source
theorem Cauchy.mono' {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α} (h_c : Cauchy f) :
g.NeBot → ∀ (h_le : g ≤ f), Cauchy g
source
theorem cauchy_nhds {α : Type u} [uniformSpace : UniformSpace α] {a : α} :
Cauchy (nhds a)
source
theorem cauchy_pure {α : Type u} [uniformSpace : UniformSpace α] {a : α} :
Cauchy (pure a)
source
theorem Filter.Tendsto.cauchy_map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [l.NeBot] {f : β → α} {a : α} (h : Tendsto f l (nhds a)) :
Cauchy (map f l)
source
theorem Cauchy.mono_uniformSpace {β : Type v} {u v : UniformSpace β} {F : Filter β} (huv : u ≤ v) (hF : Cauchy F) :
Cauchy F
source
theorem cauchy_inf_uniformSpace {β : Type v} {u v : UniformSpace β} {F : Filter β} :
Cauchy F ↔ Cauchy F ∧ Cauchy F
source
theorem cauchy_iInf_uniformSpace {β : Type v} {ι : Sort u_1} [Nonempty ι] {u : ι → UniformSpace β} {l : Filter β} :
Cauchy l ↔ ∀ (i : ι), Cauchy l
source
theorem cauchy_iInf_uniformSpace' {β : Type v} {ι : Sort u_1} {u : ι → UniformSpace β} {l : Filter β} [l.NeBot] :
Cauchy l ↔ ∀ (i : ι), Cauchy l
source
theorem cauchy_comap_uniformSpace {β : Type v} {u : UniformSpace β} {α : Type u_1} {f : α → β} {l : Filter α} :
Cauchy l ↔ Cauchy (Filter.map f l)
source
theorem cauchy_prod_iff {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {F : Filter (α × β)} :
Cauchy F ↔ Cauchy (Filter.map Prod.fst F) ∧ Cauchy (Filter.map Prod.snd F)
source
theorem Cauchy.prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter α} {g : Filter β} (hf : Cauchy f) (hg : Cauchy g) :
Cauchy (f ×ˢ g)
source
theorem le_nhds_of_cauchy_adhp_aux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α} (adhs : ∀ s ∈ uniformity α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t) :
f ≤ nhds x

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`.

source
theorem le_nhds_of_cauchy_adhp {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α} (hf : Cauchy f) (adhs : ClusterPt x f) :
f ≤ nhds x

If `x` is an adherent (cluster) point for a Cauchy filter `f`, then it is a limit point for `f`.

source
theorem le_nhds_iff_adhp_of_cauchy {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α} (hf : Cauchy f) :
f ≤ nhds x ↔ ClusterPt x f
source
theorem Cauchy.map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter α} {m : α → β} (hf : Cauchy f) (hm : UniformContinuous m) :
Cauchy (Filter.map m f)
source
theorem Cauchy.comap {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f) (hm : Filter.comap (fun (p : α × α) => (m p.1, m p.2)) (uniformity β) ≤ uniformity α) [(Filter.comap m f).NeBot] :
Cauchy (Filter.comap m f)
source
theorem Cauchy.comap' {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f) (hm : Filter.comap (fun (p : α × α) => (m p.1, m p.2)) (uniformity β) ≤ uniformity α) :
(Filter.comap m f).NeBot → Cauchy (Filter.comap m f)
source
def CauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] (u : β → α) :
Prop

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.

Equations

- CauchySeq u = Cauchy (Filter.map u Filter.atTop)

Instances For

source
theorem CauchySeq.tendsto_uniformity {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (h : CauchySeq u) :
Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)
source
theorem CauchySeq.nonempty {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (hu : CauchySeq u) :
Nonempty β
source
theorem CauchySeq.mem_entourage {α : Type u} [uniformSpace : UniformSpace α] {β : Type u_1} [SemilatticeSup β] {u : β → α} (h : CauchySeq u) {V : SetRel α α} (hV : V ∈ uniformity α) :
∃ (k₀ : β), ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
source
theorem Filter.Tendsto.cauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] {f : β → α} {x : α} (hx : Tendsto f atTop (nhds x)) :
CauchySeq f
source
theorem cauchySeq_const {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] (x : α) :
CauchySeq fun (x_1 : β) => x
source
theorem cauchySeq_iff_tendsto {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} :
CauchySeq u ↔ Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)
source
theorem CauchySeq.comp_tendsto {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [Preorder β] [SemilatticeSup γ] [Nonempty γ] {f : β → α} (hf : CauchySeq f) {g : γ → β} (hg : Filter.Tendsto g Filter.atTop Filter.atTop) :
CauchySeq (f ∘ g)
source
theorem CauchySeq.comp_injective {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [NoMaxOrder β] [Nonempty β] {u : ℕ → α} (hu : CauchySeq u) {f : β → ℕ} (hf : Function.Injective f) :
CauchySeq (u ∘ f)
source
theorem Function.Bijective.cauchySeq_comp_iff {α : Type u} [uniformSpace : UniformSpace α] {f : ℕ → ℕ} (hf : Bijective f) (u : ℕ → α) :
CauchySeq (u ∘ f) ↔ CauchySeq u
source
theorem CauchySeq.subseq_subseq_mem {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} (hu : CauchySeq u) {f g : ℕ → ℕ} (hf : Filter.Tendsto f Filter.atTop Filter.atTop) (hg : Filter.Tendsto g Filter.atTop Filter.atTop) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
source
theorem cauchySeq_iff' {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} :
CauchySeq u ↔ ∀ V ∈ uniformity α, ∀ᶠ (k : ℕ × ℕ) in Filter.atTop, k ∈ Prod.map u u ⁻¹' V
source
theorem cauchySeq_iff {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} :
CauchySeq u ↔ ∀ V ∈ uniformity α, ∃ (N : ℕ), ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
source
theorem CauchySeq.prodMap {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} {δ : Type u_2} [UniformSpace β] [Preorder γ] [Preorder δ] {u : γ → α} {v : δ → β} (hu : CauchySeq u) (hv : CauchySeq v) :
CauchySeq (Prod.map u v)
source
theorem CauchySeq.prodMk {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [UniformSpace β] [Preorder γ] {u : γ → α} {v : γ → β} (hu : CauchySeq u) (hv : CauchySeq v) :
CauchySeq fun (x : γ) => (u x, v x)
source
theorem CauchySeq.eventually_eventually {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (hu : CauchySeq u) {V : SetRel α α} (hV : V ∈ uniformity α) :
∀ᶠ (k : β) (l : β) in Filter.atTop, (u k, u l) ∈ V
source
theorem UniformContinuous.comp_cauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [UniformSpace β] [Preorder γ] {f : α → β} (hf : UniformContinuous f) {u : γ → α} (hu : CauchySeq u) :
CauchySeq (f ∘ u)
source
theorem CauchySeq.subseq_mem {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} (hu : CauchySeq u) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
source
theorem Filter.Tendsto.subseq_mem_entourage {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} {a : α} (hu : Tendsto u atTop (nhds a)) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
source
theorem tendsto_nhds_of_cauchySeq_of_subseq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (hu : CauchySeq u) {ι : Type u_1} {f : ι → β} {p : Filter ι} [p.NeBot] (hf : Filter.Tendsto f p Filter.atTop) {a : α} (ha : Filter.Tendsto (u ∘ f) p (nhds a)) :
Filter.Tendsto u Filter.atTop (nhds a)

If a Cauchy sequence has a convergent subsequence, then it converges.

source
theorem cauchySeq_shift {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} (k : ℕ) :
(CauchySeq fun (n : ℕ) => u (n + k)) ↔ CauchySeq u

Any shift of a Cauchy sequence is also a Cauchy sequence.

source
theorem Filter.HasBasis.cauchySeq_iff {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → SetRel α α} (h : (uniformity α).HasBasis p s) :
CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
source
theorem Filter.HasBasis.cauchySeq_iff' {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → SetRel α α} (H : (uniformity α).HasBasis p s) :
CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
source
theorem cauchySeq_of_controlled {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] (U : β → SetRel α α) (hU : ∀ s ∈ uniformity α, ∃ (n : β), U n ⊆ s) {f : β → α} (hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N) :
CauchySeq f
source
theorem isComplete_iff_clusterPt {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
IsComplete s ↔ ∀ (l : Filter α), Cauchy l → l ≤ Filter.principal s → ∃ x ∈ s, ClusterPt x l
source
theorem isComplete_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ Filter.principal s → ∃ x ∈ s, ↑l ≤ nhds x
source
theorem isComplete_iff_ultrafilter' {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ nhds x
source
theorem IsComplete.union {α : Type u} [uniformSpace : UniformSpace α] {s t : Set α} (hs : IsComplete s) (ht : IsComplete t) :
IsComplete (s ∪ t)
source
theorem isComplete_iUnion_separated {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {s : ι → Set α} (hs : ∀ (i : ι), IsComplete (s i)) {U : SetRel α α} (hU : U ∈ uniformity α) (hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j) :
IsComplete (⋃ (i : ι), s i)
source
class CompleteSpace (α : Type u) [UniformSpace α] :
Prop

A complete space is defined here using uniformities. A uniform space is complete if every Cauchy filter converges.

- complete {f : Filter α} : Cauchy f → ∃ (x : α), f ≤ nhds x

  In a complete uniform space, every Cauchy filter converges.

Instances

source
theorem complete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] :
IsComplete Set.univ
source
instance CompleteSpace.prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [CompleteSpace α] [CompleteSpace β] :
CompleteSpace (α × β)
source
theorem CompleteSpace.fst_of_prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty β] :
CompleteSpace α
source
theorem CompleteSpace.snd_of_prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty α] :
CompleteSpace β
source
theorem completeSpace_prod_of_nonempty {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [Nonempty α] [Nonempty β] :
CompleteSpace (α × β) ↔ CompleteSpace α ∧ CompleteSpace β
source
instance CompleteSpace.mulOpposite {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] :
CompleteSpace α ᵐᵒᵖ
source
instance CompleteSpace.addOpposite {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] :
CompleteSpace α ᵃᵒᵖ
source
theorem completeSpace_of_isComplete_univ {α : Type u} [uniformSpace : UniformSpace α] (h : IsComplete Set.univ) :
CompleteSpace α

If `univ` is complete, the space is a complete space

source
theorem completeSpace_iff_isComplete_univ {α : Type u} [uniformSpace : UniformSpace α] :
CompleteSpace α ↔ IsComplete Set.univ
source
theorem completeSpace_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] :
CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ∃ (x : α), ↑l ≤ nhds x
source
theorem cauchy_iff_exists_le_nhds {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {l : Filter α} [l.NeBot] :
Cauchy l ↔ ∃ (x : α), l ≤ nhds x
source
theorem cauchy_map_iff_exists_tendsto {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [CompleteSpace α] {l : Filter β} {f : β → α} [l.NeBot] :
Cauchy (Filter.map f l) ↔ ∃ (x : α), Filter.Tendsto f l (nhds x)
source
theorem cauchySeq_tendsto_of_complete {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] [CompleteSpace α] {u : β → α} (H : CauchySeq u) :
∃ (x : α), Filter.Tendsto u Filter.atTop (nhds x)

A Cauchy sequence in a complete space converges

source
theorem cauchySeq_tendsto_of_isComplete {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {K : Set α} (h₁ : IsComplete K) {u : β → α} (h₂ : ∀ (n : β), u n ∈ K) (h₃ : CauchySeq u) :
∃ v ∈ K, Filter.Tendsto u Filter.atTop (nhds v)

If `K` is a complete subset, then any Cauchy sequence in `K` converges to a point in `K`

source
theorem Cauchy.le_nhds_lim {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {f : Filter α} (hf : Cauchy f) :
f ≤ nhds (lim f)
source
theorem CauchySeq.tendsto_limUnder {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] [CompleteSpace α] {u : β → α} (h : CauchySeq u) :
Filter.Tendsto u Filter.atTop (nhds (limUnder Filter.atTop u))
source
theorem IsClosed.isComplete {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α} (h : IsClosed s) :
IsComplete s
source
theorem DiscreteUniformity.eq_pure_of_cauchy {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α] {f : Filter α} (hf : Cauchy f) :
∃ (x : α), f = pure x

A Cauchy filter in a discrete uniform space is contained in the principal filter of a point.

source
instance DiscreteUniformity.instCompleteSpace {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α] :
CompleteSpace α

The discrete uniformity makes a space complete.

source
noncomputable def DiscreteUniformity.cauchyConst {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α] {f : Filter α} (hf : Cauchy f) :
α

A constant to which a Cauchy filter in a discrete uniform space converges.

Equations

- DiscreteUniformity.cauchyConst hf = ⋯.choose

Instances For

source
theorem DiscreteUniformity.eq_pure_cauchyConst {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α] {f : Filter α} (hf : Cauchy f) :
f = pure (cauchyConst hf)
source
def TotallyBounded {α : Type u} [uniformSpace : UniformSpace α] (s : Set α) :
Prop

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`.

Equations

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

Instances For

source
theorem TotallyBounded.exists_subset {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : TotallyBounded s) {U : SetRel α α} (hU : U ∈ uniformity α) :
∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
source
theorem totallyBounded_iff_subset {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
TotallyBounded s ↔ ∀ d ∈ uniformity α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ d}
source
theorem Filter.HasBasis.totallyBounded_iff {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → SetRel α α} (H : (uniformity α).HasBasis p U) {s : Set α} :
TotallyBounded s ↔ ∀ (i : ι), p i → ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}
source
theorem totallyBounded_of_forall_isSymm {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : ∀ V ∈ uniformity α, SetRel.IsSymm V → ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, UniformSpace.ball y V) :
TotallyBounded s
source
theorem TotallyBounded.subset {α : Type u} [uniformSpace : UniformSpace α] {s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) (h : TotallyBounded s₂) :
TotallyBounded s₁
source
theorem TotallyBounded.closure {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : TotallyBounded s) :
TotallyBounded (_root_.closure s)

The closure of a totally bounded set is totally bounded.

source
@[simp]
theorem totallyBounded_closure {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
TotallyBounded (closure s) ↔ TotallyBounded s
source
@[simp]
theorem totallyBounded_iUnion {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} [Finite ι] {s : ι → Set α} :
TotallyBounded (⋃ (i : ι), s i) ↔ ∀ (i : ι), TotallyBounded (s i)

A finite indexed union is totally bounded if and only if each set of the family is totally bounded.

source
theorem totallyBounded_biUnion {α : Type u} [uniformSpace : UniformSpace α] {ι : Type u_1} {I : Set ι} (hI : I.Finite) {s : ι → Set α} :
TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

A union indexed by a finite set is totally bounded if and only if each set of the family is totally bounded.

source
theorem totallyBounded_sUnion {α : Type u} [uniformSpace : UniformSpace α] {S : Set (Set α)} (hS : S.Finite) :
TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

A union of a finite family of sets is totally bounded if and only if each set of the family is totally bounded.

source
theorem Set.Finite.totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : s.Finite) :
TotallyBounded s

A finite set is totally bounded.

source
theorem Set.Subsingleton.totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : s.Subsingleton) :
TotallyBounded s

A subsingleton is totally bounded.

source
@[simp]
theorem totallyBounded_singleton {α : Type u} [uniformSpace : UniformSpace α] (a : α) :
TotallyBounded {a}
source
@[simp]
theorem totallyBounded_empty {α : Type u} [uniformSpace : UniformSpace α] :
TotallyBounded ∅
source
@[simp]
theorem totallyBounded_union {α : Type u} [uniformSpace : UniformSpace α] {s t : Set α} :
TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

The union of two sets is totally bounded if and only if each of the two sets is totally bounded.

source
theorem TotallyBounded.union {α : Type u} [uniformSpace : UniformSpace α] {s t : Set α} (hs : TotallyBounded s) (ht : TotallyBounded t) :
TotallyBounded (s ∪ t)

The union of two totally bounded sets is totally bounded.

source
@[simp]
theorem totallyBounded_insert {α : Type u} [uniformSpace : UniformSpace α] (a : α) {s : Set α} :
TotallyBounded (insert a s) ↔ TotallyBounded s
source
theorem TotallyBounded.insert {α : Type u} [uniformSpace : UniformSpace α] (a : α) {s : Set α} :
TotallyBounded s → TotallyBounded (insert a s)

Alias of the reverse direction of `totallyBounded_insert`.

source
theorem TotallyBounded.image {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} (hs : TotallyBounded s) (hf : UniformContinuous f) :
TotallyBounded (f '' s)

The image of a totally bounded set under a uniformly continuous map is totally bounded.

source
theorem Ultrafilter.cauchy_of_totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (f : Ultrafilter α) (hs : TotallyBounded s) (h : ↑f ≤ Filter.principal s) :
Cauchy ↑f
source
theorem totallyBounded_iff_filter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
TotallyBounded s ↔ ∀ (f : Filter α), f.NeBot → f ≤ Filter.principal s → ∃ c ≤ f, Cauchy c
source
theorem totallyBounded_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
TotallyBounded s ↔ ∀ (f : Ultrafilter α), ↑f ≤ Filter.principal s → Cauchy ↑f
source
theorem isCompact_iff_totallyBounded_isComplete {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} :
IsCompact s ↔ TotallyBounded s ∧ IsComplete s
source
theorem IsCompact.totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : IsCompact s) :
TotallyBounded s
source
theorem IsCompact.isComplete {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : IsCompact s) :
IsComplete s
source
@[instance 100]
instance complete_of_compact {α : Type u} [UniformSpace α] [CompactSpace α] :
CompleteSpace α
source
theorem TotallyBounded.isCompact_of_isComplete {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (ht : TotallyBounded s) (hc : IsComplete s) :
IsCompact s
source
theorem TotallyBounded.isCompact_of_isClosed {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α} (ht : TotallyBounded s) (hc : IsClosed s) :
IsCompact s
source
@[deprecated TotallyBounded.isCompact_of_isClosed (since := "2025-08-30")]
theorem isCompact_of_totallyBounded_isClosed {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α} (ht : TotallyBounded s) (hc : IsClosed s) :
IsCompact s

Alias of `TotallyBounded.isCompact_of_isClosed`.

source
theorem CauchySeq.totallyBounded_range {α : Type u} [uniformSpace : UniformSpace α] {s : ℕ → α} (hs : CauchySeq s) :
TotallyBounded (Set.range s)

Every Cauchy sequence over `ℕ` is totally bounded.

source
def interUnionBalls {α : Type u} (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → SetRel α α) :
Set α

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.

Equations

- interUnionBalls xs u V = ⋂ (n : ℕ), ⋃ (m : ℕ), ⋃ (_ : m ≤ u n), UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)

Instances For

source
theorem totallyBounded_interUnionBalls {α : Type u} [uniformSpace : UniformSpace α] {p : ℕ → Prop} {U : ℕ → SetRel α α} (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
TotallyBounded (interUnionBalls xs u U)
source
theorem isCompact_closure_interUnionBalls {α : Type u} [uniformSpace : UniformSpace α] {p : ℕ → Prop} {U : ℕ → SetRel α α} (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
IsCompact (closure (interUnionBalls xs u U))

The construction `interUnionBalls` is used to have a relatively compact set.

### Sequentially complete space #

In this section we prove that a uniform space is complete provided that it is sequentially complete (i.e., any Cauchy sequence converges) and its uniformity filter admits a countable generating set. In particular, this applies to (e)metric spaces, see the files `Topology/MetricSpace/EmetricSpace` and `Topology/MetricSpace/Basic`.

More precisely, we assume that there is a sequence of entourages `U_n` such that any other entourage includes one of `U_n`. Then any Cauchy filter `f` generates a decreasing sequence of sets `s_n ∈ f` such that `s_n × s_n ⊆ U_n`. Choose a sequence `x_n∈s_n`. It is easy to show that this is a Cauchy sequence. If this sequence converges to some `a`, then `f ≤ 𝓝 a`.

source
def SequentiallyComplete.setSeqAux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) :
{ s : Set α // s ∈ f ∧ s ×ˢ s ⊆ U n }

An auxiliary sequence of sets approximating a Cauchy filter.

Equations

- SequentiallyComplete.setSeqAux hf U_mem n = Classical.indefiniteDescription (fun (s : Set α) => s ∈ f ∧ s ×ˢ s ⊆ U n) ⋯

Instances For

source
def SequentiallyComplete.setSeq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) :
Set α

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`.

Equations

- SequentiallyComplete.setSeq hf U_mem n = ⋂ m ∈ Set.Iic n, ↑(SequentiallyComplete.setSeqAux hf U_mem m)

Instances For

source
theorem SequentiallyComplete.setSeq_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) :
setSeq hf U_mem n ∈ f
source
theorem SequentiallyComplete.setSeq_mono {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃m n : ℕ⦄ (h : m ≤ n) :
setSeq hf U_mem n ⊆ setSeq hf U_mem m
source
theorem SequentiallyComplete.setSeq_sub_aux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) :
setSeq hf U_mem n ⊆ ↑(setSeqAux hf U_mem n)
source
theorem SequentiallyComplete.setSeq_prod_subset {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) {N m n : ℕ} (hm : N ≤ m) (hn : N ≤ n) :
setSeq hf U_mem m ×ˢ setSeq hf U_mem n ⊆ U N
source
def SequentiallyComplete.seq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) :
α

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.

Equations

- SequentiallyComplete.seq hf U_mem n = Exists.choose ⋯

Instances For

source
theorem SequentiallyComplete.seq_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) :
seq hf U_mem n ∈ setSeq hf U_mem n
source
theorem SequentiallyComplete.seq_pair_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃N m n : ℕ⦄ (hm : N ≤ m) (hn : N ≤ n) :
(seq hf U_mem m, seq hf U_mem n) ∈ U N
source
theorem SequentiallyComplete.seq_is_cauchySeq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ s ∈ uniformity α, ∃ (n : ℕ), U n ⊆ s) :
CauchySeq (seq hf U_mem)
source
theorem SequentiallyComplete.le_nhds_of_seq_tendsto_nhds {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ s ∈ uniformity α, ∃ (n : ℕ), U n ⊆ s) ⦃a : α⦄ (ha : Filter.Tendsto (seq hf U_mem) Filter.atTop (nhds a)) :
f ≤ nhds a

If the sequence `SequentiallyComplete.seq` converges to `a`, then `f ≤ 𝓝 a`.

source
theorem UniformSpace.complete_of_convergent_controlled_sequences {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (U : ℕ → SetRel α α) (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Filter.Tendsto u Filter.atTop (nhds a)) :
CompleteSpace α

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.

source
theorem UniformSpace.complete_of_cauchySeq_tendsto {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (H' : ∀ (u : ℕ → α), CauchySeq u → ∃ (a : α), Filter.Tendsto u Filter.atTop (nhds a)) :
CompleteSpace α

A sequentially complete uniform space with a countable basis of the uniformity filter is complete.

source
@[instance 100]
instance UniformSpace.firstCountableTopology (α : Type u) [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] :
FirstCountableTopology α
source
instance UniformSpace.secondCountable_of_separable (α : Type u) [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] [TopologicalSpace.SeparableSpace α] :
SecondCountableTopology α

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 `𝓤 α`.