proposition: Lemma eqOmegaE (F : filter_on T) (f e : T -> V) : (f =Omega_F(e)) = (f \is 'Omega_F(e)).
proof: Proof. rewrite propeqE; split=> [->|]; rewrite qualifE; last first. by move=> H; rewrite /the_bigOmega val_insubd H. by apply/asboolP; rewrite /the_bigOmega val_insubd; case: ifPn => // /asboolP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule