Mathlib v3 is deprecated. Go to Mathlib v4

Def emetric.diam

Modification history

2022-10-01 23:57
src/topology/metric_space/emetric_space.lean
chore(topology,analysis): make the sup metric and norm computable (#16570) …
Deleted emetric.diamView on Github →
2020-02-03 07:14
src/topology/metric_space/emetric_space.lean
refactor(topology/metric_space/emetric_space): redefine `diam` (#1941) …
Modified emetric.diamView on Github →
2019-01-30 09:57
src/topology/metric_space/emetric_space.lean
feat(topology/metric_space): diameter of a set in metric spaces (#651)
Added emetric.diamView on Github →