move `preimage_set_system` to `classical_sets.v`?

[affeldt-aist]

analysis/theories/measure_theory/measurable_structure.v

Line 1307 in bd05c57

Definition preimage_set_system {aT rT : Type} (D : set aT) (f : aT -> rT)

It is not specific to measure theory and would enable the definition of

Definition cross X Y :=
  preimage_set_system [set: T1 * T2] fst X
  `|` preimage_set_system [set: T1 * T2] snd Y.

inside classical_sets.v where it intuitively belongs.

@shinya-katsumata