proposition: Lemma linear_boundedP (f : {linear V -> W}) : bounded_near f (nbhs 0) <-> \forall r \near +oo, forall x, `|f x| <= r * `|x|.
proof: Proof. split=> [|/pinfty_ex_gt0 [r r0 Bf]]; last first. apply/ex_bound; exists r; apply/nbhs_norm0P; exists 1 => //= x /=. by rewrite -(gtr_pMr _ r0) => /ltW; exact/le_trans/Bf. rewrite /bounded_near => /pinfty_ex_gt0 [M M0 /nbhs_norm0P [_/posnumP[e] efM]]. near (0 : R)^'+ => d; near=> r => x. have[->|x0] := eqVneq x 0; first by rewrite raddf0 !normr0 mulr0. have nd0 : d / `|x| > 0 by rewrite divr_gt0 ?normr_gt0. have: `|f (d / `|x| *: x)| <= M. by apply: efM => /=; rewrite normrZ gtr0_norm// divfK ?normr_eq0//. rewrite linearZ/= normrZ gtr0_norm// -ler_pdivlMl//; move/le_trans; apply. rewrite invfM invrK mulrAC ler_wpM2r//; near: r; apply: nbhs_pinfty_ge. by rewrite rpredM// ?rpredV ?gtr0_real. 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