proposition: Lemma filter_pair_set (T T' : Type) (F : set_system T) (F' : set_system T') : Filter F -> Filter F' -> forall (P : set T) (P' : set T') (Q : set (T * T')), (forall x x', P x -> P' x' -> Q (x, x')) -> F P /\ F' P' -> filter_prod F F' Q.
proof: Proof. by move=> FF FF' P P' Q PQ [FP FP']; near=> x do [have := PQ x.1 x.2; rewrite -surjective_pairing; apply]; [apply: cvg_fst | apply: cvg_snd]. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed