proposition: Lemma linear_continuous (R : realFieldType) (U : normedModType R) (V : normedModType R) (f : {linear U -> V}) : (f : _ -> _) =O_ (0 : U) (cst (1 : R^o)) -> continuous f.
proof: Proof. by apply: linear_for_continuous => ? ?; rewrite normrZ. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule