proposition: Lemma measurable_fun_limn_esup D (f : (T -> \bar R)^nat) : (forall n, measurable_fun D (f n)) -> measurable_fun D (fun x => limn_esup (f ^~ x)).
proof: Proof. move=> mf mD; rewrite (_ : (fun _ => _) = (fun x => ereal_inf [set esups (f^~ x) n | n in [set n | n >= 0]%N])). by apply: measurable_fun_einfs => // k; exact: measurable_fun_esups. rewrite funeqE => t; rewrite limn_esup_lim; apply/cvg_lim => //. rewrite [X in _ --> X](_ : _ = ereal_inf (range (esups (f^~t)))). exact: cvg_esups_inf. by congr (ereal_inf [set _ | _ in _]); rewrite predeqE. 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