proposition: Lemma bounded_fun_has_lbound (T : Type) (R : realFieldType) (a : T -> R) : bounded_fun a -> has_lbound (range a).
proof: Proof. move=> /bounded_funN/bounded_fun_has_ubound ba; apply/has_lb_ubN. by apply: subset_has_ubound ba => _ [_ [n _] <- <-]; exists n. 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