proposition: Lemma bigThetaP {W} (F : set_system T) (g : T -> W) (f : {Theta_F g}) : bigTheta_def F f g.
proof: Proof. exact/asboolP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule