proposition: Lemma uniform_separatorP {T : topologicalType} {R : realType} (A B : set T) : uniform_separator A B <-> exists (f : T -> R), [/\ continuous f, range f `<=` `[0, 1], f @` A `<=` [set 0] & f @` B `<=` [set 1]].
proof: Proof. split; first do [move=> ?; exists (Urysohn A B); split]. - exact: Urysohn_continuous. - exact: Urysohn_range. - exact: Urysohn_sub0. - exact: Urysohn_sub1. case=> f [ctsf f01 fA0 fB1]. pose T' := weak_topology f. exists (Uniform.class T'), ([set xy | ball (f xy.1) 1 (f xy.2)]); split. - exists [set xy | ball xy.1 1 xy.2]; last by case. by rewrite -entourage_ballE; exists 1 => //=. - rewrite -subset0 => -[a b [[/= Aa Bb]]]. by rewrite (imsub1 fA0)// (imsub1 fB1)// /ball/= sub0r normrN normr1 ltxx. - move=> x U [V [[W oW <- /=]]] ? /filterS; apply; apply: ctsf. exact: open_nbhs_nbhs. 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