Theorems · Definition · category theory

CpltSepUniformSpace.of

(X : Type u) → [inst : UniformSpace X] → [CompleteSpace X] → [T0Space X] → CpltSepUniformSpace

Construct a bundled UniformSpace from the underlying type and the appropriate typeclasses.

Defined in

Mathlib.Topology.Category.UniformSpace

Cited by

3 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

UniformSpaceCompleteSpaceT0Space