mathlib3
9f77db21 - chore(topology/metric_space): add '@[continuity]' attributes (#6780)

Commit

4 years ago

chore(topology/metric_space): add '@[continuity]' attributes (#6780) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents