proposition: Fact is_bigOmega_key {W} (F : set_system T) (g : T -> W) : pred_key (is_bigOmega F g).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule