proposition: Lemma ent_closure {M : uniformType} (x : M) E : entourage E -> closure (to_set (split_ent E) x) `<=` to_set E x.
proof: Proof. pose E' := (split_ent E) `&` ((split_ent E)^-1)%classic. move=> entE z /(_ [set y | E' (z, y)])[]. by rewrite -nbhs_entourageE; exists E' => //; exact: filterI. by move=> y [/=] + [_]; exact: entourage_split. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed