Theorem filter.le_map_comap'

refactor(topology): topological_space.induced resembles set.image; second_countable_topology on subtypes; simplify filter.map_comap

order(filter): rename `vmap` to `comap`