Theory of complete separated uniform spaces.
This file is for elementary lemmas that depend on both Cauchy filters and separation.
theorem
is_complete.is_closed
{α : Type u_1}
[uniform_space α]
[separated_space α]
{s : set α} :
is_complete s → is_closed s
theorem
dense_inducing.continuous_extend_of_cauchy
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[topological_space β]
{γ : Type u_3}
[uniform_space γ]
[complete_space γ]
[separated_space γ]
{e : α → β}
{f : α → γ}
(de : dense_inducing e) :
(∀ (b : β), cauchy (filter.map f (filter.comap e (nhds b)))) → continuous (de.extend f)