proposition: Lemma nearP_dep {T U} {F : set_system T} {G : set_system U} {FF : Filter F} {FG : Filter G} (P : T -> U -> Prop) : (\forall x \near F & y \near G, P x y) -> \forall x \near F, \forall y \near G, P x y.
proof: Proof. move=> [[Q R] [/=FQ GR]] QRP. by apply: filterS FQ => x Q1x; apply: filterS GR => y Q2y; apply: (QRP (_, _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed