Module mathcomp.analysis.topology_theory.separation_axioms

From HB Require Import structures.
From mathcomp Require Import boot order algebra interval_inference finmap.
From mathcomp Require Import boolp classical_sets functions wochoice.
From mathcomp Require Import cardinality fsbigop set_interval filter reals.
From mathcomp Require Import topology_structure compact subspace_topology
  discrete_topology order_topology pseudometric_structure num_topology
  one_point_compactification uniform_structure connected supremum_topology
  sigT_topology.

# Separation Axioms This file introduces the separation axioms, a series of topological properties about separating points and sets. They are sometimes denoted by the names T0 through T6. Although we use their full names (hausdorff, accessible, uniform, etc). This file also provides related topological properties like zero dimensional and perfect, and discrete. ``` set_nbhs A == filter from open sets containing A ``` ## The classic separation axioms ``` kolmogorov_space T == T is a Kolmogorov space (T0) accessible_space T == T is an accessible space (T1) hausdorff_space T == T is a Hausdorff space (T2) close x y == x and y are arbitrarily close w.r.t. open sets normal_space T == T is normal (sometimes called T4) regular_space T == T is regular (sometimes called T3) ``` ## related concepts ``` totally_disconnected A == the only connected subsets of A are empty or singletons zero_dimensional T == points are separable by a clopen set perfect_set A == A is closed, and every point in A is a limit point of A ``` ## metrizability for uniform spaces ``` countable_uniform.type == endows a pseudoMetric on a uniform type whose entourage has a countable basis sup_pseudometric == the pseudometric induced for the supremum of countably many pseudoMetrics gauge E == for an entourage E, gauge E is a filter which includes `iter n split_ent E`. Critically, `gauge E` forms a uniform space with a countable uniformity. ```

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section set_nbhs.
Context { : topologicalType} ( : set T).

Definition := \bigcap_( in A) nbhs x.

Global Instance : Filter set_nbhs.

Proof.

split => P Q; first by exact: filterT.
by move=> Px Qx x Ax; apply: filterI; [exact: Px | exact: Qx].
by move=> PQ + x Ax => /(_ _ Ax)/filterS; exact.
Qed.

Global Instance : A !=set0 -> ProperFilter set_nbhs.

Proof.

case=> x Ax; split; last exact: set_nbhs_filter.
by move/(_ x Ax)/nbhs_singleton.
Qed.

Lemma ( : set T) :
set_nbhs B <-> (exists , [/\ open C, A `<=` C & C `<=` B]).

Proof.

split; first last.
  by case=> V [? AV /filterS +] x /AV ?; apply; apply: open_nbhs_nbhs.
move=> snB; have Ux x : exists , A x -> [/\ U x, open U & U `<=` B].
  have [/snB|?] := pselect (A x); last by exists point.
  by rewrite nbhsE => -[V [? ? ?]]; exists V.
exists (\bigcup_( in A) (projT1 (cid (Ux x)))); split.
- by apply: bigcup_open => x Ax; have [] := projT2 (cid (Ux x)).
- by move=> x Ax; exists x => //; have [] := projT2 (cid (Ux x)).
- by move=> x [y Ay]; have [//| _ _] := projT2 (cid (Ux y)); exact.
Qed.

End set_nbhs.

Section point_separation_axioms.
Context { : topologicalType}.

Definition := forall , x != y ->
exists : set T, (A \in nbhs x /\ y \in ~` A) \/ (A \in nbhs y /\ x \in ~` A).

Definition := forall , x != y ->
exists : set T, [/\ open A, x \in A & y \in ~` A].

Definition := forall : T, cluster (nbhs p) q -> p = q.

Lemma ( : set T) : hausdorff_space -> compact A -> closed A.

Proof.

move=> hT Aco p clAp; have pA := [elaborate @withinT _ (nbhs p) A _].
have [q [Aq clsAp_q]] := [elaborate Aco _ _ pA]; rewrite (hT p q) //.
by apply: cvg_cluster clsAp_q; apply: cvg_within.
Qed.

Lemma ( : T) :
hausdorff_space -> compact V -> nbhs x V ->
ProperFilter F -> F V -> cluster F = [set x] -> F --> x.

Proof.

move=> ? cptV nxV PF FV clFx1 U nbhsU; rewrite nbhs_simpl.
wlog oU : U nbhsU / open U.
  rewrite /= nbhsE in nbhsU; case: nbhsU => O oO OsubU /(_ O) WH.
  by apply: (filterS OsubU); apply: WH; [exact: open_nbhs_nbhs | by case: oO].
have /compact_near_coveringP : compact (V `\` U).
  apply: (subclosed_compact _ cptV) => //.
  by apply: closedI; [exact: compact_closed | exact: open_closedC].
move=> /(_ _ (powerset_filter_from F) (fun => ~ W x))[].
  move=> z [Vz ?]; have zE : x <> z by move/nbhs_singleton: nbhsU => /[swap] ->.
  have : ~ cluster F z by move: zE; apply: contra_not; rewrite clFx1 => ->.
  case/existsNP=> C /existsPNP [D] FC /existsNP [Dz] /nonemptyPn.
  rewrite setIC => /disjoints_subset CD0; exists (D, [set | F W /\ W `<=` C]).
    by split; rewrite //= nbhs_simpl; exact: powerset_filter_fromP.
  by case => t W [Dt] [FW] /subsetCP; apply; apply: CD0.
move=> M [MF ME2 [W] MW /(_ _ MW) VUW].
apply: (@filterS _ _ _ (V `&` W)); last by apply: filterI => //; exact: MF.
by move=> t [Vt Wt]; apply: contrapT => Ut; exact: (VUW t).
Qed.

Lemma ( : set T) :
hausdorff_space -> compact A -> precompact A.

Proof.

by move=> h c; rewrite precompactE -(closure_id _).1//; exact: compact_closed.
Qed.

Lemma : hausdorff_space =
  forall ( : T), x != y ->
    exists2 , (x \in AB.1 /\ y \in AB.2) &
                [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0].

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.

Lemma : hausdorff_space -> accessible_space.

Proof.

rewrite open_hausdorff => hsdfT => x y /hsdfT [[U V] [xU yV]] [/= ? ? /eqP].
rewrite setIC => /disjoints_subset VUc; exists U; repeat split => //.
by rewrite inE; apply: VUc; rewrite -inE.
Qed.

Lemma : accessible_space -> forall : T, closed [set x].

Proof.

move=> T1 x; rewrite -[X in closed X]setCK; apply: open_closedC.
rewrite openE => y /eqP /T1 [U [oU yU xU]].
rewrite /interior nbhsE /=; exists U; last by rewrite subsetC1.
by split=> //; exact: set_mem.
Qed.

Lemma : accessible_space -> kolmogorov_space.

Proof.

move=> T1 x y /T1 [A [oA xA yA]]; exists A; left; split=> //.
by rewrite nbhsE inE; exists A => //; rewrite inE in xA.
Qed.

Lemma :
accessible_space <-> forall : set T, finite_set A -> closed A.

Proof.

split => [TT1 A fA|h x y xy].
  rewrite -(fsbig_setU_set1 fA) fsbig_finite//=.
  by apply: bigsetU_closed => x xA; exact: accessible_closed_set1.
by exists (~` [set y]); rewrite !inE/=; split;
  [rewrite openC; exact: h|exact/eqP|].
Qed.

End point_separation_axioms.

Arguments hausdorff_space : clear implicits.
Arguments accessible_space : clear implicits.
Arguments kolmogorov_space : clear implicits.

Lemma { : topologicalType} ( : set T) :
accessible_space T -> closed (limit_point A).

Proof.

move=> accT; rewrite -openC openE/= => a.
rewrite /setC/= not_limit_pointE => -[X].
rewrite nbhsE/= => -[U oaU UX] XAa.
rewrite /interior nbhsE/=.
exists U => // x Ux /=.
rewrite not_limit_pointE.
have [xa|xneqa] := eqVneq x a.
  exists U; rewrite xa; first exact: open_nbhs_nbhs.
  by apply: subset_trans XAa; exact: setIS.
exists (U `&` [set~ a]).
  apply: open_nbhs_nbhs; split.
    apply: openI; first by case: oaU.
    by rewrite openC; exact: accessible_closed_set1.
  by split => //; exact/eqP.
apply: (@subset_trans _ (A `&` (X `&` [set~ a]))).
  by apply: setIS; exact: setSI.
apply: (@subset_trans _ ([set a] `&` [set~ a])).
  by rewrite setIA; exact: setSI.
by rewrite setICr.
Qed.

Arguments limit_point_closed {T} A.

Lemma { : topologicalType} ( : set T) :
hausdorff_space T -> hausdorff_space (subspace A).

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); split => //=; [exact: oP | exact: oQ].
Qed.

Lemma { : discreteTopologicalType} : hausdorff_space T.

Proof.

by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q)) [] // x [] -> ->.
Qed.

Lemma {} { : orderTopologicalType d} : hausdorff_space T.

Proof.

rewrite open_hausdorff=> p q; wlog : p q / (p < q)%O.
  have /orP[] := le_total p q; rewrite le_eqVlt => /predU1P[->|].
  - by rewrite eqxx.
  - by move=> ?; exact.
  - by rewrite eqxx.
  - move=> qp WH; rewrite eq_sym => /(WH _ _ qp)[[P Q] [? ?] [? ? ?]].
    by exists (Q, P); split; rewrite // setIC.
move=> plq ?; have [[z /andP[pz zq]]|] := pselect (exists , p < z < q)%O.
  exists (`]-oo,z[, `]z,+oo[)%classic.
    by split => //=; apply/mem_set; rewrite set_itvE.
  split => //= ; apply/eqP; rewrite -subset0 => r; rewrite set_itvE => -[/= rz].
  by apply/negP; rewrite in_itv/= andbT -leNgt (ltW rz).
move=> npzq; exists (`]-oo, q[, `]p, +oo[)%classic; split => //=.
- by apply /mem_set; rewrite set_itvE.
- by apply /mem_set; rewrite set_itvE.
- apply/eqP; rewrite -subset0 => r; rewrite !set_itvE => -[/= rz zr].
  by apply: npzq; exists r; rewrite rz zr.
Qed.

Section ball_hausdorff.
Variables ( : numDomainType) ( : pseudoMetricType R).

Lemma : hausdorff_space T =
  forall ( : T), a != b ->
  exists : {posnum R} * {posnum R},
    ball a r.1%:num `&` ball b r.2%:num == set0.

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)//; exact: interior_subset.
Qed.

End ball_hausdorff.

Import numFieldTopology.Exports.
Lemma ( : realFieldType) : hausdorff_space R.

Proof.

exact: order_hausdorff. Qed.

Lemma { : topologicalType} :
   locally_compact [set: X] ->
   hausdorff_space X ->
   hausdorff_space (one_point_compactification X).

Proof.

move=> lcpt hsdfX [x|] [y|] //=.
- move=> clxy; congr Some; apply: hsdfX => U V Ux Vy.
  have [] := clxy (Some @` U) (Some @` V).
    by apply: filterS Ux; exact: preimage_image.
    by apply: filterS Vy; exact: preimage_image.
  by case=> [_|] [] /= [// p /[swap] -[] <- Up] [q /[swap] -[] -> Vp]; exists p.
- have [U] := lcpt x I; rewrite withinET => Ux [cU clU].
  case/(_ (Some @` U) (Some @` (~` U) `|` [set None])).
  + exact: one_point_compactification_some_nbhs.
  + by exists U.
  + by move=> [?|] [][]// z /[swap] -[] <- ? []//= [? /[swap] -[] ->].
- have [U] := lcpt y I; rewrite withinET => Uy [cU clU].
  case/(_ (Some @` (~` U) `|` [set None]) (Some @` U)); first by exists U.
    exact: one_point_compactification_some_nbhs.
  by case=> [?|] [] [] //= + [] ? // /[swap] -[] -> => -[? /[swap] -[] <-].
Qed.

Section hausdorff_topologicalType.
Variable : topologicalType.
Implicit Types x y : T.

Local Open Scope classical_set_scope.
Definition : Prop := forall , open_nbhs y M -> closure M x.

Lemma : close x = cluster (nbhs x).

Proof.

transitivity (cluster (open_nbhs x)); last first.
by rewrite /cluster; under eq_fun do rewrite -meets_openl.
rewrite clusterEonbhs /close funeqE => y /=; rewrite meetsC /meets.
apply/eq_forall => A; rewrite forall_swap.
by rewrite closureEonbhs/= meets_globallyl.
Qed.

Lemma : close x = [set | open_nbhs x `#` open_nbhs y].

Proof.

by rewrite closeEnbhs; under eq_fun do rewrite -meets_openl -meets_openr.
Qed.

Lemma : close x y -> close y x.

Proof.

by rewrite !closeEnbhs /cluster/= meetsC. Qed.

Lemma {} { : ProperFilter F} : F --> x -> F --> y -> close x y.

Proof.

by move=> /sub_meets sx /sx; rewrite closeEnbhs; apply; apply/proper_meetsxx.
Qed.

Lemma : close x x.

Proof.

exact: (@cvg_close (nbhs x)). Qed.

Hint Resolve close_refl : core.

Lemma : x --> y -> close x y.

Proof.

exact: cvg_close. Qed.

Lemma {} { : ProperFilter F} ( : T' -> set T) ( : T) :
{near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'.

Proof.

move=> f_prop fFl fFl'.
suff f_totalfun: {near F, is_totalfun f}.
by apply: cvg_close fFl fFl'; exact: fmapi_proper_filter.
apply: filter_app f_prop; near do split=> //=.
have: (f `@ F) setT by apply: fFl; apply: filterT.
by rewrite fmapiE; apply: filterS => x [y []]; exists y.
Unshelve. all: by end_near. Qed.

Hypothesis : hausdorff_space T.

Lemma : close x y = (x = y).

Proof.

rewrite propeqE; split; last by move=> ->; exact: close_refl.
by rewrite closeEnbhs; exact: sep.
Qed.

Lemma : close x y -> x = y.

Proof.

by rewrite closeE. Qed.

Lemma {} { : ProperFilter F} : is_subset1 [set : T | F --> x].

Proof.

move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.

Lemma : x --> y -> x = y.

Proof.

by rewrite -closeE //; apply: cvg_close. Qed.

Lemma { : Type} {} { : ProperFilter F} ( : U -> set T) :
{near F, is_fun f} -> is_subset1 [set : T | f `@ F --> x].

Proof.

by move=> ffun fx fy; rewrite -closeE //; exact: cvgi_close. Qed.

End hausdorff_topologicalType.

Section hausdorff_ptopologicalType.
Variable : ptopologicalType.
Implicit Types x y : T.

Lemma ( : set_system T) { : ProperFilter F2} :
F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2).

Proof.

move=> F12 F21.
have [/(cvg_trans F21) F2l|dvgF1] := pselect (cvg F1).
by apply: (@cvg_close _ F2) => //; apply: cvgP F2l.
have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2).
rewrite dvgP // dvgP //; exact/close_refl.
Qed.

Hypothesis : hausdorff_space T.

Lemma {} { : ProperFilter F} ( : T) :
F --> l -> lim F = l.

Proof.

by move=> /[dup] /cvgP /cvg_unique; apply. Qed.

Lemma : lim (nbhs x) = x.

Proof.

exact: cvg_lim. Qed.

Lemma {} {} { : ProperFilter F} ( : T) ( : U -> T) :
(\forall \near F, f x = l) -> lim (f @ F) = l.

Proof.

by move=> /cvg_near_cst/cvg_lim. Qed.

Lemma {} {} { : ProperFilter F} ( : T) : lim (@cst U _ k @ F) = k.

Proof.

exact: cvg_lim. Qed.

Lemma {} {} { : ProperFilter F} ( : U -> T -> Prop) ( : T) :
F (fun : U => is_subset1 (f x)) ->
f `@ F --> l -> lim (f `@ F) = l.

Proof.

by move=> f_prop fl; apply: get_unique =>// l' fl'; exact: cvgi_unique _ fl' fl.
Qed.

End hausdorff_ptopologicalType.
#[global] Hint Resolve close_refl : core.
Arguments close_cvg {T} F1 F2 {FF2} _.

Section close_uniform.
Implicit Types (U : uniformType).

Lemma {} ( : U) :
close x y = forall , entourage A -> A (x, y).

Proof.

rewrite propeqE; split=> [cxy A entA|cxy].
  have /entourage_split_ent entsA := entA; rewrite closeEnbhs in cxy.
  have yl := nbhs_entourage _ (entourage_inv entsA).
  have yr := nbhs_entourage _ entsA.
  have [z [/xsectionP zx /xsectionP zy]] := cxy _ _ (yr x) (yl y).
  exact: (entourage_split z).
rewrite closeEnbhs => A B /nbhsP[E1 entE1 sE1A] /nbhsP[E2 entE2 sE2B].
exists y; split.
- by apply/sE1A/xsectionP; exact: cxy.
- by apply/sE2B/xsectionP; exact: entourage_refl.
Qed.

Lemma {} ( : U) : close x y -> close y z -> close x z.

Proof.

rewrite !entourage_close => cxy cyz A entA.
exact: entourage_split (cxy _ _) (cyz _ _).
Qed.

Lemma {} ( : U) : close x y -> x --> y.

Proof.

rewrite entourage_close => cxy P /= /nbhsP[A entA sAP].
apply/nbhsP; exists (split_ent A) => // z /xsectionP xz; apply: sAP.
apply/xsectionP; apply: (entourage_split x) => //.
by have := cxy _ (entourage_inv (entourage_split_ent entA)).
Qed.

Lemma { : puniformType} ( : set_system U) ( : U) :
ProperFilter F ->
F --> l <-> ([cvg F in U] /\ close (lim F) l).

Proof.

move=> FF; split=> [Fl|[cvF]Cl].
by have /cvgP := Fl; split=> //; apply: (@cvg_close _ F).
by apply: cvg_trans (close_cvgxx Cl).
Qed.

Lemma { : numFieldType} { : pseudoMetricType R} ( : M) :
close x y = forall : {posnum R}, ball x eps%:num y.

Proof.

rewrite propeqE; split => [cxy eps|cxy].
  have := [elaborate cxy _ (open_nbhs_ball _ (eps%:num/2)%:pos)].
  rewrite closureEonbhs/= meetsC meets_globallyr.
  move/(_ _ (open_nbhs_ball _ (eps%:num/2)%:pos)) => [z [zx zy]].
  by apply: (@ball_splitl _ _ z); apply: interior_subset.
rewrite closeEnbhs => B A /nbhs_ballP[_/posnumP[e2 e2B]]
  /nbhs_ballP[_/posnumP[e1 e1A]].
by exists y; split; [apply/e2B|apply/e1A; exact: ballxx].
Qed.

End close_uniform.

Section set_separations.
Context { : topologicalType}.

Definition :=
  forall : set T, closed A ->
    filter_from (set_nbhs A) closure `=>` set_nbhs A.

Definition :=
  forall : T, filter_from (nbhs a) closure --> a.

Lemma ( : T) : hausdorff_space T -> compact V ->
  nbhs x V -> {for x, regular_space}.

Proof.

move=> sep 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/closureS/disjoints_subset; rewrite setIC.
Qed.

Lemma ( : set T) : hausdorff_space T -> compact K ->
forall : set T, A `<=` K° -> {for A, normal_space}.

Proof.

move=> hT cptV A AK clA B snAB; have /compact_near_coveringP cvA : compact A.
  apply/(subclosed_compact clA cptV)/(subset_trans AK).
  exact: interior_subset.
have snbC ( : set T) : Filter (filter_from (set_nbhs U) closure).
  apply: filter_from_filter; first by exists setT; apply: filterT.
  by move=> P Q sAP sAQ; exists (P `&` Q); [apply filterI|exact: closureI].
have [/(congr1 setC)|/set0P[b0 B0]] := eqVneq (~` B) set0.
  by rewrite setCK setC0 => ->; exact: filterT.
have PsnA : ProperFilter (filter_from (set_nbhs (~` B)) closure).
  apply: filter_from_proper => ? P.
  by exists b0; apply/subset_closure; apply: nbhs_singleton; exact: P.
pose F := powerset_filter_from (filter_from (set_nbhs (~` B)) closure).
have PF : Filter F by exact: powerset_filter_from_filter.
have cvP ( : T) : A x -> \forall \near x & \near F, (~` i) x'.
  move=> Ax; case/set_nbhsP : snAB => C [oC AC CB].
  have [] := @compact_regular x _ hT cptV _ C; first exact: AK.
    by rewrite nbhsE /=; exists C => //; split => //; exact: AC.
  move=> D /nbhs_interior nD cDC.
  have snBD : filter_from (set_nbhs (~` B)) closure (closure (~` closure D)).
    exists (closure (~` closure D)) => [z|].
      move=> nBZ; apply: filterS; first exact: subset_closure.
      apply: open_nbhs_nbhs; split; first exact/closed_openC/closed_closure.
      exact/(subsetC _ nBZ)/(subset_trans cDC).
    by have := @closed_closure _ (~` closure D); rewrite closure_id => <-.
  near=> y U => /=; have Dy : D° y by exact: (near nD _).
  have UclD : U `<=` closure (~` closure D).
    exact: (near (small_set_sub snBD) U).
  move=> Uy; have [z [/= + Dz]] := UclD _ Uy _ Dy.
  by apply; exact: subset_closure.
case/(_ _ _ _ _ cvP) : cvA => R /= [RA Rmono [U RU] RBx].
have [V /set_nbhsP [W [oW cBW WV] clVU]] := RA _ RU; exists (~` W).
  apply/set_nbhsP; exists (~` closure W); split.
  - exact/closed_openC/closed_closure.
  - by move=> y /(RBx _ RU) + Wy; apply; exact/clVU/(closureS WV).
  - by apply: subsetC; exact/subset_closure.
have : closed (~` W) by exact: open_closedC.
by rewrite closure_id => <-; exact: subsetCl.
Unshelve. all: by end_near. Qed.

Lemma : hausdorff_space T -> compact [set: T] -> normal_space.

Proof.

move=> ? /compact_normal_local + A clA; apply => //.
by move=> z ?; exact: filterT.
Qed.

End set_separations.

Arguments normal_space : clear implicits.
Arguments regular_space : clear implicits.

Local Open Scope relation_scope.
Lemma { : uniformType} : @regular_space T.

Proof.

move=> x R /=; rewrite -{1}nbhs_entourageE => -[E entE ER].
pose E' := split_ent E; have eE' : entourage E' by exact: entourage_split_ent.
exists (xsection (E' `&` E'^-1) x).
  rewrite -nbhs_entourageE; exists (E' `&` E'^-1) => //.
  exact: filterI.
move=> z /= clEz; apply/ER/xsectionP; apply: subset_split_ent => //.
have [] := clEz (xsection (E' `&` E'^-1) z).
  rewrite -nbhs_entourageE; exists (E' `&` E'^-1) => //.
  exact: filterI.
by move=> y /= [/xsectionP[? ?] /xsectionP[? ?]]; exists y.
Qed.

Local Close Scope relation_scope.

#[global] Hint Resolve uniform_regular : core.

Section totally_disconnected.
Implicit Types T : topologicalType.

Definition {} ( : set T) :=
forall , A x -> connected_component A x = [set x].

Definition :=
(forall , x != y -> exists : set T, [/\ clopen U, U x & ~ U y]).

Lemma { : discreteTopologicalType} : zero_dimensional T.

Proof.

move=> x y xny; exists [set x]; split => //; last exact/nesym/eqP.
by split; [exact: discrete_open | exact: discrete_closed].
Qed.

Lemma {} :
zero_dimensional T -> totally_disconnected [set: T].

Proof.

move=> zdA x _; rewrite eqEsubset.
split=> [z [R [Rx _ ctdR Rz]]|_ ->]; last exact: connected_component_refl.
apply: contrapT => /eqP znx; have [U [[oU cU] Uz Ux]] := zdA _ _ znx.
suff : R `&` U = R by move: Rx => /[swap] <- [].
by apply: ctdR; [exists z|exists U|exists U].
Qed.

Lemma {} ( : T) :
hausdorff_space T -> zero_dimensional T -> compact [set: T] ->
filter_from [set : set T | D x /\ clopen D] id --> x.

Proof.

pose F := filter_from [set : set T | D x /\ clopen D] id.
have FF : Filter F.
  apply: filter_from_filter; first by exists setT; split => //; exact: clopenT.
  by move=> A B [? ?] [? ?]; exists (A `&` B) => //; split=> //; exact: clopenI.
have PF : ProperFilter F by apply: filter_from_proper; move=> ? [? _]; exists x.
move=> hsdfT zdT cmpT U Ux; rewrite nbhs_simpl -/F.
wlog oU : U Ux / open U.
  move: Ux; rewrite /= nbhsE => -[] V [? ?] /filterS + /(_ V) P.
  by apply; apply: P => //; exists V.
have /(iffLR (compact_near_coveringP _)) : compact (~` U).
  by apply: (subclosed_compact _ cmpT) => //; exact: open_closedC.
move=> /(_ _ _ setC (powerset_filter_from_filter PF))[].
  move=> y nUy; have /zdT [C [[oC cC] Cx Cy]] : x != y.
    by apply: contra_notN nUy => /eqP <-; exact: nbhs_singleton.
  exists (~` C, [set | U `<=` C]); first split.
  - by apply: open_nbhs_nbhs; split => //; exact: closed_openC.
  - apply/near_powerset_filter_fromP; first by move=> ? ?; exact: subset_trans.
    by exists C => //; exists C.
  - by case=> i j [? /subsetC]; apply.
by move=> D [DF _ [C DC]]/(_ _ DC)/subsetC2/filterS; apply; exact: DF.
Qed.

Lemma {} { : orderTopologicalType d} ( : T) :
(x < y)%O -> zero_dimensional T ->
exists , [/\ clopen U, U y , ~ U x & forall , U r -> ~ U l -> l < r]%O.

Proof.

move=> xy zt; have xNy : y != x by move: xy; rewrite lt_def => /andP[].
have [U [clU Uy nUx]] := zt y x xNy.
have := clopen_bigcup_clopen clU Uy; set I := (I in clopen I); case=> ? ?.
pose V := I `|` `[y, +oo[; have Iy : I y.
  case: clU => + _; rewrite openE => /(_ _ Uy).
  rewrite /interior /= itv_nbhsE /= => -[i [] iy yi iU].
  by exists i => //; split => //; exact: itv_open_ends_open.
have IU : I `<=` U by move=> ? [? [+ _ _]] => /subset_trans; exact.
exists V; split; first split.
- suff -> : V = I `|` `]y,+oo[ by exact: openU.
  have /mem_set := Iy; rewrite -sub1set => /setUidl <-.
  by rewrite -setUA setU1itv.
- by apply: closedU => //; exact: rray_closed.
- by left.
- by move=> [/IU //|]; rewrite set_itvE/= leNgt xy.
- move=> l r Vr Vl; rewrite ltNge; apply/negP; move: Vl; apply: contra_not.
  move=> rl; case: Vr; first last.
    by rewrite set_itvE => yr; right; rewrite set_itvE; exact: (le_trans yr).
  have /orP[|ly] := le_total y l; first by move=> + _; right; rewrite set_itvE.
  case=> i [iu oi /= yi ri]; left; exists i; first by split.
  move: iu oi => _ _; case: i yi ri => p q /= /andP [py yq] /andP[pr rq].
  apply/andP; split.
  + by rewrite (le_trans pr)// bnd_simp.
  + by rewrite (le_trans _ yq)// bnd_simp.
Qed.

End totally_disconnected.

Module .
Section countable_uniform.
Local Open Scope relation_scope.
Context { : realType} { : uniformType}.

Hypothesis : @countable_uniformity T.

Let := projT1 (cid2 (iffLR countable_uniformityP cnt_unif)).

Local Lemma : forall , entourage A -> exists , f_ N `<=` A.

Proof.

by have [] := projT2 (cid2 (iffLR countable_uniformityP cnt_unif)). Qed.

Let : forall , entourage (f_ n).

Proof.

by have [] := projT2 (cid2 (iffLR countable_uniformityP cnt_unif)). Qed.

Local Fixpoint : set (T * T) :=
if n is n.+1 then let := split_ent (split_ent (g_ n)) `&` f_ n in W `&` W^-1
else [set: T*T].

Let : entourage (g_ n).

Proof.

elim: n => /=; first exact: entourageT.
by move=> n entg; apply/entourage_invI; exact: filterI.
Qed.

Local Lemma : (g_ n)^-1 = g_ n.

Proof.

by case: n => // n; rewrite eqEsubset; split; case=> ? ?; rewrite /= andC.
Qed.

Local Lemma : g_ n.+1 `<=` g_ n.

Proof.

apply: subIset; left; apply: subIset; left; apply: subset_trans.
by apply: split_ent_subset; exact: entourage_split_ent.
by apply: subset_trans; last exact: split_ent_subset.
Qed.

Local Lemma : (m <= n)%N -> g_ n `<=` g_ m.

Proof.

elim: n; rewrite ?leqn0; first by move=>/eqP ->.
move=> n IH; rewrite leq_eqVlt ltnS => /orP [/eqP <- //|] /IH.
by apply: subset_trans; exact: descendG1.
Qed.

Local Lemma : g_ n.+1 \; g_ n.+1 \; g_ n.+1 `<=` g_ n.

Proof.

suff g2split : g_ n.+1 \; g_ n.+1 `<=` split_ent (g_ n).
  apply: subset_trans; last exact: subset_split_ent (entG n).
  apply: set_compose_subset (g2split); rewrite -[_ n.+1]set_compose_diag.
  apply: subset_trans g2split; apply: set_compose_subset => //.
  by move=> [_ _] [z _] [<- <-]; exact: entourage_refl.
apply: subset_trans; last exact: subset_split_ent.
by apply: set_compose_subset; apply: subIset; left; apply: subIset; left.
Qed.

Local Lemma : g_ n.+1 `<=` f_ n.

Proof.

by apply: subIset; left; apply: subIset; right. Qed.

Local Lemma : entourage A -> exists , g_ N `<=` A.

Proof.

move=> /countableBase [N] fnA; exists N.+1.
by apply: subset_trans fnA; exact: gsubf.
Qed.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Local Definition ( : R) : nat := Num.truncn e^-1.

Local Lemma : distN 0 = 0%N.

Proof.

by rewrite /distN invr0 truncn0. Qed.

Local Lemma ( : nat) : distN n%:R^-1 = n.

Proof.

by rewrite /distN invrK; apply/eqP; rewrite -(@eqr_nat R) -natrEtruncn.
Qed.

Local Lemma : e1 > 0 -> e1 <= e2 -> (distN e2 <= distN e1)%N.

Proof.

move=> e1pos e1e2; rewrite /distN le_truncn// lef_pV2// posrE.
by rewrite (lt_le_trans e1pos).
Qed.

Local Fixpoint :=
  if n is n.+1 then exists ,
    [/\ n_step_ball n x d1 y,
        0 < d1,
        0 < d2,
        g_ (distN d2) (y, z) &
        d1 + d2 = e]
  else e > 0 /\ g_ (distN e) (x, z).

Local Definition := exists , (n_step_ball i x e z).

Local Lemma : n_step_ball n x e z -> 0 < e.

Proof.

by case: n => [[]|] // n; case=> [?] [?] [?] [] ? ? ? ? <-; exact: addr_gt0.
Qed.

Local Lemma : step_ball x e z -> 0 < e.

Proof.

by case => ?; exact: n_step_ball_pos. Qed.

Local Lemma :
0 < e -> entourage [set | step_ball xy.1 e xy.2].

Proof.

move=> epos; apply: (@filterS _ _ _ (g_ (distN e))) => // [[x y]] ?.
by exists 0%N.
Qed.

Local Lemma : 0 < e -> n_step_ball 0 x e x.

Proof.

by move=> epos; split => //; exact: entourage_refl. Qed.

Local Lemma : 0 < e -> step_ball x e x.

Proof.

by move=> epos; exists 0%N; apply: n_step_ball_center. Qed.

Local Lemma :
  n_step_ball n x d1 y ->
  n_step_ball m y d2 z ->
  n_step_ball (n + m).+1 x (d1 + d2) z.

Proof.

move: n z d2; elim: m => [n z d2 Nxy [? ?]|n IH m z d2 Oxy].
by exists y, d1, d2; split; rewrite ?addn0 // (n_step_ball_pos Nxy).
move=> [w] [e1] [e2] [Oyw ? ? ? <-].
exists w, (d1 + e1), e2; rewrite addnS addrA.
split => //; last by rewrite addr_gt0//; exact: n_step_ball_pos Oxy.
by case: (IH m w e1 Oxy Oyw) => t [e3] [e4] [] Oxt ? ? ? <-; exists t, e3, e4.
Qed.

Local Lemma :
step_ball x d1 y -> step_ball y d2 z -> step_ball x (d1 + d2) z.

Proof.

move=> [n Oxy] [m Oyz]; exists (n + m).+1.
exact: n_step_ball_triangle Oxy Oyz.
Qed.

Local Lemma :
n_step_ball n x e y -> n_step_ball n y e x.

Proof.

move: x y e; elim: n; first by move=> ? ? ?; rewrite /= -{1}symG.
move=> n IH x y e [t] [d1] [d2] [] /IH Oty ? ?.
rewrite addrC -symG -[n]add0n => gty <-; apply: (n_step_ball_triangle _ Oty).
by split => //; exact: gty.
Qed.

Local Lemma : step_ball x e y -> step_ball y e x.

Proof.

by case=> n /n_step_ball_sym ?; exists n. Qed.

Local Lemma :
e1 <= e2 -> n_step_ball n x e1 `<=` n_step_ball n x e2.

Proof.

move: x e1 e2; elim: n.
move=> x e1 e2 e1e2 y [?] gxy; split; first exact: (lt_le_trans _ e1e2).
by apply: descendG; last (exact: gxy); exact: distN_le.
move=> n IH x e1 e2 e1e2 z [y] [d1] [d2] [] /IH P d1pos d2pos gyz d1d2e1.
exists y, (e2 - d2), d2; split => //.
- by apply: P; rewrite lerBrDr d1d2e1.
- by apply: lt_le_trans d1pos _; rewrite lerBrDr d1d2e1.
- by rewrite subrK.
Qed.

Local Lemma :
e1 <= e2 -> step_ball x e1 `<=` step_ball x e2.

Proof.

by move=> e1e2 ? [n P]; exists n; exact: (n_step_ball_le e1e2). Qed.

Local Lemma ( : nat) : n.+1%:R^-1 / (2:R) <= n.+2%:R^-1.

Proof.

rewrite -invrM //; [exact: unitf_gt0 |exact: unitf_gt0|].
rewrite lef_pV2 ?posrE // -?natrM ?ler_nat -addn1 -addn1 -addnA mulnDr.
by rewrite muln1 leq_add2r leq_pmull.
Qed.

Local Lemma :
  0 < e1 -> 0 < e2 -> n_step_ball n.+1 x (e1 + e2) z ->
    exists ,
    [/\
      n_step_ball a x e1 t1,
      n_step_ball 0 t1 (e1 + e2) t2,
      n_step_ball b t2 e2 z &
      (a + b = n)%N
    ].

Proof.

move: e1 e2 x z; elim: n.
  move=> e1 e2 x z e1pos e2pos [y] [d1] [d2] [] Oxy ? ? gd2yz deE.
  case: (pselect (e1 <= d1)).
    move=> e1d1; exists x, y, 0%N, 0%N; split.
    - exact: n_step_ball_center.
    - apply: n_step_ball_le; last exact: Oxy.
      by rewrite -deE lerDl; apply: ltW.
    - by apply: (@n_step_ball_le _ _ d2); rewrite // -(lerD2l e1) -deE lerD.
    - by rewrite addn0.
  move=> /negP; rewrite -ltNge//.
  move=> e1d1; exists y, z, 0%N, 0%N; split.
  - by apply: n_step_ball_le; last (exact: Oxy); exact: ltW.
  - by apply: (@n_step_ball_le _ _ d2); rewrite // -deE lerDr ltW.
  - exact: n_step_ball_center.
  - by rewrite addn0.
move=> n IH e1 e2 x z e1pos e2pos [y] [d1] [d2] [] Od1xy d1pos d2pos gd2yz deE.
case: (pselect (e2 <= d2)).
  move=> e2d2; exists y, z, n.+1, 0%N; split.
  - by apply: (@n_step_ball_le _ _ d1); rewrite // -(lerD2r e2) -deE lerD.
  - by apply: (@n_step_ball_le _ _ d2); rewrite // -deE lerDr; exact: ltW.
  - exact: n_step_ball_center.
  - by rewrite addn0.
have d1E' : d1 = e1 + (e2 - d2) by rewrite addrA -deE addrK.
move=> /negP; rewrite -ltNge// => d2lee2.
  case: (IH e1 (e2 - d2) x y); rewrite ?subr_gt0 // -d1E' //.
  move=> t1 [t2] [c1] [c2] [] Oxy1 gt1t2 t2y <-.
  exists t1, t2, c1, c2.+1; split => //.
  - by apply: (@n_step_ball_le _ _ d1); rewrite -?deE // ?lerDl; exact: ltW.
  - by exists y, (e2 - d2), d2; rewrite // ?subr_gt0// subrK.
  - by rewrite addnS.
Qed.

Local Lemma :
n_step_ball 0 x n%:R^-1 `<=` [set | g_ n (x,y)].

Proof.

by move=> y [] ?; rewrite distN_nat. Qed.

Local Lemma :
n_step_ball n x N.+1%:R^-1 `<=` [set | (g_ N) (x, y)].

Proof.

move: N x; elim: n {-2}n (leqnn n) => n.
  rewrite leqn0 => /eqP -> N x; apply: subset_trans.
    exact: n_step_ball_le_g.
  by move=> y ?; exact: descendG.
move=> IH1 + + N x1 x4; case.
  by move=> ? [?] P; apply: descendG _ P; rewrite distN_nat.
move=> l ln1 Ox1x4.
case: (@split_n_step_ball l x1 (N.+1%:R^-1/2) (N.+1%:R^-1/2) x4) => //.
  by rewrite -splitr.
move=> x2 [x3] [l1] [l2] [] P1 [? +] P3 l1l2; rewrite -splitr distN_nat => ?.
have l1n : (l1 <= n)%N by rewrite (leq_trans (leq_addr l2 l1))// l1l2 -ltnS.
have l2n : (l2 <= n)%N by rewrite (leq_trans (leq_addl l1 l2))// l1l2 -ltnS.
apply: splitG3; exists x3; [exists x2 => //|].
  by move/(n_step_ball_le (distN_half N))/(IH1 _ l1n) : P1.
by move/(n_step_ball_le (distN_half N))/(IH1 _ l2n) : P3.
Qed.

Local Lemma :
step_ball x N.+1%:R^-1 `<=` [set | (g_ N) (x, y)].

Proof.

by move=> y [] n; exact: subset_n_step_ball. Qed.

Local Lemma : entourage = entourage_ step_ball.

Proof.

rewrite predeqE => E; split; first last.
by case=> e /= epos esubE; apply: (filterS esubE); exact: entourage_nball.
move=> entE; case: (countableBase entE) => N fN.
exists N.+2%:R^-1; first by rewrite /= invr_gt0.
apply: (subset_trans _ fN); apply: subset_trans; last apply: gsubf.
by case=> x y /= N1ball; apply: (@subset_step_ball x N.+1).
Qed.

Definition : Type := let _ := countableBase in let _ := entF in T.

..on type.
..Build R type
step_ball_center step_ball_sym step_ball_triangle step_ball_entourage.
. T} :=
Pointed.copy type (Pointed.Pack q).

Lemma ( : T) : @ball _ type x 2 y.

Proof.

rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN.
rewrite (_ : Num.truncn _ = 0)//.
by apply/eqP; rewrite truncn_eq// invr_ge0// ler0n/= invf_lt1// ltr1n.
Qed.

End countable_uniform.

Module . HB.reexport. End Exports.
End countable_uniform.
Export countable_uniform.Exports.

Notation := countable_uniform.type.

Definition ( : realType) ( : Type) ( : Type)
  ( : Ii -> PseudoMetric R T) ( : countable [set: Ii]) : Type := T.

Section sup_pseudometric.
Variable ( : realType) ( : choiceType) ( : Type).
Variable ( : Ii -> PseudoMetric R T).

Hypothesis : countable [set: Ii].

Local Notation := (sup_pseudometric Tc Icnt).

Let := fun => PseudoMetric.Pack (Tc i).

Let := @countable_sup_ent T Ii Tc Icnt
  (fun => @countable_uniformity_metric _ (TS i)).

. R S :=
  PseudoMetric.on (countable_uniform countable_uniformityT).

End sup_pseudometric.

Module .
Section gauge.
Local Open Scope relation_scope.

Let { : uniformType} ( : set (T * T)) :=
  (split_ent W) `&` (split_ent W)^-1.

Section entourage_gauge.
Context { : uniformType} ( : set (T * T)) ( : entourage E).

Definition :=
  filter_from [set: nat] (fun => iter n split_sym (E `&` E^-1)).

Lemma : entourage (iter j split_sym (E `&` E^-1)).

Proof.

by elim: j => [|i IH]; exact: filterI. Qed.

Lemma : gauge A -> entourage A.

Proof.

case=> n; elim: n A; first by move=> ? _ /filterS; apply; apply: filterI.
by move=> n ? A _ /filterS; apply; apply: filterI; have ? := iter_split_ent n.
Qed.

Lemma : Filter gauge.

Proof.

apply: filter_from_filter; first by exists 0%N.
move=> i j _ _; wlog ilej : i j / (i <= j)%N.
  by move=> WH; have [|/ltnW] := leqP i j;
    [|rewrite (setIC (iter _ _ _))]; exact: WH.
exists j => //; rewrite subsetI; split => //; elim: j i ilej => [i|j IH i].
  by rewrite leqn0 => /eqP ->.
rewrite leq_eqVlt => /predU1P[<-//|/ltnSE/IH]; apply: subset_trans.
by move=> x/= [jx _]; apply: split_ent_subset => //; exact: iter_split_ent.
Qed.

Lemma : gauge A -> diagonal `<=` A.

Proof.

case=> n _; apply: subset_trans => -[_ a]/diagonalP ->.
by apply: entourage_refl; exact: iter_split_ent.
Qed.

Lemma : gauge A -> gauge A^-1.

Proof.

case=> n _ EA; apply: (@filterS _ _ _ (iter n split_sym (E `&` E^-1))).
- exact: gauge_filter.
- by case: n EA; last move=> n; move=> EA [? ?] [/=] ? ?; exact: EA.
- by exists n .
Qed.

Lemma : gauge A -> exists2 , gauge B & B \; B `<=` A.

Proof.

case => n _ EA; exists (iter n.+1 split_sym (E `&` E^-1)); first by exists n.+1.
apply: subset_trans EA; apply: subset_trans; first last.
by apply: subset_split_ent; exact: iter_split_ent.
by case=> a c [b] [] ? ? [] ? ?; exists b.
Qed.

Let : Type := T.

..on gauged.
.
.Build gauged gauge gauge_filter gauge_refl gauge_inv gauge_split.

Lemma : countable_uniformity gauged.

Proof.

exists [set iter n split_sym (E `&` E^-1) | in [set: nat]].
split; [exact: card_image_le | by move=> W [n] _ <-; exists n|].
by move=> D [n _ ?]; exists (iter n split_sym (E `&` E^-1)).
Qed.

Definition := countable_uniform.type gauge_countable_uniformity.
End entourage_gauge.

End gauge.
Module . HB.reexport. End Exports.
End gauge.
Export gauge.Exports.

Lemma { : realType} { : puniformType} :
@entourage T = @sup_ent T { : set (T * T) | @entourage T E}
(fun => Uniform.class (@gauge.type T (projT1 E) (projT2 E))).

Proof.

rewrite eqEsubset; split => [E entE|E].
  exists E => //=.
  pose pe : {classic { : set (T * T) | _}} * _ := (exist _ E entE, E).
  have entPE : `[< @entourage (gauge.type entE) E >].
    by apply/asboolP; exists 0%N => // ? [].
  exists (fset1 (exist _ pe entPE)) => //=; first by move=> ?; rewrite in_setE.
  by rewrite set_fset1 bigcap_set1.
case=> W /= [/= J] _ <- /filterS; apply; apply: filter_bigI => -[] [] [] /= D.
move=> entD G /[dup] /asboolP [n _ + _ _] => /filterS; apply.
exact: gauge.iter_split_ent.
Qed.

Section perfect_sets.

Implicit Types (T : topologicalType).

Definition {} ( : set T) := closed A /\ limit_point A = A.

Lemma {} ( : set T) :
perfect_set A <-> closed A /\ isolated A = set0.

Proof.

split=> [[cA limA]|[cA isoA]]; have := closure_isolated_limit_point A.
- move=> /(congr1 (fun => x `\` limit_point A)).
  rewrite setUDK.
    by apply/disj_setPS; rewrite disj_set_sym disjoint_isolated_limit_point.
  by rewrite limA -(closure_id A).1// setDv.
- by rewrite isoA set0U -(closure_id A).1.
Qed.

Lemma {} : perfect_set [set: T] <-> forall : T, ~ open [set x].

Proof.

split.
  case=> _; rewrite eqEsubset; case=> _ + x Ox => /(_ x I [set x]).
  by (case; [by apply: open_nbhs_nbhs; split |]) => y [+ _] => /[swap] -> /eqP.
move=> NOx; split; [exact: closedT |]; rewrite eqEsubset; split => x // _.
move=> U; rewrite nbhsE; case=> V [] oV Vx VU.
have Vnx: V != [set x] by apply/eqP => M; apply: (NOx x); rewrite -M.
have /existsNP [y /existsNP [Vy Ynx]] : ~ forall , V y -> y = x.
  move/negP: Vnx; apply: contra_not => Vxy; apply/eqP; rewrite eqEsubset.
  by split => // ? ->.
by exists y; split => //; [exact/eqP | exact: VU].
Qed.

Lemma {} : perfect_set [set: T] <->
forall ( : set T), open U -> U !=set0 ->
exists , [/\ U x, U y & x != y] .

Proof.

apply: (iff_trans perfectTP); split.
  move=> nx1 U oU [] x Ux; exists x.
  have : U <> [set x] by move=> Ux1; apply: (nx1 x); rewrite -Ux1.
  apply: contra_notP => /not_existsP/contrapT=> Uyx; rewrite eqEsubset.
  by split => [y Uy|? ->//]; have /not_and3P[//|//|/negP/negPn/eqP] := Uyx y.
move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x.
by move=> y [] ? [->] -> /eqP.
Qed.

End perfect_sets.

Section sigT_separations.
Context { : choiceType} { : I -> topologicalType}.

Lemma :
(forall , hausdorff_space (X i)) -> hausdorff_space { & X i}.

Proof.

move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= 2!sigT_nbhsE /= => cl.
have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]);
[by apply: existT_nbhs; exact: filterT..|].
move=> p [/= [_ _ <-] [_ _ [ji]]] _.
rewrite {}ji {j} in x y cl *.
congr existT; apply: hX => U V Ux Vy.
have [] := cl (existT X i @` U) (existT X i @` V); [exact: existT_nbhs..|].
move=> z [] [l Ul <-] [r Vr lr]; exists l; split => //.
by rewrite -(existT_inj2 lr).
Qed.

End sigT_separations.

Files

Module mathcomp.analysis.topology_theory.separation_axioms