Commit 2022-06-28 00:05 37bf8a2e

chore(topology/separation): Extract set product lemma (#14958) Move prod_subset_compl_diagonal_iff_disjoint to data.set.prod, where it belongs. Delete diagonal_eq_range_diagonal_map because it duplicates set.diagonal_eq_range. Move set.disjoint_left/set.disjoint_right to data.set.basic to avoid an import cycle. Make variable semi-implicit in the RHS of disjoint_left and disjoint_right.