proposition: Lemma ball_hausdorff : hausdorff_space T = forall (a b : T), a != b -> exists r : {posnum R} * {posnum R}, ball a r.1%:num `&` ball b r.2%:num == set0.
proof: Proof. rewrite propeqE open_hausdorff; split => T2T a b /T2T[[/=]]. move=> A B; rewrite 2!inE => [[aA bB] [oA oB /eqP ABeq0]]. have /nbhs_ballP[_/posnumP[r] rA]: nbhs a A by apply: open_nbhs_nbhs. have /nbhs_ballP[_/posnumP[s] rB]: nbhs b B by apply: open_nbhs_nbhs. by exists (r, s) => /=; rewrite (subsetI_eq0 _ _ ABeq0). move=> r s /eqP brs_eq0; exists ((ball a r%:num)^°, (ball b s%:num)^°) => /=. split; by rewrite inE; apply: nbhs_singleton; apply: nbhs_interior; apply/nbhs_ballP; apply: in_filter_from => /=. split; do ?by apply: open_interior. by rewrite (subsetI_eq0 _ _ brs_eq0)//; apply: interior_subset. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed