proposition: Lemma near_map2 {T T' U U'} (f : T -> U) (g : T' -> U') (F : set_system T) (G : set_system T') (P : U -> set U') : Filter F -> Filter G -> (\forall y \near f @ F & y' \near g @ G, P y y') = (\forall x \near F & x' \near G , P (f x) (g x')).
proof: Proof. move=> FF FG; rewrite propeqE; split=> -[[A B] /= [fFA fGB] ABP]. exists (f @^-1` A, g @^-1` B) => //= -[x y /=] xyAB. by apply: (ABP (_, _)); apply: xyAB. exists (f @` A, g @` B) => //=; last first. by move=> -_ [/= [x Ax <-] [x' Bx' <-]]; apply: (ABP (_, _)). rewrite !nbhs_simpl /fmap /=; split. by apply: filterS fFA=> x Ax; exists x. by apply: filterS fGB => x Bx; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed