proposition: Lemma eqOmegaO {W} (F : filter_on T) (f : T -> V) (e : T -> W) : (f \is 'Omega_F(e)) = (e =O_F f) :> Prop.
proof: Proof. rewrite propeqE; split => [| /eqO_exP[x x0 Hx] ]; [rewrite qualifE => /asboolP[x x0 Hx]; apply/eqO_exP | rewrite qualifE; apply/asboolP]; exists x^-1; rewrite ?invr_gt0 //; near=> y. by rewrite ler_pdivlMl //; near: y. by rewrite ler_pdivrMl //; near: y. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule