proposition: Lemma bounded_linear_continuous (f : {linear V -> W}) : bounded_near f (nbhs (0 : V)) -> continuous f.
proof: Proof. move=> /linear_boundedP [y [yreal fr]] x; near +oo_R => r. apply/(@cvgrPdist_lt _ _ _ (nbhs x)) => e e_gt0; near=> z; rewrite -linearB. rewrite (le_lt_trans (fr r _ _))// -?ltr_pdivlMl//. by near: z; apply: cvgr_dist_lt => //; rewrite mulrC divr_gt0. Unshelve. all: by end_near. 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