Commit 2020-06-30 22:34 06256910

chore(topology/*): use dot syntax for some lemmas (#3251) Rename:

• closure_eq_of_is_closed to is_closed.closure_eq;
• closed_of_compact to compact.is_closed;
• bdd_above_of_compact to compact.bdd_above;
• bdd_below_of_compact to compact.bdd_below.
• is_complete_of_is_closed to is_closed.is_complete
• is_closed_of_is_complete to is_complete.is_closed
• is_closed_iff_nhds to is_closed_iff_cluster_pt
• closure_subset_iff_subset_of_is_closed to is_closed.closure_subset_iff Add:
• closure_closed_ball (@[simp] lemma)
• is_closed.closure_subset : is_closed s → closure s ⊆ s