proposition: Lemma weak_sep_openE : @open T = @open weakT.
proof: Proof. rewrite predeqE => A; rewrite ?openE /interior. by split => + z => /(_ z); rewrite weak_sep_nbhsE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed