proposition: Lemma bigO_class (F : set_system T) (g : T -> W) (f : {O_F g}) : `[< bigO_def F f g >].
proof: Proof. by case: f => ?. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule