proposition: Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) : {near F, f =2 g} -> g `@ F `=>` f `@ F.
proof: Proof. move=> eq_fg P /=; apply: filterS2 eq_fg => x eq_fg [y [fxy Py]]. by exists y; rewrite -eq_fg. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed