Theory of complete separated uniform spaces. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 α}
(h : is_complete 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)
(h : ∀ (b : β), cauchy (filter.map f (filter.comap e (nhds b)))) :
continuous (de.extend f)