proposition: Lemma open_subspace1out (x : subspace A) : ~ A x -> open [set x].
proof: Proof. move=> /nbhs_subspace_out E; have : nbhs x [set x] by rewrite /nbhs //= -E. rewrite nbhsE => [[U []]] oU Ux Usub; suff : U = [set x] by move=> <-. by rewrite eqEsubset; split => // t ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed