proposition: Lemma hausdorrf_close_eq_in (A : set U) (f g : {uniform` A -> V}) : hausdorff_space V -> close f g = {in A, f =1 g}.
proof: Proof. move=> hV. rewrite propeqE; split; last exact: eq_in_close. rewrite entourage_close => C u; rewrite inE => uA; apply: hV. rewrite /cluster -nbhs_entourageE /= => X Y [X' eX X'X] [Y' eY Y'Y]. exists (g u); split; [apply: X'X| apply: Y'Y]; last exact: entourage_refl. apply: (C [set fg | forall y, A y -> X' (fg.1 y, fg.2 y)]) => //=. by rewrite uniform_entourage; exists X'. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed