proposition: Lemma regular_openP {T : topologicalType} (x : T) : {for x, @regular_space T} <-> forall A, closed A -> ~ A x -> exists U V : set T, [/\ open U, open V, U x, A `<=` V & U `&` V = set0].
proof: Proof. split. move=> + A clA nAx => /(_ (~` A)) []. by apply: open_nbhs_nbhs; split => //; exact: closed_openC. move=> U Ux /subsetC; rewrite setCK => AclU; exists (interior U). exists (~` closure U) ; split => //; first exact: open_interior. exact/closed_openC/closed_closure. apply/disjoints_subset; rewrite setCK. exact: (subset_trans (@interior_subset _ _) (@subset_closure _ _)). move=> + A Ax => /(_ (~` interior A)) []; [|exact|]. exact/open_closedC/open_interior. move=> U [V] [oU oV Ux /subsetC cAV /disjoints_subset UV]; exists U. exact/open_nbhs_nbhs. apply: (subset_trans (closure_subset UV)). move/open_closedC/closure_id : oV => <-. by apply: (subset_trans cAV); rewrite setCK; exact: interior_subset. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule