Theorem topological_space.tendsto_prod_mk_nhds

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