Commit 2021-05-20 02:00 5a67f2c6
View on Github →chore(topology): rename compact to is_compact in theorem names (#7672)
Some time ago, we switched from compact to is_compact, for coherence with is_open, is_closed and so on. However, several lemma names were not changed at the time. This PR fixes some of them. Plus a few minor stuff (notably, introduce le_self_add to replace the dozen of uses of le_add_right (le_refl _) in the library -- and weaken some metric assumptions to pseudo_metric, without touching the proofs).