basic): golf, avoid unfold (#13923)

Commit

3 years ago

feat(topology/metric_space/basic): golf, avoid unfold (#13923) * Don't use `unfold` in `nnreal.pseudo_metric_space`. * Golf some proofs.

Author

urkud

Parents