mathlib
06256910 - chore(topology/*): use dot syntax for some lemmas (#3251)

Commit
5 years ago
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`
Author
Parents
Loading