proposition: Lemma filter2P T U (F : set_system T) (G : set_system U) {FF : Filter F} {FG : Filter G} (P : set (T * U)) : (exists2 Q : set T * set U, F Q.1 /\ G Q.2 & forall (x : T) (y : U), Q.1 x -> Q.2 y -> P (x, y)) <-> \forall x \near (F, G), P x.
proof: Proof. split=> [][[A B] /=[FA GB] ABP]; exists (A, B) => //=. by move=> [a b] [/=Aa Bb]; apply: ABP. by move=> a b Aa Bb; apply: (ABP (_, _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed