proposition: Lemma uniform_separatorW {T : uniformType} (A B : set T) : (exists2 E, entourage E & A `*` B `&` E = set0) -> uniform_separator A B.
proof: Proof. by case=> E entE AB0; exists (Uniform.class T), E; split => // ?. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule