mathlib3

4dd837dc - refactor(topology/sequences): redefine `is_seq_closed`, define Fréchet-Urysohn spaces (#15953)

refactor(topology/sequences): redefine `is_seq_closed`, define Fréchet-Urysohn spaces (#15953) * redefine `is_seq_closed` as "the set contains every limit of a sequence of points from this set"; * delete `is_seq_closed_of_def` and `is_seq_closed.mem_of_tendsto`, because now we use this property as the definition; * rename `sequential_space` to `frechet_urysohn_space`, add new `sequential_space`; this way our definitions agree with textbooks.