Theorems · Theorem · general topology

UniformSpace.Completion.extension_unique

∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β} [T0Space β]
  [CompleteSpace β],
  UniformContinuous f →
    ∀ {g : UniformSpace.Completion α → β},
      UniformContinuous g → (∀ (a : α), f a = g ↑a) → UniformSpace.Completion.extension f = g

Defined in

Mathlib.Topology.UniformSpace.Completion

Cited by

3 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpaceT0SpaceCompleteSpace