proposition: Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f.
proof: Proof. have /finite_seqP[r fr] := fimfunP f. exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)). split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx). have ? : f z \in r by have := imageT f z; rewrite fr. rewrite -[leLHS]/(fine `|f z|%:E) fine_le//. have := @bigmaxe_fin_num _ (map normr r) `|f z|. by rewrite big_map => ->//; apply/mapP; exists (f z). by rewrite (bigmax_sup_seq _ _ (lexx _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun