proposition: Lemma eqOEx (F : filter_on T) (f : T -> V) h (e : T -> W) : (forall x, f x = mkbigO a_tag F h e x) -> (forall x, f x =O_(x \near F) e x).
proof: Proof. by have := @eqOE F f h e; rewrite !funeqE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule