proposition: Lemma meets_openr {T : topologicalType} (F : set_system T) (x : T) : F `#` nbhs x = F `#` open_nbhs x.
proof: Proof. rewrite propeqE; split; [exact/meetsSr/open_nbhs_nbhs|]. by move=> P A B {}/P P; rewrite nbhsE => -[B' /P + sB]; apply: subsetI_neq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed