proposition: Lemma within_interior (x : T) : A^° x -> within A (nbhs x) = nbhs x.
proof: Proof. move=> Aox; rewrite eqEsubset; split; last exact: cvg_within. rewrite ?nbhsE => W /= => [[B + BsubW]]. rewrite open_nbhsE => [[oB nbhsB]]. exists (B `&` A^°); last by move=> t /= [] /BsubW + /interior_subset; apply. rewrite open_nbhsE; split; first by apply: openI => //; exact: open_interior. by apply: filterI => //; move:(open_interior A); rewrite openE; exact. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed