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 α] [T0Space α] {s : Set α} (h : IsComplete s) :
IsClosed s
In a separated space, a complete set is closed.
theorem IsUniformEmbedding.isClosedEmbedding {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] [CompleteSpace α] [T0Space β] {f : α → β} (hf : IsUniformEmbedding f) :
theorem IsDenseInducing.continuous_extend_of_cauchy {α : Type u_1} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] {γ : Type u_4} [UniformSpace γ] [CompleteSpace γ] [T0Space γ] {e : α → β} {f : α → γ} (de : IsDenseInducing e) (h : ∀ (b : β), Cauchy (Filter.map f (Filter.comap e (nhds b)))) :
Continuous (de.extend f)