Commit 2022-06-26 04:37 ccb1cf38

feat(data/set/lattice): Preimages are disjoint iff the sets are disjoint (#14951) Prove disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ disjoint s t and disjoint (f '' s) (f '' t) ↔ disjoint s t when f is surjective/injective. Delete set.disjoint_preimage in favor of disjoint.preimage. Fix the statement of set.preimage_eq_empty_iff (the name referred to the RHS).