proposition: Lemma open_nbhsI (p : T) (A B : set T) : open_nbhs p A -> open_nbhs p B -> open_nbhs p (A `&` B).
proof: Proof. by move=> [Aop Ap] [Bop Bp]; split; [apply: openI|split]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed