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)`.
