proposition: Lemma subspace_hausdorff : hausdorff_space T -> hausdorff_space [the topologicalType of subspace A].
proof: Proof. rewrite ?open_hausdorff => + x y xNy => /(_ x y xNy). move=> [[P Q]] /= [Px Qx] /= [/open_subspaceW oP /open_subspaceW oQ]. by move=> ?; exists (P, Q). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed