Commit 2020-08-21 10:07 045b6c7f

chore(topology/basic): use dot notation (#3861)

API changes

• add set.range_sigma_mk, finset.sigma_preimage_mk, finset.sigma_preimage_mk_of_subset, finset.sigma_image_fst_preimage_mk, finset.prod_preimage';
• rename filter.monotone.tendsto_at_top_finset to filter.tendsto_at_top_finset_of_monotone, add alias monotone.tendsto_at_top_finset;
• add filter.tendsto_finset_preimage_at_top_at_top;
• add filter.tendsto.frequently;
• add cluster_pt_principal_iff_frequently, mem_closure_iff_frequently, filter.frequently.mem_closure, filter.frequently.mem_of_closed, is_closed.mem_of_frequently_of_tendsto;
• rename mem_of_closed_of_tendsto to is_closed.mem_of_tendsto;
• delete mem_of_closed_of_tendsto'; use new is_closed.mem_of_frequently_of_tendsto instead;