proposition: Lemma close_cvgxx (x y : U) : close x y -> x --> y.
proof: Proof. rewrite entourage_close => cxy P /= /nbhsP[A entA sAP]. apply/nbhsP; exists (split_ent A) => // z xz; apply: sAP. apply: (entourage_split x) => //. by have := cxy _ (entourage_inv (entourage_split_ent entA)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed