proposition: Lemma measurable_fun_sups D (h : (T -> R)^nat) n : (forall t, D t -> has_ubound (range (h ^~ t))) -> (forall m, measurable_fun D (h m)) -> measurable_fun D (fun x => sups (h ^~ x) n).
proof: Proof. move=> f_ub mf mD; apply: (measurability (RGenOInfty.measurableE R)) => //. move=> _ [_ [x ->] <-]; rewrite sups_preimage // setI_bigcupr. by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure