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.toIsClosedEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
[T0Space β]
{f : α → β}
(hf : IsUniformEmbedding f)
:
@[deprecated IsUniformEmbedding.toIsClosedEmbedding]
theorem
IsUniformEmbedding.toClosedEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
[T0Space β]
{f : α → β}
(hf : IsUniformEmbedding f)
:
Alias of IsUniformEmbedding.toIsClosedEmbedding.
@[deprecated IsUniformEmbedding.toIsClosedEmbedding]
theorem
UniformEmbedding.toIsClosedEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
[T0Space β]
{f : α → β}
(hf : IsUniformEmbedding f)
:
Alias of IsUniformEmbedding.toIsClosedEmbedding.
@[deprecated UniformEmbedding.toIsClosedEmbedding]
theorem
UniformEmbedding.toClosedEmbedding
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[UniformSpace β]
[CompleteSpace α]
[T0Space β]
{f : α → β}
(hf : IsUniformEmbedding f)
:
Alias of IsUniformEmbedding.toIsClosedEmbedding.
Alias of IsUniformEmbedding.toIsClosedEmbedding.
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)