Theorem topological_space.prod_mem_nhds_sets

refactor(analysis): add nndist; add finite product of metric spaces; prepare for normed spaces

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