Commit 2021-04-27 11:31 18403ac8

feat(topology/separation): change regular_space definition, added t1_characterisation and definition of Urysohn space (#7367) This PR changes the definition of regular_space becouse the previous definition requests t1_space and it's posible to only require t0_space as a condition. Due to that change, we had to reformulate the prove of the lemma separed_regular in src/topology/uniform_space/separation.lean adding the t0 condition. We've also define the Uryson space , with his respectives lemmas about the relation with T_2 and T_3, and prove the relation between the definition of t1_space from mathlib and the common definition with open sets.