mathlib3

0ff90682 - feat(data/finset/basic, topology/separation): add induction_on_union, separate, and separate_finset_of_t2 (#5332)

feat(data/finset/basic, topology/separation): add induction_on_union, separate, and separate_finset_of_t2 (#5332) prove lemma disjoint_finsets_opens_of_t2 showing that in a t2_space disjoint finsets have disjoint open neighbourhoods, using auxiliary lemma not_mem_finset_opens_of_t2.