Theorems · Theorem · general topology

completeSpace_extension

∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {m : β → α},
  IsUniformInducing m → DenseRange m → (∀ (f : Filter β), Cauchy f → ∃ x, Filter.map m f ≤ nhds x) → CompleteSpace α

Defined in

Mathlib.Topology.UniformSpace.UniformEmbedding

Cited by

0 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpaceUniformSpace