proposition: Lemma nbhs_subspace_ex (U : set T) (x : T) : A x -> nbhs (x : subspace A) U <-> exists2 V, nbhs (x : T) V & U `&` A = V `&` A.
proof: Proof. by case: (nbhs _) / nbhs_subspaceP; rewrite // ?withinE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed