proposition: Lemma bigO_exP (F : set_system T) (f : T -> V) (g : T -> W) : Filter F -> bigO_ex_def F f g <-> bigO_def F f g.
proof: Proof. split=> [[k k0 fOg] | [k [kreal fOg]]]. exists k; rewrite realE (ltW k0) /=; split=> // l ltkl; move: fOg. by apply: filter_app; near=> x => /le_trans; apply; rewrite ler_wpM2r // ltW. exists (Num.max 1 `|k + 1|) => //. apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //. by rewrite (@lt_le_trans _ _ (k + 1)) ?ltrDl // real_ler_norm ?realD. by rewrite comparable_le_maxr ?real_comparable// lexx orbT. Unshelve. end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule