mathlib

f33b0847 - feat(topology/separation): generalize a lemma (#14154)

feat(topology/separation): generalize a lemma (#14154) * generalize `nhds_eq_nhds_iff` from a `[t1_space α]` to a `[t0_space α]`; * relate `indistinguishable` to `nhds`.