proposition: Lemma linear_eqO (V' W' : normedModType R) (f : {linear V' -> W'}) : continuous f -> (f : V' -> W') =O_ (0 : V') id.
proof: Proof. move=> /linear_lipschitz [k kgt0 flip]; apply/eqO_exP; exists k => //. exact: filterE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms