replace original zorn lemma with georges'

classical/classical_sets.v

@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg matrix finmap ssrnum.
 From mathcomp Require Import ssrint interval.
-From mathcomp Require Import mathcomp_extra boolp.
+From mathcomp Require Import mathcomp_extra boolp wochoice.
 
 (**md**************************************************************************)
 (* # Set Theory                                                               *)
@@ -2599,127 +2599,55 @@ End partitions.
 #[deprecated(note="Use trivIset_setIl instead")]
 Notation trivIset_setI := trivIset_setIl (only parsing).
 
+Section Zorn.
+
 Definition total_on T (A : set T) (R : T -> T -> Prop) :=
   forall s t, A s -> A t -> R s t \/ R t s.
 
-Section ZL.
-
-Variable (T : Type) (t0 : T) (R : T -> T -> Prop).
-Hypothesis (Rrefl : forall t, R t t).
-Hypothesis (Rtrans : forall r s t, R r s -> R s t -> R r t).
-Hypothesis (Rantisym : forall s t, R s t -> R t s -> s = t).
-Hypothesis (tot_lub : forall A : set T, total_on A R -> exists t,
-  (forall s, A s -> R s t) /\ forall r, (forall s, A s -> R s r) -> R t r).
-Hypothesis (Rsucc : forall s, exists t, R s t /\ s <> t /\
-  forall r, R s r -> R r t -> r = s \/ r = t).
-
-Let Teq := @gen_eqMixin T.
-Let Tch := @gen_choiceMixin T.
-Let Tp : pointedType :=  (* FIXME: use HB.pack *)
-  Pointed.Pack (@Pointed.Class T (isPointed.Axioms_ t0) Tch Teq).
-Let lub := fun A : {A : set T | total_on A R} =>
-  [get t : Tp | (forall s, sval A s -> R s t) /\
-    forall r, (forall s, sval A s -> R s r) -> R t r].
-Let succ := fun s => [get t : Tp | R s t /\ s <> t /\
-  forall r, R s r -> R r t -> r = s \/ r = t].
-
-Inductive tower : set T :=
-  | Lub : forall A, sval A `<=` tower -> tower (lub A)
-  | Succ : forall t, tower t -> tower (succ t).
-
-Lemma ZL' : False.
-Proof.
-have lub_ub (A : {A : set T | total_on A R}) :
-  forall s, sval A s -> R s (lub A).
-  suff /getPex [] : exists t : Tp, (forall s, sval A s -> R s t) /\
-    forall r, (forall s, sval A s -> R s r) -> R t r by [].
-  by apply: tot_lub; apply: (svalP A).
-have lub_lub (A : {A : set T | total_on A R}) :
-  forall t, (forall s, sval A s -> R s t) -> R (lub A) t.
-  suff /getPex [] : exists t : Tp, (forall s, sval A s -> R s t) /\
-    forall r, (forall s, sval A s -> R s r) -> R t r by [].
-  by apply: tot_lub; apply: (svalP A).
-have RS s : R s (succ s) /\ s <> succ s.
-  by have /getPex [? []] : exists t : Tp, R s t /\ s <> t /\
-    forall r, R s r -> R r t -> r = s \/ r = t by apply: Rsucc.
-have succS s : forall t, R s t -> R t (succ s) -> t = s \/ t = succ s.
-  by have /getPex [? []] : exists t : Tp, R s t /\ s <> t /\
-    forall r, R s r -> R r t -> r = s \/ r = t by apply: Rsucc.
-suff Twtot : total_on tower R.
-  have [R_S] := RS (lub (exist _ tower Twtot)); apply.
-  by apply/Rantisym => //; apply/lub_ub/Succ/Lub.
-move=> s t Tws; elim: Tws t => {s} [A sATw ihA|s Tws ihs] t Twt.
-  have [?|/asboolP] := pselect (forall s, sval A s -> R s t).
-    by left; apply: lub_lub.
-  rewrite asbool_neg => /existsp_asboolPn [s /asboolP].
-  rewrite asbool_neg => /imply_asboolPn [As nRst]; right.
-  by have /lub_ub := As; apply: Rtrans; have [] := ihA _ As _ Twt.
-suff /(_ _ Twt) [Rts|RSst] : forall r, tower r -> R r s \/ R (succ s) r.
-    by right; apply: Rtrans Rts _; have [] := RS s.
-  by left.
-move=> r; elim=> {r} [A sATw ihA|r Twr ihr].
-  have [?|/asboolP] := pselect (forall r, sval A r -> R r s).
-    by left; apply: lub_lub.
-  rewrite asbool_neg => /existsp_asboolPn [r /asboolP].
-  rewrite asbool_neg => /imply_asboolPn [Ar nRrs]; right.
-  by have /lub_ub := Ar; apply: Rtrans; have /ihA [] := Ar.
-have [Rrs|RSsr] := ihr; last by right; apply: Rtrans RSsr _; have [] := RS r.
-have : tower (succ r) by apply: Succ.
-move=> /ihs [RsSr|]; last by left.
-by have [->|->] := succS _ _ Rrs RsSr; [right|left]; apply: Rrefl.
-Qed.
-
-End ZL.
-
-Lemma Zorn T (R : T -> T -> Prop) :
+Let total_on_wo_chain (T : Type) (R : rel T) (P : {pred T}) :
+  (forall A, total_on A R -> exists t, forall s, A s -> R s t) ->
+  wo_chain R P -> exists2 z, z \in predT & upper_bound R P z.
+Proof.
+move: R P; elim/Peq : T => T R P Atot RP.
+suff : total_on P R by move=> /Atot[t ARt]; exists t.
+move=> s t Ps Pt; have [| |] := RP [predU (pred1 s) & (pred1 t)].
+- by move=> x; rewrite !inE => /orP[/eqP ->{x}|/eqP ->{x}].
+- by exists s; rewrite !inE eqxx.
+- move=> x [[]]; rewrite !inE => /orP[/eqP ->{x}|/eqP ->{x}].
+  + by move=> /(_ t); rewrite !inE eqxx orbT => /(_ isT) Rst _; left.
+  + by move=> /(_ s); rewrite !inE eqxx => /(_ isT) Rts _; right.
+Qed.
+
+Lemma Zorn (T : Type) (R : rel T) :
   (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) ->
   (forall s t, R s t -> R t s -> s = t) ->
   (forall A : set T, total_on A R -> exists t, forall s, A s -> R s t) ->
   exists t, forall s, R t s -> s = t.
 Proof.
-move=> Rrefl Rtrans Rantisym Rtot_max.
-pose totR := {A : set T | total_on A R}.
-set R' := fun A B : totR => sval A `<=` sval B.
-have R'refl A : R' A A by [].
-have R'trans A B C : R' A B -> R' B C -> R' A C by apply: subset_trans.
-have R'antisym A B : R' A B -> R' B A -> A = B.
-  rewrite /R'; move: A B => [/= A totA] [/= B totB] sAB sBA.
-  by apply: eq_exist; rewrite predeqE=> ?; split=> [/sAB|/sBA].
-have R'tot_lub A : total_on A R' -> exists t, (forall s, A s -> R' s t) /\
-    forall r, (forall s, A s -> R' s r) -> R' t r.
-  move=> Atot.
-  have AUtot : total_on (\bigcup_(B in A) (sval B)) R.
-    move=> s t [B AB Bs] [C AC Ct].
-    have [/(_ _ Bs) Cs|/(_ _ Ct) Bt] := Atot _ _ AB AC.
-      by have /(_ _ _ Cs Ct) := svalP C.
-    by have /(_ _ _ Bs Bt) := svalP B.
-  exists (exist _ (\bigcup_(B in A) sval B) AUtot); split.
-    by move=> B ? ? ?; exists B.
-  by move=> B Bub ? /= [? /Bub]; apply.
-apply: contrapT => nomax.
-have {}nomax t : exists s, R t s /\ s <> t.
-  have /asboolP := nomax; rewrite asbool_neg => /forallp_asboolPn /(_ t).
-  move=> /asboolP; rewrite asbool_neg => /existsp_asboolPn [s].
-  by move=> /asboolP; rewrite asbool_neg => /imply_asboolPn []; exists s.
-have tot0 : total_on set0 R by [].
-apply: (ZL' (exist _ set0 tot0)) R'tot_lub _ => // A.
-have /Rtot_max [t tub] := svalP A; have [s [Rts snet]] := nomax t.
-have Astot : total_on (sval A `|` [set s]) R.
-  move=> u v [Au|->]; last first.
-    by move=> [/tub Rvt|->]; right=> //; apply: Rtrans Rts.
-  move=> [Av|->]; [apply: (svalP A)|left] => //.
-  by apply: Rtrans Rts; apply: tub.
-exists (exist _ (sval A `|` [set s]) Astot); split; first by move=> ? ?; left.
-split=> [AeAs|[B Btot] sAB sBAs].
-  have [/tub Rst|] := pselect (sval A s); first exact/snet/Rantisym.
-  by rewrite AeAs /=; apply; right.
-have [Bs|nBs] := pselect (B s).
-  by right; apply: eq_exist; rewrite predeqE => r; split=> [/sBAs|[/sAB|->]].
-left; case: A tub Astot sBAs sAB => A Atot /= tub Astot sBAs sAB.
-apply: eq_exist; rewrite predeqE => r; split=> [Br|/sAB] //.
-by have /sBAs [|ser] // := Br; rewrite ser in Br.
+move: R; elim/Peq : T => T R Rxx Rtrans Ranti Atot.
+have [//| |P _ RP|] := @Zorn's_lemma _ R predT _.
+- by move=> ? ? ? _ _ _; exact: Rtrans.
+- exact: total_on_wo_chain.
+by move=> x _ Rx; exists x => s Rxs; apply: (Ranti _ _ _ Rxs) => //; exact: Rx.
+Qed.
+
+Definition premaximal T (R : T -> T -> Prop) (t : T) :=
+  forall s, R t s -> R s t.
+
+Lemma ZL_preorder (T : Type) (t0 : T) (R : rel T) :
+  (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) ->
+  (forall A, total_on A R -> exists t, forall s, A s -> R s t) ->
+  exists t, premaximal R t.
+Proof.
+move: t0 R; elim/Peq : T => T t0 R Rxx Rtrans Atot.
+have [//| | |z _ Hz] := @Zorn's_lemma T R predT.
+- by move=> ? ? ? _ _ _; exact: Rtrans.
+- by move=> A _ RA; exact: total_on_wo_chain.
+by exists z => s Rzs; exact: Hz.
 Qed.
 
+End Zorn.
+
 Section Zorn_subset.
 Variables (T : Type) (P : set (set T)).
 
@@ -2728,20 +2656,24 @@ Lemma Zorn_bigcup :
       P (\bigcup_(X in F) X)) ->
   exists A, P A /\ forall B, A `<` B -> ~ P B.
 Proof.
-move=> totP; pose R (sA sB : P) := sval sA `<=` sval sB.
+move=> totP; pose R (sA sB : P) := `[< sval sA `<=` sval sB >].
 have {}totR F (FR : total_on F R) : exists sB, forall sA, F sA -> R sA sB.
    have FP : [set val x | x in F] `<=` P.
-     by move=> _ [X FX <-]; apply: set_mem; apply: valP.
+     by move=> _ [X FX <-]; exact/set_mem/valP.
    have totF : total_on [set val x | x in F] subset.
-     by move=> _ _ [X FX <-] [Y FY <-]; apply: FR.
-   exists (SigSub (mem_set (totP _ FP totF))) => A FA; rewrite /R/=.
-   exact: (bigcup_sup (imageP val _)).
+     move=> _ _ [X FX <-] [Y FY <-].
+     by have [/asboolP|/asboolP] := FR _ _ FX FY; [left|right].
+   exists (SigSub (mem_set (totP _ FP totF))) => A FA.
+   exact/asboolP/(bigcup_sup (imageP val _)).
 have [| | |sA sAmax] := Zorn _ _ _ totR.
-- by move=> ?; exact: subset_refl.
-- by move=> ? ? ?; exact: subset_trans.
-- by move=> [A PA] [B PB]; rewrite /R /= => AB BA; exact/eq_exist/seteqP.
+- by move=> ?; apply/asboolP; exact: subset_refl.
+- by move=> ? ? ? /asboolP ? /asboolP st; apply/asboolP; exact: subset_trans st.
+- by move=> [A PA] [B PB] /asboolP AB /asboolP BA; exact/eq_exist/seteqP.
 - exists (val sA); case: sA => A PA /= in sAmax *; split; first exact: set_mem.
-  move=> B AB PB; have [BA] := sAmax (SigSub (mem_set PB)) (properW AB).
+  move=> B AB PB.
+  have : R (exist (fun x : T -> Prop => x \in P) A PA) (SigSub (mem_set PB)).
+    by apply/asboolP; exact: properW.
+  move=> /(sAmax (SigSub (mem_set PB)))[BA].
   by move: AB; rewrite BA; exact: properxx.
 Qed.
 
@@ -2775,58 +2707,6 @@ Qed.
 
 End maximal_disjoint_subcollection.
 
-Definition premaximal T (R : T -> T -> Prop) (t : T) :=
-  forall s, R t s -> R s t.
-
-Lemma ZL_preorder T (t0 : T) (R : T -> T -> Prop) :
-  (forall t, R t t) -> (forall r s t, R r s -> R s t -> R r t) ->
-  (forall A : set T, total_on A R -> exists t, forall s, A s -> R s t) ->
-  exists t, premaximal R t.
-Proof.
-set Teq := @gen_eqMixin T; set Tch := @gen_choiceMixin T.
-pose Tpo := isPointed.Build T t0.
-pose Tp : pointedType := HB.pack T Teq Tch Tpo.
-move=> Rrefl Rtrans tot_max.
-set eqR := fun s t => R s t /\ R t s; set ceqR := fun s => [set t | eqR s t].
-have eqR_trans r s t : eqR r s -> eqR s t -> eqR r t.
-  by move=> [Rrs Rsr] [Rst Rts]; split; [apply: Rtrans Rst|apply: Rtrans Rsr].
-have ceqR_uniq s t : eqR s t -> ceqR s = ceqR t.
-  by rewrite predeqE => - [Rst Rts] r; split=> [[Rr rR] | [Rr rR]]; split;
-    try exact: Rtrans Rr; exact: Rtrans rR _.
-set ceqRs := ceqR @` setT; set quotR := sig ceqRs.
-have ceqRP t : ceqRs (ceqR t) by exists t.
-set lift := fun t => exist _ (ceqR t) (ceqRP t).
-have lift_surj (A : quotR) : exists t : Tp, lift t = A.
-  case: A => A [t Tt ctA]; exists t; rewrite /lift; case : _ / ctA.
-  exact/congr1/Prop_irrelevance.
-have lift_inj s t : eqR s t -> lift s = lift t.
-  by move=> eqRst; apply/eq_exist/ceqR_uniq.
-have lift_eqR s t : lift s = lift t -> eqR s t.
-  move=> cst; have ceqst : ceqR s = ceqR t by have := congr1 sval cst.
-  by rewrite [_ s]ceqst; split; apply: Rrefl.
-set repr := fun A : quotR => get [set t : Tp | lift t = A].
-have repr_liftE t : eqR t (repr (lift t))
-  by apply: lift_eqR; have -> := getPex (lift_surj (lift t)).
-set R' := fun A B : quotR => R (repr A) (repr B).
-have R'refl A : R' A A by apply: Rrefl.
-have R'trans A B C : R' A B -> R' B C -> R' A C by apply: Rtrans.
-have R'antisym A B : R' A B -> R' B A -> A = B.
-  move=> RAB RBA; have [t tA] := lift_surj A; have [s sB] := lift_surj B.
-  rewrite -tA -sB; apply: lift_inj; apply (eqR_trans _ _ _ (repr_liftE t)).
-  have eAB : eqR (repr A) (repr B) by [].
-  rewrite tA; apply: eqR_trans eAB _; rewrite -sB.
-  by have [] := repr_liftE s.
-have [A Atot|A Amax] := Zorn R'refl R'trans R'antisym.
-  have /tot_max [t tmax] : total_on [set repr B | B in A] R.
-    by move=> ?? [B AB <-] [C AC <-]; apply: Atot.
-  exists (lift t) => B AB; have [Rt _] := repr_liftE t.
-  by apply: Rtrans Rt; apply: tmax; exists B.
-exists (repr A) => t RAt.
-have /Amax <- : R' A (lift t).
-  by have [Rt _] := repr_liftE t; apply: Rtrans Rt.
-by have [] := repr_liftE t.
-Qed.
-
 Section UpperLowerTheory.
 Import Order.TTheory.
 Variables (d : unit) (T : porderType d).

classical/mathcomp_extra.v

@@ -1,6 +1,5 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 Require Import BinPos.
-From mathcomp Require choice.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import finset interval.
 

classical/wochoice.v

@@ -171,7 +171,7 @@ have init_total Y Z: f_ind Y -> f_ind Z -> {init_seg Y Z} + {init_seg Z Y}.
     rewrite -(fY z Yz); congr f; apply/esym/funext=> x /=.
     apply/idP/idP=> [/andP[Yx] | Ix]; first by contra=> I'x; apply/minYz/andP.
     have Yx := sIY x Ix; rewrite Yx /=; contra: (I'z) => Rzx.
-    by rewrite (RYanti z x) // Rzx RIY.    
+    by rewrite (RYanti z x) // Rzx RIY.
   case: iI1Y {iI1}(iI1 Z) => [<- _| iI1Y [||<-|iI1Z]//]; [by left | by right |].
   by case/notCf/negP: Ich; apply/(maxI I1); [apply/asboolP|apply/predU1l].
 pose U x := `[< exists2 X, x \in X & f_ind X >].
@@ -182,7 +182,7 @@ have Umax X: f_ind X -> init_seg X U.
 have RUanti: {in U &, antisymmetric R}.
   move=> x y /asboolP[X Xx indX] /asboolP[Y Yy indY].
   without loss [sXY _]: x y X Y Xx Yy {indX} indY / init_seg X Y.
-    move=> IH. 
+    move=> IH.
     by case: (init_total X Y) => // {}/IH-IH; [|rewrite andbC] => /IH->.
   have [/wo_chain_antisymmetric RYanti _] := indY.
   by apply: RYanti => //; apply: sXY.
@@ -323,7 +323,7 @@ have /maxR/(_ _)/asboolP: ([predU1 z & D] : pred T, Rz : rel T) \in pwo.
     have /minXy/= := Xx; case: ifP => // _ /idPn[].
     by rewrite negb_or andbT (memPn notDz).
   apply: Ux; split=> [|t /andP[/minXy]]; first exact/andP.
-  by rewrite /= Dy => /predU1P[-> /idPn[]|].   
+  by rewrite /= Dy => /predU1P[-> /idPn[]|].
 case=> [|/= -> //]; last exact/predU1l.
 apply/asboolP; split=> [x|x y /= Dx]; first exact: predU1r.
 rewrite Dx => /predU1P[-> | /= Dy]; first by rewrite eqxx (negPf notDz).

theories/forms.v

@@ -2,7 +2,7 @@ From HB Require Import structures.
 From mathcomp
 Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum.
 From mathcomp
-Require Import matrix mxalgebra vector falgebra ssrnum algC algnum.
+Require Import matrix mxalgebra vector falgebra ssrnum.
 From mathcomp
 Require Import fieldext.
 From mathcomp Require Import vector.

theories/topology.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
-From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
 Require Import reals signed.
 
@@ -3040,34 +3040,39 @@ Lemma ultraFilterLemma T (F : set_system T) :
 Proof.
 move=> FF.
 set filter_preordset := ({G : set_system T & ProperFilter G /\ F `<=` G}).
-set preorder := fun G1 G2 : filter_preordset => projT1 G1 `<=` projT1 G2.
-suff [G Gmax] : exists G : filter_preordset, premaximal preorder G.
-  have [GF sFG] := projT2 G; exists (projT1 G); split=> //; split=> // H HF sGH.
+set preorder :=
+  fun G1 G2 : {classic filter_preordset} => `[< projT1 G1 `<=` projT1 G2 >].
+suff [G Gmax] : exists G : {classic filter_preordset}, premaximal preorder G.
+  have [GF sFG] := projT2 G; exists (projT1 G); split; last exact: sFG.
+  split; [exact: GF|move=> H HF sGH].
   have sFH : F `<=` H by apply: subset_trans sGH.
-  have sHG : preorder (existT _ H (conj HF sFH)) G by apply: Gmax.
-  by rewrite predeqE => ?; split=> [/sHG|/sGH].
+  have sHG : preorder (existT _ H (conj HF sFH)) G.
+    by move/asboolP in sGH; exact: (Gmax (existT _ H (conj HF sFH)) sGH).
+  by rewrite predeqE => A; split; [move/asboolP : sHG; exact|exact: sGH].
 have sFF : F `<=` F by [].
-apply: (ZL_preorder ((existT _ F (conj FF sFF)) : filter_preordset)) =>
-  [?|G H I sGH sHI ? /sGH /sHI|A Atot] //.
-case: (pselect (A !=set0)) => [[G AG] | A0]; last first.
-  exists (existT _ F (conj FF sFF)) => G AG.
-  by have /asboolP := A0; rewrite asbool_neg => /forallp_asboolPn /(_ G).
-have [GF sFG] := projT2 G.
-suff UAF : ProperFilter (\bigcup_(H in A) projT1 H).
-  have sFUA : F `<=` \bigcup_(H in A) projT1 H.
-    by move=> B FB; exists G => //; apply: sFG.
-  exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH B HB /=.
-  by exists H.
-apply: Build_ProperFilter.
-  by move=> B [H AH HB]; have [HF _] := projT2 H; apply: (@filter_ex _ _ HF).
-split; first by exists G => //; apply: filterT.
-  move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC.
-    exists HC => //; have [HCF _] := projT2 HC; apply: filterI HCC.
-    exact: sHBC.
-  exists HB => //; have [HBF _] := projT2 HB; apply: filterI HBB _.
-  exact: sHCB.
-move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H.
-exact: filterS HB.
+apply: (ZL_preorder (existT _ F (conj FF sFF))).
+- by move=> t; exact/asboolP.
+- move=> r s t; rewrite /preorder => /asboolP sr /asboolP st.
+  exact/asboolP/(subset_trans _ st).
+- move=> A Atot; have [[G AG] | A0] := pselect (A !=set0); last first.
+    exists (existT _ F (conj FF sFF)) => G AG.
+    by have /asboolP := A0; rewrite asbool_neg => /forallp_asboolPn /(_ G).
+  have [GF sFG] := projT2 G.
+  suff UAF : ProperFilter (\bigcup_(H in A) projT1 H).
+    have sFUA : F `<=` \bigcup_(H in A) projT1 H.
+      by move=> B FB; exists G => //; exact: sFG.
+    exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH.
+    by apply/asboolP => B HB /=; exists H.
+  apply: Build_ProperFilter.
+    by move=> B [H AH HB]; have [HF _] := projT2 H; exact: (@filter_ex _ _ HF).
+  split; first by exists G => //; apply: filterT.
+  + move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC.
+    * exists HC => //; have [HCF _] := projT2 HC; apply: filterI HCC.
+      by move/asboolP : sHBC; exact.
+    * exists HB => //; have [HBF _] := projT2 HB; apply: filterI HBB _.
+      by move/asboolP : sHCB; exact.
+  + move=> B C SBC [H AH HB]; exists H => //; have [HF _] := projT2 H.
+    exact: filterS HB.
 Qed.
 
 Lemma compact_ultra (T : topologicalType) :