proposition: Lemma measurable_fun_bool D (f : T1 -> bool) b : measurable (f @^-1` [set b]) -> measurable_fun D f.
proof: Proof. have FNT : [set false] = [set~ true] by apply/seteqP; split => -[]//=. wlog {b}-> : b / b = true. case: b => [|h]; first exact. by rewrite FNT -preimage_setC => /measurableC; rewrite setCK; exact: h. move=> mfT mD /= Y; have := @subsetT _ Y; rewrite setT_bool => YT. have [-> _|-> _|-> _ |-> _] := subset_set2 YT. - by rewrite preimage0 ?setI0. - by apply: measurableI => //; exact: mfT. - rewrite -[X in measurable X]setCK; apply: measurableC; rewrite setCI. apply: measurableU; first exact: measurableC. by rewrite FNT preimage_setC setCK; exact: mfT. - by rewrite -setT_bool preimage_setT setIT. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)