Theory of complete separated uniform spaces. #

This file is for elementary lemmas that depend on both Cauchy filters and separation.

theorem IsComplete.isClosed {α : Type u_1} [UniformSpace α] [SeparatedSpace α] {s : Set α} (h : IsComplete s) :

In a separated space, a complete set is closed.

theorem DenseInducing.continuous_extend_of_cauchy {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {γ : Type u_3} [UniformSpace γ] [CompleteSpace γ] [SeparatedSpace γ] {e : αβ} {f : αγ} (de : DenseInducing e) (h : ∀ (b : β), Cauchy ( f (Filter.comap e (nhds b)))) :