mathlib documentation

topology.uniform_space.complete_separated

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 α} (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 (𝓝 b)))) :