proposition: Lemma normal_uniform_separator (B : set T) : closed A -> closed B -> A `&` B = set0 -> uniform_separator A B.
proof: Proof. move=> clA clB AB0; have /(_ (~`B))[x Ax|] := normalT clA. apply: open_nbhs_nbhs; split => //. - exact/closed_openC. - by move: x Ax; apply/ disjoints_subset. move=> V /set_nbhsP [U [oU AU UV]] cVcb. exists (Uniform.class urysohnType), (apxU (U, ~` B)); split => //. - move=> ?; apply:sub_gen_smallest; exists (U, ~`B) => //; split => //=. exact/closed_openC. by move: UV => /closure_subset/subset_trans; apply. - rewrite eqEsubset; split; case=> // a b [/=[Aa Bb] [[//]|]]. by have /subset_closure ? := AU _ Aa; case. move=> x ? [E gE] /(@filterS T); apply; move: gE. rewrite /= /ury_unif filterI_iterE; case => K /= [i _] /= uiK KE. suff : @nbhs T T x to_set K (x) by apply: filterS => y /KE. elim: i K uiK {E KE}; last by move=> ? H ? [N] /H ? [M] /H ? <-; apply: filterI. move=> K [->|]; first exact: filterT. move=> [[/= P Q] [/= oP oQ AP cPQ <-]]; rewrite /apxU /=. set M := [set y | _ \/ _]. have [Qx|nQx] := pselect (Q x); first last. suff -> : M = ~` closure P. apply: open_nbhs_nbhs; split; first exact/closed_openC/closed_closure. by move/cPQ. rewrite eqEsubset /M; split => z; first by do 2!case. by move=> ?; right; split => // /cPQ. have [nPx|cPx] := pselect (closure P x). suff -> : M = Q by apply: open_nbhs_nbhs; split. rewrite eqEsubset /M; split => z; first by do 2!case. by move=> ?; left; split. suff -> : M = setT by exact: filterT. rewrite eqEsubset; split => // z _. by have [Qz|/(subsetC cPQ)] := pselect (Q z); constructor. 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