proposition: Lemma fmap_within_eq {S : topologicalType} (F : set_system T) (f g : T -> S) : Filter F -> {in A, f =1 g} -> f @ within A F --> g @ within A F.
proof: Proof. move=> FF feq U /=; near_simpl; apply: filter_app. rewrite ?nbhs_simpl; near_simpl; near=> w; rewrite (feq w) // inE. exact: (near (withinT A FF) w). Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed