Theorems · Definition · general topology

UniformSpace.Completion.extension

{α : Type u_1} → [inst : UniformSpace α] → {β : Type u_2} → [UniformSpace β] → (α → β) → UniformSpace.Completion α → β

"Extension" to the completion. It is defined for any map f but returns an arbitrary constant value if f is not uniformly continuous

Defined in

Mathlib.Topology.UniformSpace.Completion

Cited by

16 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace