proposition: Lemma entourage_E {R : numDomainType} {T T'} (ball : T -> R -> set T') : entourage_ ball = @filter_from R _ [set x | 0 < x] (fun e => [set xy | ball xy.1 e xy.2]).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed