diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 56017a4e2..e5a20cd80 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -33,7 +33,10 @@ + lemma `integral_measure_add` - in `probability.v` - + lemma `integral_distribution` (existsing lemma `integral_distribution` has been renamed) + + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed) + +- in `measure.v`: + + lemma `countable_bigcupT_measurable` ### Changed diff --git a/classical/classical_sets.v b/classical/classical_sets.v index e4dc9adeb..e5e7579d2 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2602,6 +2602,7 @@ Proof. by apply: qcanon; elim/eqPchoice; elim/choicePpointed => [[T F]|T]; [left; exists (Empty.Pack F) | right; exists T]. Qed. + Lemma Ppointed : quasi_canonical Type pointedType. Proof. by apply: qcanon; elim/Peq; elim/eqPpointed => [[T F]|T]; diff --git a/theories/measure.v b/theories/measure.v index 691b79f9b..702cd1d65 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1390,11 +1390,22 @@ Qed. End sigma_ring_lambda_system. +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. +move=> /countable_bijP[B] /ppcard_eqP[f] Fm. +rewrite (reindex_bigcup f^-1%FUN setT)//=; first exact: bigcupT_measurable. +exact: (@subl_surj _ _ B). +Qed. + Lemma bigcupT_measurable_rat d (T : sigmaRingType d) (F : rat -> set T) : (forall i, measurable (F i)) -> measurable (\bigcup_i F i). Proof. -move=> Fm; have /ppcard_eqP[f] := card_rat. -by rewrite (reindex_bigcup f^-1%FUN setT)//=; exact: bigcupT_measurable. +apply: countable_bigcupT_measurable. +by apply/countable_bijP; exists setT; exact: card_rat. Qed. Section measurable_lemmas.