basic): `positivity` extension for `diam` (#16842)

Commit

3 years ago

feat(topology/metric_space/basic): `positivity` extension for `diam` (#16842) Add `positivity_diam`, a `positivity` extension for `metric.diam`.

Author

YaelDillies

Parents