proposition: Lemma bounded_funP (f : {linear V -> W}) : (forall r, exists M, forall x, `|x| <= r -> `|f x| <= M) <-> bounded_near f (nbhs (0 : V)).
proof: Proof. split => [/(_ 1) [M Bf]|/linear_boundedP fr y]. apply/ex_bound; exists M; apply/nbhs_normP => /=; exists 1 => //= x /=. by rewrite sub0r normrN => x1; exact/Bf/ltW. near +oo_R => r; exists (r * y) => x xe. rewrite (@le_trans _ _ (r * `|x|)) //; first by move: {xe} x; near: r. by rewrite ler_pM //. 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