Mathlib v3 is deprecated. Go to Mathlib v4

Def uniform_space.core.mk_of_basis

Modification history

2022-04-03 16:42

src/topology/uniform_space/basic.lean

feat(topology/uniform_space/basic): constructing a `uniform_space.core` from a filter basis for the uniformity (#13065)

Added uniform_space.core.mk_of_basis View on Github →