Def UniformSpace.ofCore

Modification history

2024-05-07 01:05

Mathlib/Topology/UniformSpace/Basic.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted UniformSpace.ofCore View on Github →

2024-03-20 13:11

Mathlib/Topology/UniformSpace/Basic.lean

refactor(UniformSpace): change the definition (#10901) …

Modified UniformSpace.ofCore View on Github →

2023-02-02 05:07

Mathlib/Topology/UniformSpace/Basic.lean

feat: port Topology.UniformSpace.Basic (#1993)

Added UniformSpace.ofCore View on Github →