naming of measurable lemmas

[affeldt-aist]

This one is called bigsetU_measurable
while this one is called measurable_bigcup.
Should the former follow the naming of the latter?

[CohenCyril]

• bigsetU_measurable is the good name for this lemma.
• measurable_bigcup is not a lemma: it's a field of a factory, and as of now it cannot be used outside of a builder section. However, for consitency and in anticipation of potential named based future features of HB, it could and should be renamed to follow the conventions of the former, i.e. bigcup_measurable.