Def UniformSpace.ofFun

Modification history

2024-09-29 03:18

Mathlib/Topology/UniformSpace/Basic.lean

chore(UniformSpace): move `ofFun` to a new file (#16737) …

Modified UniformSpace.ofFun View on Github →

2023-02-28 04:45

Mathlib/Topology/UniformSpace/Basic.lean

feat: define `UniformSpace.ofFun` (#2511) …

Added UniformSpace.ofFun View on Github →