mathlib3

refactor(topology/*): define and use dense_inducing

#1193

Merged