mathlib

fef4fb83 - refactor(topology/inseparable): redefine `specializes` and `inseparable` (#14647)

refactor(topology/inseparable): redefine `specializes` and `inseparable` (#14647) * Redefine `specializes` and `inseparable` in terms of `nhds`. * Review API. * Define `inseparable_setoid` and `separation_quotient`. * Add `function.surjective.subsingleton`.