Commit 2021-02-22 14:12 120feb11

refactor(order/filter,topology): review API (#6347)

Filters

• move old filter.map_comap to filter.map_comap_of_mem;
• add a new filter.map_comap that doesn't assume range m ∈ f but gives map m (comap m f) = f ⊓ 𝓟 (range m) instead of map m (comap m f) = f;
• add filter.comap_le_comap_iff, use it to golf a couple of proofs;
• move some lemmas using filter.map_comap/filter.map_comap_of_mem closure to these lemmas;
• use function.injective m instead of ∀ x y, m x = m y → x = y in some lemmas;
• drop filter.le_map_comap_of_surjective', filter.map_comap_of_surjective', and filter.le_map_comap_of_surjective: the inequalities easily follow from equalities, and filter.map_comap_of_surjective' is just filter.map_comap_of_mem+filter.mem_sets_of_superset;

Topology

• add closed_embedding_subtype_coe, ennreal.open_embedding_coe;
• drop inducing_open, inducing_is_closed, embedding_open, and embedding_is_closed replace them with inducing.is_open_map and inducing.is_closed_map;
• move old inducing.map_nhds_eq to inducing.map_nhds_of_mem, the new inducing.map_nhds_eq says map f (𝓝 a) = 𝓝[range f] (f a);
• add inducing.is_closed_iff;
• move old embedding.map_nhds_eq to embedding.map_nhds_of_mem, the new embedding.map_nhds_eq says map f (𝓝 a) = 𝓝[range f] (f a);
• add open_embedding.map_nhds_eq;
• change signature of is_closed_induced_iff to match other similar lemmas;
• move old map_nhds_induced_eq to map_nhds_induced_of_mem, the new map_nhds_induced_eq give 𝓝[range f] (f a) instead of 𝓝 (f a).