proposition: Lemma weak_sep_nbhsE x : @nbhs T T x = @nbhs T weakT x.
proof: Proof. rewrite predeqE => U; split; move: U. by have P := weak_sep_cvg x (nbhs_filter (x : weakT)); exact/P. by have P := weak_sep_cvg x (nbhs_filter (x : T)); exact/P. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed