proposition: Lemma fcvg_ball2P {F : set_system U} {G : set_system V} {FF : Filter F} {FG : Filter G} (y : U) (z : V): (F, G) --> (y, z) <-> forall eps : R, eps > 0 -> \forall y' \near F & z' \near G, ball y eps y' /\ ball z eps z'.
proof: Proof. exact: fcvg_ballP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed