proposition: Lemma nbhs_subspace_interior (x : T) : A^° x -> nbhs x = (nbhs (x : subspace A)).
proof: Proof. move=> /[dup] /[dup] /interior_subset ? /within_interior <- ?. by case: RHS / nbhs_subspaceP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed