proposition: Lemma compact_regular (x : T) V : compact V -> nbhs x V -> {for x, regular_space}.
proof: Proof. move=> cptv Vx; apply: (@compact_cluster_set1 T x _ V) => //. - apply: filter_from_proper => //; first last. by move=> ? /nbhs_singleton/subset_closure ?; exists x. apply: filter_from_filter; first by exists setT; exact: filterT. move=> P Q Px Qx; exists (P `&` Q); [exact: filterI | exact: closureI]. - by exists V => //; have /closure_id <- : closed V by exact: compact_closed. rewrite eqEsubset; split; first last. move=> _ -> A B [C Cx CA /nbhs_singleton Bx]; exists x; split => //. by apply/CA/subset_closure; exact: nbhs_singleton. move=> y /=; apply: contraPeq; move: sep; rewrite open_hausdorff => /[apply]. move=> [[B A]]/=; rewrite ?inE; case=> By Ax [oB oA BA0]. apply/existsNP; exists (closure A); apply/existsNP; exists B; apply/not_implyP. split; first by exists A => //; exact: open_nbhs_nbhs. apply/not_implyP; split; first exact: open_nbhs_nbhs. apply/set0P/negP; rewrite negbK; apply/eqP/disjoints_subset. have /closure_id -> : closed (~` B); first by exact: open_closedC. by apply/closure_subset/disjoints_subset; rewrite setIC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed