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

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 = (Filter.NeBot f ∧ f ×ˢ f ≤ uniformity α)

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, x ∈ s ∧ f ≤ nhds x

theorem Filter.HasBasis.cauchy_iff {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)} (h : Filter.HasBasis (uniformity α) p s) {f : Filter α} : Cauchy f ↔ Filter.NeBot f ∧ ∀ (i : ι), p i → ∃ t, t ∈ f ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (x, y) ∈ s i

theorem cauchy_iff' {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} : Cauchy f ↔ Filter.NeBot f ∧ ∀ (s : Set (α × α)), s ∈ uniformity α → ∃ t, t ∈ f ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → (x, y) ∈ s

theorem cauchy_iff {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} : Cauchy f ↔ Filter.NeBot f ∧ ∀ (s : Set (α × α)), s ∈ uniformity α → ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s

theorem cauchy_iff_le {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} [hl : Filter.NeBot l] : Cauchy l ↔ l ×ˢ l ≤ uniformity α

theorem Cauchy.ultrafilter_of {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} (h : Cauchy l) : Cauchy ↑(Ultrafilter.of l)

theorem cauchy_map_iff {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} {f : β → α} : Cauchy (Filter.map f l) ↔ Filter.NeBot l ∧ Filter.Tendsto (fun p => (f p.fst, f p.snd)) (l ×ˢ l) (uniformity α)

theorem cauchy_map_iff' {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [hl : Filter.NeBot l] {f : β → α} : Cauchy (Filter.map f l) ↔ Filter.Tendsto (fun p => (f p.fst, f p.snd)) (l ×ˢ l) (uniformity α)

theorem Cauchy.mono {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {g : Filter α} [hg : Filter.NeBot g] (h_c : Cauchy f) (h_le : g ≤ f) : Cauchy g

theorem Cauchy.mono' {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {g : Filter α} (h_c : Cauchy f) : Filter.NeBot g → g ≤ f → Cauchy g

theorem cauchy_nhds {α : Type u} [uniformSpace : UniformSpace α] {a : α} : Cauchy (nhds a)

theorem cauchy_pure {α : Type u} [uniformSpace : UniformSpace α] {a : α} : Cauchy (pure a)

theorem Filter.Tendsto.cauchy_map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [Filter.NeBot l] {f : β → α} {a : α} (h : Filter.Tendsto f l (nhds a)) : Cauchy (Filter.map f l)

theorem Cauchy.mono_uniformSpace {β : Type v} {u : UniformSpace β} {v : UniformSpace β} {F : Filter β} (huv : u ≤ v) (hF : Cauchy F) : Cauchy F

theorem cauchy_inf_uniformSpace {β : Type v} {u : UniformSpace β} {v : UniformSpace β} {F : Filter β} : Cauchy F ↔ Cauchy F ∧ Cauchy F

theorem cauchy_iInf_uniformSpace {β : Type v} {ι : Sort u_1} [Nonempty ι] {u : ι → UniformSpace β} {l : Filter β} : Cauchy l ↔ ∀ (i : ι), Cauchy l

theorem cauchy_iInf_uniformSpace' {β : Type v} {ι : Sort u_1} {u : ι → UniformSpace β} {l : Filter β} [Filter.NeBot l] : Cauchy l ↔ ∀ (i : ι), Cauchy l

theorem cauchy_comap_uniformSpace {α : Type u} {β : Type v} {u : UniformSpace β} {f : α → β} {l : Filter α} : Cauchy l ↔ Cauchy (Filter.map f l)

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)

theorem Cauchy.prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter α} {g : Filter β} (hf : Cauchy f) (hg : Cauchy g) : Cauchy (f ×ˢ g)

theorem le_nhds_of_cauchy_adhp_aux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α} (adhs : ∀ (s : Set (α × α)), s ∈ uniformity α → ∃ t, 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.

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.

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

theorem Cauchy.map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter α} {m : α → β} (hf : Cauchy f) (hm : UniformContinuous m) : Cauchy (Filter.map m f)

theorem Cauchy.comap {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f) (hm : Filter.comap (fun p => (m p.fst, m p.snd)) (uniformity β) ≤ uniformity α) [Filter.NeBot (Filter.comap m f)] : Cauchy (Filter.comap m f)

theorem Cauchy.comap' {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f) (hm : Filter.comap (fun p => (m p.fst, m p.snd)) (uniformity β) ≤ uniformity α) : Filter.NeBot (Filter.comap m f) → Cauchy (Filter.comap m f)

def CauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] (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)

theorem CauchySeq.tendsto_uniformity {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] {u : β → α} (h : CauchySeq u) : Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)

theorem CauchySeq.nonempty {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] {u : β → α} (hu : CauchySeq u) : Nonempty β

theorem CauchySeq.mem_entourage {α : Type u} [uniformSpace : UniformSpace α] {β : Type u_1} [SemilatticeSup β] {u : β → α} (h : CauchySeq u) {V : Set (α × α)} (hV : V ∈ uniformity α) : ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

theorem Filter.Tendsto.cauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] {f : β → α} {x : α} (hx : Filter.Tendsto f Filter.atTop (nhds x)) : CauchySeq f

theorem cauchySeq_const {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] (x : α) : CauchySeq fun x => x

theorem cauchySeq_iff_tendsto {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)

theorem CauchySeq.comp_tendsto {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [SemilatticeSup β] [SemilatticeSup γ] [Nonempty γ] {f : β → α} (hf : CauchySeq f) {g : γ → β} (hg : Filter.Tendsto g Filter.atTop Filter.atTop) : CauchySeq (f ∘ g)

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)

theorem Function.Bijective.cauchySeq_comp_iff {α : Type u} [uniformSpace : UniformSpace α] {f : ℕ → ℕ} (hf : Function.Bijective f) (u : ℕ → α) : CauchySeq (u ∘ f) ↔ CauchySeq u

theorem CauchySeq.subseq_subseq_mem {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → Set (α × α)} (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

theorem cauchySeq_iff' {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} : CauchySeq u ↔ ∀ (V : Set (α × α)), V ∈ uniformity α → ∀ᶠ (k : ℕ × ℕ) in Filter.atTop, k ∈ Prod.map u u ⁻¹' V

theorem cauchySeq_iff {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} : CauchySeq u ↔ ∀ (V : Set (α × α)), V ∈ uniformity α → ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ N → (u k, u l) ∈ V

theorem CauchySeq.prod_map {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} {δ : Type u_2} [UniformSpace β] [SemilatticeSup γ] [SemilatticeSup δ] {u : γ → α} {v : δ → β} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (Prod.map u v)

theorem CauchySeq.prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [UniformSpace β] [SemilatticeSup γ] {u : γ → α} {v : γ → β} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq fun x => (u x, v x)

theorem CauchySeq.eventually_eventually {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] {u : β → α} (hu : CauchySeq u) {V : Set (α × α)} (hV : V ∈ uniformity α) : ∀ᶠ (k : β) (l : β) in Filter.atTop, (u k, u l) ∈ V

theorem UniformContinuous.comp_cauchySeq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [UniformSpace β] [SemilatticeSup γ] {f : α → β} (hf : UniformContinuous f) {u : γ → α} (hu : CauchySeq u) : CauchySeq (f ∘ u)

theorem CauchySeq.subseq_mem {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → Set (α × α)} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} (hu : CauchySeq u) : ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n

theorem Filter.Tendsto.subseq_mem_entourage {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → Set (α × α)} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} {a : α} (hu : Filter.Tendsto u Filter.atTop (nhds a)) : ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

theorem tendsto_nhds_of_cauchySeq_of_subseq {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] {u : β → α} (hu : CauchySeq u) {ι : Type u_1} {f : ι → β} {p : Filter ι} [Filter.NeBot p] (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.

theorem Filter.HasBasis.cauchySeq_iff {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)} (h : Filter.HasBasis (uniformity α) p s) : CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

theorem Filter.HasBasis.cauchySeq_iff' {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)} (H : Filter.HasBasis (uniformity α) p s) : CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (n : β), n ≥ N → (u n, u N) ∈ s i

theorem cauchySeq_of_controlled {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] (U : β → Set (α × α)) (hU : ∀ (s : Set (α × α)), s ∈ uniformity α → ∃ n, U n ⊆ s) {f : β → α} (hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N) : CauchySeq f

theorem isComplete_iff_clusterPt {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsComplete s ↔ ∀ (l : Filter α), Cauchy l → l ≤ Filter.principal s → ∃ x, x ∈ s ∧ ClusterPt x l

theorem isComplete_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ Filter.principal s → ∃ x, x ∈ s ∧ ↑l ≤ nhds x

theorem isComplete_iff_ultrafilter' {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x, x ∈ s ∧ ↑l ≤ nhds x

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

theorem isComplete_iUnion_separated {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {s : ι → Set α} (hs : ∀ (i : ι), IsComplete (s i)) {U : Set (α × α)} (hU : U ∈ uniformity α) (hd : ∀ (i j : ι) (x : α), x ∈ s i → ∀ (y : α), y ∈ s j → (x, y) ∈ U → i = j) : IsComplete (⋃ (i : ι), s i)

class CompleteSpace (α : Type u) [UniformSpace α] : Prop

• complete : ∀ {f : Filter α}, Cauchy f → ∃ x, f ≤ nhds x

  In a complete uniform space, every Cauchy filter converges.

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

theorem complete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] : IsComplete Set.univ

instance CompleteSpace.prod {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] [CompleteSpace α] [CompleteSpace β] : CompleteSpace (α × β)

Equations

• @CompleteSpace.prod = @CompleteSpace.prod.proof_1

abbrev CompleteSpace.addOpposite.match_1 {α : Type u_1} [uniformSpace : UniformSpace α] : {f : Filter αᵃᵒᵖ} → (motive : (∃ x, Filter.map AddOpposite.unop f ≤ nhds x) → Prop) → ∀ (x : ∃ x, Filter.map AddOpposite.unop f ≤ nhds x), (∀ (x : α) (hx : Filter.map AddOpposite.unop f ≤ nhds x), motive (_ : ∃ x, Filter.map AddOpposite.unop f ≤ nhds x)) → motive x

Equations

• CompleteSpace.addOpposite.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

instance CompleteSpace.addOpposite {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] : CompleteSpace αᵃᵒᵖ

Equations

• @CompleteSpace.addOpposite = @CompleteSpace.addOpposite.proof_1

theorem CompleteSpace.addOpposite.proof_1 {α : Type u_1} [uniformSpace : UniformSpace α] [CompleteSpace α] : CompleteSpace αᵃᵒᵖ

instance CompleteSpace.mulOpposite {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] : CompleteSpace αᵐᵒᵖ

Equations

• @CompleteSpace.mulOpposite = @CompleteSpace.mulOpposite.proof_1

theorem completeSpace_of_isComplete_univ {α : Type u} [uniformSpace : UniformSpace α] (h : IsComplete Set.univ) : CompleteSpace α

If univ is complete, the space is a complete space

theorem completeSpace_iff_isComplete_univ {α : Type u} [uniformSpace : UniformSpace α] : CompleteSpace α ↔ IsComplete Set.univ

theorem completeSpace_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] : CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ∃ x, ↑l ≤ nhds x

theorem cauchy_iff_exists_le_nhds {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {l : Filter α} [Filter.NeBot l] : Cauchy l ↔ ∃ x, l ≤ nhds x

theorem cauchy_map_iff_exists_tendsto {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [CompleteSpace α] {l : Filter β} {f : β → α} [Filter.NeBot l] : Cauchy (Filter.map f l) ↔ ∃ x, Filter.Tendsto f l (nhds x)

theorem cauchySeq_tendsto_of_complete {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [CompleteSpace α] {u : β → α} (H : CauchySeq u) : ∃ x, Filter.Tendsto u Filter.atTop (nhds x)

A Cauchy sequence in a complete space converges

theorem cauchySeq_tendsto_of_isComplete {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] {K : Set α} (h₁ : IsComplete K) {u : β → α} (h₂ : ∀ (n : β), u n ∈ K) (h₃ : CauchySeq u) : ∃ v, 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

theorem Cauchy.le_nhds_lim {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] [Nonempty α] {f : Filter α} (hf : Cauchy f) : f ≤ nhds (lim f)

theorem CauchySeq.tendsto_limUnder {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [CompleteSpace α] [Nonempty α] {u : β → α} (h : CauchySeq u) : Filter.Tendsto u Filter.atTop (nhds (limUnder Filter.atTop u))

theorem IsClosed.isComplete {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α} (h : IsClosed s) : IsComplete s

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 : Set (α × α)), d ∈ uniformity α → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}

theorem TotallyBounded.exists_subset {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : TotallyBounded s) {U : Set (α × α)} (hU : U ∈ uniformity α) : ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}

theorem totallyBounded_iff_subset {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : TotallyBounded s ↔ ∀ (d : Set (α × α)), d ∈ uniformity α → ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ d}

theorem Filter.HasBasis.totallyBounded_iff {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → Set (α × α)} (H : Filter.HasBasis (uniformity α) p U) {s : Set α} : TotallyBounded s ↔ ∀ (i : ι), p i → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U i}

theorem totallyBounded_of_forall_symm {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : ∀ (V : Set (α × α)), V ∈ uniformity α → SymmetricRel V → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), UniformSpace.ball y V) : TotallyBounded s

theorem totallyBounded_subset {α : Type u} [uniformSpace : UniformSpace α] {s₁ : Set α} {s₂ : Set α} (hs : s₁ ⊆ s₂) (h : TotallyBounded s₂) : TotallyBounded s₁

theorem totallyBounded_empty {α : Type u} [uniformSpace : UniformSpace α] : TotallyBounded ∅

