Documentation

Mathlib.Topology.UniformSpace.CompleteSeparated

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) :

In a separated space, a complete set is closed.

theorem IsUniformEmbedding.toClosedEmbedding {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] [CompleteSpace α] [T0Space β] {f : αβ} (hf : IsUniformEmbedding f) :
@[deprecated IsUniformEmbedding.toClosedEmbedding]
theorem UniformEmbedding.toClosedEmbedding {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] [CompleteSpace α] [T0Space β] {f : αβ} (hf : IsUniformEmbedding f) :

Alias of IsUniformEmbedding.toClosedEmbedding.

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)