proposition: Lemma nbhs_subspaceT (x : T) : nbhs (x : subspace setT) = nbhs x.
proof: Proof. have [_|] := nbhs_subspaceP [set: T]; last by cbn. rewrite eqEsubset withinE; split => [W [V nbhsV]|W ?]; last by exists W. by rewrite 2!setIT => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed