proposition: Lemma bounded_fun_has_ubound (T : Type) (R : realFieldType) (a : T -> R) : bounded_fun a -> has_ubound (range a).
proof: Proof. move=> [M [Mreal]]/(_ (`|M| + 1)). rewrite (le_lt_trans (ler_norm _)) ?ltrDl// => /(_ erefl) aM. by exists (`|M| + 1) => _ [n _ <-]; rewrite (le_trans (ler_norm _))// aM. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule