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) : IsClosed 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 (Filter.map f (Filter.comap e (nhds b)))) : Continuous (DenseInducing.extend de f)