Theorems · Inductive type · general topology
UniformSpace.Core
Type u → Type u
This core description of a uniform space is outside of the type class hierarchy. It is useful for constructions of uniform spaces, when the topology is derived from the uniform space.
- Defined in
- Mathlib.Topology.UniformSpace.Defs
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by24
Results whose statement or proof uses this declaration.
- UniformSpace.Core.uniformitystatement and proof · cited by 8
- UniformSpace.toCorestatement · cited by 3
- UniformSpace.Core.toTopologicalSpacestatement and proof · cited by 3
- UniformSpace.Core.reflstatement and proof · cited by 2
- UniformSpace.Core.mk.injstatement · cited by 1
- UniformSpace.Core.mk.noConfusionstatement · cited by 1
- UniformSpace.Core.compstatement and proof · cited by 1
- UniformSpace.Core.comp_mem_uniformity_setsstatement and proof · cited by 1
- UniformSpace.Core.nhds_toTopologicalSpacestatement and proof · cited by 1
- UniformSpace.ofCorestatement and proof · cited by 1
- UniformSpace.ofCoreEqstatement and proof · cited by 1
- UniformSpace.Core.mk.injEqstatement · cited by 0