proposition: Lemma withinE F : Filter F -> within A F = [set U | exists2 V, F V & U `&` A = V `&` A].
proof: Proof. move=> FF; rewrite eqEsubset; split=> U. move=> Wu; exists [set x | A x -> U x] => //. by rewrite eqEsubset; split => t [L R]; split=> //; apply: L. move=> [V FV AU]; rewrite /within /prop_near1 nbhs_simpl/=; near=> w => Aw. by have []// : (U `&` A) w; rewrite AU; split => //; apply: (near FV). 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