proposition: Lemma linear_for_continuous (f : {linear U -> V | GRing.Scale.Law.sort s}) : (f : _ -> _) =O_ (0 : U) (cst (1 : R^o)) -> continuous f.
proof: Proof. move=> /eqO_exP [_/posnumP[k0] Of1] x. apply/cvgrPdist_lt => _/posnumP[e]; rewrite !near_simpl. rewrite (near_shift 0) /= subr0; near=> y => /=. rewrite -linearB opprD addrC addrNK linearN normrN; near: y. suff flip : \forall k \near +oo, forall x, `|f x| <= k * `|x|. near +oo => k; near=> y. rewrite (le_lt_trans (near flip k _ _)) // -ltr_pdivlMl; last first. by near: k; exists 0. near: y; apply/nbhs_normP. eexists; last by move=> ?; rewrite /= sub0r normrN; apply. by rewrite /= mulr_gt0 // invr_gt0; near: k; exists 0. have /nbhs_normP [_/posnumP[d]] := Of1. rewrite /cst [X in _ * X]normr1 mulr1 => fk; near=> k => y. case: (ler0P `|y|) => [|y0]. by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0. have ky0 : 0 <= k0%:num / (k * `|y|). by rewrite pmulr_rge0 // invr_ge0 mulr_ge0 // ltW //; near: k; exists 0. rewrite -[leRHS]mulr1 -ler_pdivrMl ?pmulr_rgt0 //. rewrite -(ler_pM2l [gt0 of k0%:num]) mulr1 mulrA -[_ / _]ger0_norm //. rewrite -normm_s. rewrite -linearZ fk //= /= distrC subr0 normrZ ger0_norm //. rewrite invfM mulrA mulfVK ?lt0r_neq0 // ltr_pdivrMr //. by rewrite -ltr_pdivrMl//. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule