minor generalization

[affeldt-aist]

Motivation for this change

This generalizes bigcupT_measurable_ratto any choiceType whose whole set is countable.
I didn't prove a version with countType because I didn't manage to generalize the
quasi_canonical machinery. Anyway, that doesn't make the lemma less general. @CohenCyril

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[CohenCyril]

Actually there is no reason to assume a choice type (it is not used in the statement), so I would do:

Suggested change

	Lemma countable_bigcupT_measurable d (T : sigmaRingType d) (U : choiceType)
	(F : U -> set T) : countable [set: U] ->
	(forall i, measurable (F i)) -> measurable (\bigcup_i F i).
	Proof.
	elim/choicePpointed: U => U in F *.
	by move=> _ _; rewrite empty_eq0 bigcup0.
	Lemma countable_bigcupT_measurable d (T : sigmaRingType d) U
	(F : U -> set T) : countable [set: U] ->
	(forall i, measurable (F i)) -> measurable (\bigcup_i F i).
	Proof.
	elim/Ppointed: U => U in F *; first by move=> *; rewrite empty_eq0 bigcup0.