proposition: Lemma cvg_ball2P {I J} {F : set_system I} {G : set_system J} {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V): (f @ F, g @ G) --> (y, z) <-> forall eps : R, eps > 0 -> \forall i \near F & j \near G, ball y eps (f i) /\ ball z eps (g j).
proof: Proof. rewrite fcvg_ball2P; split=> + e e0 => /(_ e e0). by rewrite near_map2; apply. by move=> fgyz; rewrite near_map2; apply: fgyz. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed