proposition: Lemma bigThetaE {W} (F : filter_on T) (f : T -> V) (g : T -> W) : (f \is 'Theta_F(g)) = (f =O_F g /\ f \is 'Omega_F(g)) :> Prop.
proof: Proof. rewrite propeqE; split. - rewrite qualifE => /asboolP[[/= k1 k2] /andP[k10 k20]] /near_andP[Hx1 Hx2]. by split; [rewrite eqO_exP; exists k2| rewrite qualifE; apply/asboolP; exists k1]. - case; rewrite eqO_exP qualifE => -[k1 k10 H1] /asboolP[k2 k20 H2]. rewrite qualifE; apply/asboolP; exists (k2, k1) => /=; first by rewrite k20. by apply/near_andP; split. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule