proposition: Lemma continuous_linear_bounded (x : V) (f : {linear V -> W}) : {for 0, continuous f} -> bounded_near f (nbhs x).
proof: Proof. rewrite /prop_for/continuous_at linear0 /bounded_near => f0. near=> M; apply/nbhs0P. near do rewrite /= linearD (le_trans (ler_normD _ _))// -lerBrDl. by apply: cvgr0_norm_le; rewrite // subr_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