proposition: Lemma entourage_close (x y : U) : close x y = forall A, entourage A -> A (x, y).
proof: Proof. rewrite propeqE; split=> [cxy A entA|cxy]. have /entourage_split_ent entsA := entA; rewrite closeEnbhs in cxy. have yl := nbhs_entourage _ (entourage_inv entsA). have yr := nbhs_entourage _ entsA. have [z [zx zy]] := cxy _ _ (yr x) (yl y). exact: (entourage_split z). rewrite closeEnbhs => A B /nbhsP[E1 entE1 sE1A] /nbhsP[E2 entE2 sE2B]. by exists y; split;[apply: sE1A; apply: cxy|apply: sE2B; apply: entourage_refl]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed