Mathlib v3 is deprecated. Go to Mathlib v4

Def dist

Modification history

2018-08-28 15:05

analysis/metric_space.lean

refactor(analysis): add nndist; add finite product of metric spaces; prepare for normed spaces

Deleted dist View on Github →

2017-08-26 15:40

topology/metric_space.lean

feat(topology): port metric space from lean2

Added dist View on Github →