proposition: Lemma measurable_fun_infs D (h : (T -> R)^nat) n : (forall t, D t -> has_lbound (range (h ^~ t))) -> (forall n, measurable_fun D (h n)) -> measurable_fun D (fun x => infs (h ^~ x) n).
proof: Proof. move=> lb_f mf mD; apply: (measurability (RGenInftyO.measurableE R)) =>//. move=> _ [_ [x ->] <-]; rewrite infs_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