Commit 2022-07-12 16:39 9c400932

chore(*): improve some definitional equalities (#15083)

• add set.mem_diagonal_iff, move simp from set.mem_diagonal;
• add @[simp] to set.prod_subset_compl_diagonal_iff_disjoint;
• redefine sum.map in terms of sum.elim, add sum.map_inl and sum.map_inr;
• redefine sum.swap in terms of sum.elim, add sum.swap_inl and sum.swap_inr;
• use lift_rel_swap_iff to prove swap_le_swap and swap_lt_swap;
• redefine equiv.sum_prod_distrib and equiv.sigma_sum_distrib in terms of sum.elim and sum.map;
• add filter.compl_diagonal_mem_prod;
• rename continuous_sum_rec to continuous.sum_elim, use sum.elim in the statement;
• add continuous.sum_map;
• golf homeomorph.sum_congr and homeomorph.sum_prod_distrib.