mathlib

0950ba3d - refactor(topology/separation): rename `indistinguishable` to `inseparable` (#14401)

refactor(topology/separation): rename `indistinguishable` to `inseparable` (#14401) * Replace `indistinguishable` by `inseparable` in the definition and lemma names. The word "indistinguishable" is too generic. * Rename `t0_space_iff_distinguishable` to `t0_space_iff_not_inseparable` because the name `t0_space_iff_separable` is misleading, slightly golf the proof. * Add `t0_space_iff_nhds_injective`, `nhds_injective`, reorder lemmas around these two.