mathlib

ede73b25 - refactor(topology/separation): rename `regular_space` to `t3_space` (#15169)

refactor(topology/separation): rename `regular_space` to `t3_space` (#15169) I'm going to add a version of `regular_space` without `t0_space` and prove, e.g., that any uniform space is a regular space in this sense. To do this, I need to rename the existing `regular_space`.