proposition: Lemma filter_pair_near_of (T T' : Type) (F : set_system T) (F' : set_system T') : Filter F -> Filter F' -> forall (P : @in_filter T F) (P' : @in_filter T' F') (Q : set (T * T')), (forall x x', prop_of P x -> prop_of P' x' -> Q (x, x')) -> filter_prod F F' Q.
proof: Proof. move=> FF FF' [P FP] [P' FP'] Q PQ; rewrite prop_ofE in FP FP' PQ. by exists (P, P') => //= -[t t'] [] /=; exact: PQ. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed