proposition: Lemma nbhs_subspace_subset A B (x : T) : A `<=` B -> nbhs (x : subspace B) `<=` nbhs (x : subspace A).
proof: Proof. rewrite /= => AB; case: (nbhs_subspaceP A); case: (nbhs_subspaceP B). - by move=> ? ?; apply: within_subset => //=; exact: (nbhs_filter x). - by move=> ? /AB. - by move=> Bx ? W /nbhs_singleton /(_ Bx) ? ? ->. - by move=> ? ?. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed