proposition: Lemma open_hausdorff : hausdorff_space T = forall x y, x != y -> exists2 AB, (x \in AB.1 /\ y \in AB.2) & [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0].
proof: Proof. rewrite propeqE; split => [T_filterT2|T_openT2] x y. have := contra_not (T_filterT2 x y); rewrite (rwP eqP) (rwP negP). move=> /[apply] /asboolPn/existsp_asboolPn[A]; rewrite -existsNE => -[B]. rewrite [nbhs _ _ -> _](rwP imply_asboolP) => /negP. rewrite asbool_imply !negb_imply => /andP[/asboolP xA] /andP[/asboolP yB]. move=> /asboolPn; rewrite -set0P => /negP; rewrite negbK => /eqP AIB_eq0. move: xA yB; rewrite !nbhsE. move=> - [oA [oA_open oAx] oAA] [oB [oB_open oBx] oBB]. by exists (oA, oB); rewrite ?inE; split => //; apply: subsetI_eq0 AIB_eq0. apply: contraPP => /eqP /T_openT2[[/=A B]]. rewrite !inE => - [xA yB] [Aopen Bopen /eqP AIB_eq0]. move=> /(_ A B (open_nbhs_nbhs _) (open_nbhs_nbhs _)). by rewrite -set0P => /(_ _ _)/negP; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed