Commit 2023-01-27 11:49 fedcb65c

feat(set_theory/zfc/basic): more trivial results (#18294) This PR does multiple very simple things at once. Here's a rundown.

• Golf Set.eq_empty.
• Add Set.eq_empty_or_nonempty, Set.insert_nonempty, Set.singleton_nonempty, Class.mem_def, Class.not_empty_hom, Class.univ_hom, Class.empty_Cong_to_Class, Class.empty_Class_to_Cong.
• Tag Class.mem_univ as simp.
• Move Set.to_set_sUnion and Set.sUnion_empty, so that the theorems on singleton injectivity aren't interspersed with the union results.