theorem TotallyBounded.closure {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : TotallyBounded s) : TotallyBounded (closure s)

The closure of a totally bounded set is totally bounded.

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.

theorem Ultrafilter.cauchy_of_totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (f : Ultrafilter α) (hs : TotallyBounded s) (h : ↑f ≤ Filter.principal s) : Cauchy ↑f

theorem totallyBounded_iff_filter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : TotallyBounded s ↔ ∀ (f : Filter α), Filter.NeBot f → f ≤ Filter.principal s → ∃ c, c ≤ f ∧ Cauchy c

theorem totallyBounded_iff_ultrafilter {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : TotallyBounded s ↔ ∀ (f : Ultrafilter α), ↑f ≤ Filter.principal s → Cauchy ↑f

theorem isCompact_iff_totallyBounded_isComplete {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsCompact s ↔ TotallyBounded s ∧ IsComplete s

theorem IsCompact.totallyBounded {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : IsCompact s) : TotallyBounded s

theorem IsCompact.isComplete {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : IsCompact s) : IsComplete s

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

Equations

• @complete_of_compact = @complete_of_compact.proof_1

theorem isCompact_of_totallyBounded_isClosed {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α} (ht : TotallyBounded s) (hc : IsClosed s) : IsCompact s

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

Every Cauchy sequence over ℕ is totally bounded.

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.

def SequentiallyComplete.setSeqAux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : { s // 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 => s ∈ f ∧ s ×ˢ s ⊆ U n) (_ : ∃ t, t ∈ f ∧ t ×ˢ t ⊆ U n)

def SequentiallyComplete.setSeq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (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 : ℕ) (_ : m ∈ Set.Iic n), ↑(SequentiallyComplete.setSeqAux hf U_mem m)

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

theorem SequentiallyComplete.setSeq_mono {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃m : ℕ⦄ ⦃n : ℕ⦄ (h : m ≤ n) : SequentiallyComplete.setSeq hf U_mem n ⊆ SequentiallyComplete.setSeq hf U_mem m

theorem SequentiallyComplete.setSeq_sub_aux {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : SequentiallyComplete.setSeq hf U_mem n ⊆ ↑(SequentiallyComplete.setSeqAux hf U_mem n)

theorem SequentiallyComplete.setSeq_prod_subset {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) {N : ℕ} {m : ℕ} {n : ℕ} (hm : N ≤ m) (hn : N ≤ n) : SequentiallyComplete.setSeq hf U_mem m ×ˢ SequentiallyComplete.setSeq hf U_mem n ⊆ U N

def SequentiallyComplete.seq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (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 = Classical.choose (_ : Set.Nonempty (SequentiallyComplete.setSeq hf U_mem n))

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

theorem SequentiallyComplete.seq_pair_mem {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃N : ℕ⦄ ⦃m : ℕ⦄ ⦃n : ℕ⦄ (hm : N ≤ m) (hn : N ≤ n) : (SequentiallyComplete.seq hf U_mem m, SequentiallyComplete.seq hf U_mem n) ∈ U N

theorem SequentiallyComplete.seq_is_cauchySeq {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ (s : Set (α × α)), s ∈ uniformity α → ∃ n, U n ⊆ s) : CauchySeq (SequentiallyComplete.seq hf U_mem)

theorem SequentiallyComplete.le_nhds_of_seq_tendsto_nhds {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ (s : Set (α × α)), s ∈ uniformity α → ∃ n, U n ⊆ s) ⦃a : α⦄ (ha : Filter.Tendsto (SequentiallyComplete.seq hf U_mem) Filter.atTop (nhds a)) : f ≤ nhds a

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

theorem UniformSpace.complete_of_convergent_controlled_sequences {α : Type u} [uniformSpace : UniformSpace α] [Filter.IsCountablyGenerated (uniformity α)] (U : ℕ → Set (α × α)) (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.

theorem UniformSpace.complete_of_cauchySeq_tendsto {α : Type u} [uniformSpace : UniformSpace α] [Filter.IsCountablyGenerated (uniformity α)] (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.

instance UniformSpace.firstCountableTopology (α : Type u) [uniformSpace : UniformSpace α] [Filter.IsCountablyGenerated (uniformity α)] : TopologicalSpace.FirstCountableTopology α

Equations

• UniformSpace.firstCountableTopology = UniformSpace.firstCountableTopology.proof_1

theorem UniformSpace.secondCountable_of_separable (α : Type u) [uniformSpace : UniformSpace α] [Filter.IsCountablyGenerated (uniformity α)] [TopologicalSpace.SeparableSpace α] : TopologicalSpace.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 𝓤 α. 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.