Mathlib.Topology.UniformSpace.CompleteSeparated

Module docstring

{"# Theory of complete separated uniform spaces.

This file is for elementary lemmas that depend on both Cauchy filters and separation. "}

IsComplete.isClosed theorem

[UniformSpace α] [T0Space α] {s : Set α} (h : IsComplete s) : IsClosed s

Full source

/-- In a separated space, a complete set is closed. -/
theorem IsComplete.isClosed [UniformSpace α] [T0Space α] {s : Set α} (h : IsComplete s) :
    IsClosed s :=
  isClosed_iff_clusterPt.2 fun a ha => by
    let f := 𝓝[s] a
    have : Cauchy f := cauchy_nhds.mono' ha inf_le_left
    rcases h f this inf_le_right with ⟨y, ys, fy⟩
    rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)]

Complete Subsets are Closed in T₀ Uniform Spaces

Informal description

In a uniform space $\alpha$ that is also a T₀ space, any complete subset $s \subseteq \alpha$ is closed.

IsUniformEmbedding.isClosedEmbedding theorem

 [UniformSpace α] [UniformSpace β] [CompleteSpace α] [T0Space β] {f : α → β} (hf : IsUniformEmbedding f) :
  IsClosedEmbedding f

Full source

theorem IsUniformEmbedding.isClosedEmbedding [UniformSpace α] [UniformSpace β] [CompleteSpace α]
    [T0Space β] {f : α → β} (hf : IsUniformEmbedding f) :
    IsClosedEmbedding f :=
  ⟨hf.isEmbedding, hf.isUniformInducing.isComplete_range.isClosed⟩

Uniform Embeddings from Complete Spaces to $T_0$ Spaces are Closed Embeddings

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, where $\alpha$ is complete and $\beta$ is a $T_0$ space. If $f : \alpha \to \beta$ is a uniform embedding, then $f$ is a closed embedding.

IsDenseInducing.continuous_extend_of_cauchy theorem

 {e : α → β} {f : α → γ} (de : IsDenseInducing e) (h : ∀ b : β, Cauchy (map f (comap e <| 𝓝 b))) :
  Continuous (de.extend f)

Full source

theorem continuous_extend_of_cauchy {e : α → β} {f : α → γ} (de : IsDenseInducing e)
    (h : ∀ b : β, Cauchy (map f (comap e <| 𝓝 b))) : Continuous (de.extend f) :=
  de.continuous_extend fun b => CompleteSpace.complete (h b)

Continuity of Extension for Dense Inducing Maps with Cauchy Condition

Informal description

Let $e : \alpha \to \beta$ and $f : \alpha \to \gamma$ be functions, where $e$ is a dense inducing map. If for every $b \in \beta$, the filter $\text{map}\, f (\text{comap}\, e (\mathcal{N}(b)))$ is Cauchy, then the extension of $f$ via $e$ is continuous.