Pull Request to Mathlib about the definition of regular_spaces and some basic propositions.