Theorem ennreal.coe_image_univ_mem_nhds

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

refactor(data/real/nnreal): derive order structure for ennreal from with_top nnreal