proposition: Lemma nbhs_interior (p : T) (A : set T) : nbhs p A -> nbhs p A^°.
proof: Proof. rewrite nbhsE /open_nbhs openE => - [B [Bop Bp] sBA]. by exists B => // q Bq; apply: filterS sBA _; apply: Bop. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed