mathlib3

3e77124c - refactor(topology/{separation,subset_properties}): use `set.subsingleton` (#12232)

refactor(topology/{separation,subset_properties}): use `set.subsingleton` (#12232) Use `set.subsingleton s` instead of `_root_.subsingleton s` in `is_preirreducible_iff_subsingleton` and `is_preirreducible_of_subsingleton`, rename the latter to `set.subsingleton.is_preirreducible`.