naming of `preimage_classes`

[affeldt-aist]

analysis/theories/measure.v

Line 5041 in f788745

Definition preimage_classes d1 d2

should maybe be renamed preimage_class_prod or preimage_class_pair to clarify that it is about two classes.

[affeldt-aist]

Or maybe g_sigma_algebra_family2 because this is a special case of a sigma-algebra generated by n mappings (with n = 2) (not using the string "mapping" in the identifier @t6s )

[affeldt-aist]

This has been taken care of by PR #1443
(preimage_classes -> g_sigma_preimageU)