Commit 2020-12-22 17:05 0ff90682
View on Github →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.