mathlib

ccb1cf38 - feat(data/set/lattice): Preimages are disjoint iff the sets are disjoint (#14951)

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).