set (set _) -> set_system

Author: affeldt-aist

classical/classical_sets.v

@@ -1699,7 +1699,7 @@ Qed.
 End rectangle.
 
 Definition preimage_set_system {aT rT : Type} (D : set aT) (f : aT -> rT)
-    (G : set_system rT) : set (set aT) :=
+    (G : set_system rT) : set_system aT :=
   [set D `&` f @^-1` B | B in G].
 
 Lemma preimage_set_system0 {aT rT : Type} (D : set aT) (f : aT -> rT) :
@@ -1720,7 +1720,7 @@ apply/seteqP; split=> [_ [B FB] <-|_ [_ [C FC <-] <-]].
 by exists C => //; rewrite setTI comp_preimage.
 Qed.
 
-Lemma preimage_set_system_id {aT : Type} (D : set aT) (F : set (set aT)) :
+Lemma preimage_set_system_id {aT : Type} (D : set aT) (F : set_system aT) :
   preimage_set_system D idfun F = setI D @` F.
 Proof. by []. Qed.
 
@@ -1730,7 +1730,7 @@ Lemma preimage_set_systemS {T1 T2} (A B : set_system T2) (f : T1 -> T2) :
 Proof. by move=> AB _ [C ? <-]; exists C => //; exact: AB. Qed.
 
 Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT)
-    (G : set (set aT)) : set (set rT) :=
+    (G : set_system aT) : set_system rT :=
   [set B : set rT | G (D `&` f @^-1` B)].
 
 Section cross.
@@ -1746,15 +1746,15 @@ End cross.
 Definition cross12 {T1 T2 : Type} := @cross (T1 * T2)%type T1 T2 fst snd.
 Notation "A `x` B" := (cross12 A B) : classical_set_scope.
 
-Lemma subKimage {T T'} {P : set (set T')} (f : T -> T') (g : T' -> T) :
+Lemma subKimage {T T'} {P : set_system T'} (f : T -> T') (g : T' -> T) :
   cancel f g -> [set A | P (f @` A)] `<=` [set g @` A | A in P].
 Proof. by move=> ? A; exists (f @` A); rewrite ?image_comp ?eq_image_id/=. Qed.
 
-Lemma subimageK T T' (P : set (set T')) (f : T -> T') (g : T' -> T) :
+Lemma subimageK T T' (P : set_system T') (f : T -> T') (g : T' -> T) :
   cancel g f -> [set g @` A | A in P] `<=` [set A | P (f @` A)].
 Proof. by move=> gK _ [B /= ? <-]; rewrite image_comp eq_image_id/=. Qed.
 
-Lemma eq_imageK {T T'} {P : set (set T')} (f : T -> T') (g : T' -> T) :
+Lemma eq_imageK {T T'} {P : set_system T'} (f : T -> T') (g : T' -> T) :
     cancel f g -> cancel g f ->
   [set g @` A | A in P] = [set A | P (f @` A)].
 Proof.
@@ -3009,10 +3009,10 @@ Qed.
 End Zorn.
 
 Section Zorn_subset.
-Variables (T : Type) (P : set (set T)).
+Variables (T : Type) (P : set_system T).
 
 Lemma Zorn_bigcup :
-    (forall F : set (set T), F `<=` P -> total_on F subset ->
+    (forall F : set_system T, F `<=` P -> total_on F subset ->
       P (\bigcup_(X in F) X)) ->
   exists A, P A /\ forall B, A `<` B -> ~ P B.
 Proof.
@@ -3049,7 +3049,7 @@ Variables (B : I -> set T) (D : set I).
 
 Let P := fun X => X `<=` D /\ trivIset X B.
 
-Let maxP (A : set (set I)) :
+Let maxP (A : set_system I) :
   A `<=` P -> total_on A (fun x y => x `<=` y) -> P (\bigcup_(x in A) x).
 Proof.
 move=> AP h; split; first by apply: bigcup_sub => E /AP [].
@@ -3223,30 +3223,28 @@ rewrite -Order.TotalTheory.ltNge => kn.
 by rewrite (Order.POrderTheory.le_trans _ (Am _ Ak)).
 Qed.
 
-Definition meets T (F G : set (set T)) :=
+Definition meets T (F G : set_system T) :=
   forall A B, F A -> G B -> A `&` B !=set0.
 
 Notation "F `#` G" := (meets F G) : classical_set_scope.
 
 Section meets.
 
-Lemma meetsC T (F G : set (set T)) : F `#` G = G `#` F.
+Lemma meetsC T (F G : set_system T) : F `#` G = G `#` F.
 Proof.
 gen have sFG : F G / F `#` G -> G `#` F.
   by move=> FG B A => /FG; rewrite setIC; apply.
 by rewrite propeqE; split; apply: sFG.
 Qed.
 
-Lemma sub_meets T (F F' G G' : set (set T)) :
+Lemma sub_meets T (F F' G G' : set_system T) :
   F `<=` F' -> G `<=` G' -> F' `#` G' -> F `#` G.
 Proof. by move=> sF sG FG A B /sF FA /sG GB; apply: (FG A B). Qed.
 
-Lemma meetsSr T (F G G' : set (set T)) :
-  G `<=` G' -> F `#` G' -> F `#` G.
+Lemma meetsSr T (F G G' : set_system T) : G `<=` G' -> F `#` G' -> F `#` G.
 Proof. exact: sub_meets. Qed.
 
-Lemma meetsSl T (G F F' : set (set T)) :
-  F `<=` F' -> F' `#` G -> F `#` G.
+Lemma meetsSl T (G F F' : set_system T) : F `<=` F' -> F' `#` G -> F `#` G.
 Proof. by move=> /sub_meets; apply. Qed.
 
 End meets.

classical/filter.v

@@ -1211,7 +1211,7 @@ Canonical within_filter_on T D (F : filter_on T) :=
   FilterType (within D F) (within_filter _ _).
 
 Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T)
-  (F : set (set T)) (P : set T) :
+  (F : set_system T) (P : set T) :
   Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) ->
   F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]).
 Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed.
@@ -1479,7 +1479,7 @@ End UltraFilters.
 
 Section filter_supremums.
 
-Global Instance smallest_filter_filter {T : Type} (F : set (set T)) :
+Global Instance smallest_filter_filter {T : Type} (F : set_system T) :
   Filter (smallest Filter F).
 Proof.
 split.
@@ -1488,21 +1488,21 @@ split.
 - by move=> ? ? /filterS + sFP ? [? ?]; apply; exact: sFP.
 Qed.
 
-Fixpoint filterI_iter {T : Type} (F : set (set T)) (n : nat) :=
+Fixpoint filterI_iter {T : Type} (F : set_system T) (n : nat) :=
   if n is m.+1
   then [set P `&` Q |
     P in filterI_iter F m & Q in filterI_iter F m]
   else setT |` F.
 
-Lemma filterI_iter_sub {T : Type} (F : set (set T)) :
+Lemma filterI_iter_sub {T : Type} (F : set_system T) :
   {homo filterI_iter F : i j / (i <= j)%N >-> i `<=` j}.
 Proof.
 move=> + j; elim: j; first by move=> i; rewrite leqn0 => /eqP ->.
 move=> j IH i; rewrite leq_eqVlt => /predU1P[->//|].
 by move=> /IH/subset_trans; apply=> A ?; do 2 exists A => //; rewrite setIid.
 Qed.
 
-Lemma filterI_iterE {T : Type} (F : set (set T)) :
+Lemma filterI_iterE {T : Type} (F : set_system T) :
   smallest Filter F = filter_from (\bigcup_n (filterI_iter F n)) id.
 Proof.
 rewrite eqEsubset; split.

theories/cantor.v

@@ -397,7 +397,7 @@ Context (t0 t1 : T).
 Hypothesis T2e : t0 != t1.
 
 Let ent_balls' (E : set (T * T)) :
-  exists M : set (set T), entourage E -> [/\
+  exists M : set_system T, entourage E -> [/\
     finite_set M,
     forall A, M A -> exists a, A a /\
       A `<=` closure (xsection (split_ent E) a),

theories/derive.v

@@ -69,22 +69,22 @@ Reserved Notation "f ^` ( n )" (format "f ^` ( n )").
 Section Differential.
 Context {K : numDomainType} {V W : normedModType K}.
 
-Definition diff (F : filter_on V) (_ : phantom (set (set V)) F) (f : V -> W) :=
+Definition diff (F : filter_on V) (_ : phantom (set_system V) F) (f : V -> W) :=
   (get (fun (df : {linear V -> W}) => continuous df /\ forall x,
       f x = f (lim F) + df (x - lim F) +o_(x \near F) (x - lim F))).
 
 Local Notation "''d' f x" := (@diff _ (Phantom _ (nbhs x)) f).
 
 Fact diff_key : forall T, T -> unit. Proof. by constructor. Qed.
 Variant differentiable_def (f : V -> W) (x : filter_on V)
-  (phF : phantom (set (set V)) x) : Prop := DifferentiableDef of
+  (phF : phantom (set_system V) x) : Prop := DifferentiableDef of
   (continuous ('d f x) /\
   f = cst (f (lim x)) + 'd f x \o center (lim x) +o_x (center (lim x))).
 
 Local Notation differentiable f F :=
   (@differentiable_def f _ (Phantom _ (nbhs F))).
 
-Class is_diff_def (x : filter_on V) (Fph : phantom (set (set V)) x) (f : V -> W)
+Class is_diff_def (x : filter_on V) (Fph : phantom (set_system V) x) (f : V -> W)
   (df : V -> W) := DiffDef {
     ex_diff : differentiable f x ;
     diff_val : 'd f x = df :> (V -> W)

theories/esum.v

@@ -41,7 +41,7 @@ Section set_of_fset_in_a_set.
 Variable (T : choiceType).
 Implicit Type S : set T.
 
-Definition fsets S : set (set T) := [set F | finite_set F /\ F `<=` S].
+Definition fsets S : set_system T := [set F | finite_set F /\ F `<=` S].
 
 Lemma fsets_set0 S : fsets S set0. Proof. by split. Qed.
 

theories/kernel.v

@@ -930,7 +930,7 @@ Lemma measurable_fun_mnormalize d d' (X : measurableType d)
     (Y : pmeasurableType d') (R : realType) (k : R.-ker X ~> Y) :
   measurable_fun [set: X] (fun x => mnormalize (k x) point : pprobability Y R).
 Proof.
-apply: (measurability (@pset _ _ _ : set (set (pprobability Y R)))) => //.
+apply: (measurability (@pset _ _ _ : set_system (pprobability Y R))) => //.
 move=> _ -[_ [r r01] [Ys mYs <-]] <-.
 rewrite /mnormalize /mset /preimage/=.
 apply: emeasurable_fun_infty_o => //.

theories/landau.v

@@ -392,7 +392,7 @@ Lemma littleoE (tag : unit) (F : filter_on T)
 Proof. by move=> /asboolP?; rewrite /the_littleo /insubd insubT. Qed.
 
 Lemma littleoE0 (tag : unit) (F : filter_on T)
-   (phF : phantom (set (set T)) F) f h :
+   (phF : phantom (set_system T) F) f h :
    ~ littleo_def F f h -> the_littleo tag F phF f h = 0.
 Proof. by move=> ?; rewrite /the_littleo /insubd insubN//; apply/asboolP. Qed.
 

theories/lebesgue_integral_theory/lebesgue_integral_fubini.v

@@ -391,7 +391,7 @@ have UFGT : \bigcup_k (F k `*` G k) = setT.
   move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split.
   - by move: x Fnx; exact/subsetPset/ndF/leq_maxl.
   - by move: y Gky; exact/subsetPset/ndG/leq_maxr.
-pose C : set (set (T1 * T2)) :=
+pose C : set_system (T1 * T2) :=
   [set C | exists A, measurable A /\ exists B, measurable B /\ C = A `*` B].
 have CI : setI_closed C.
   move=> /= _ _ [X1 [mX1 [X2 [mX2 ->]]]] [Y1 [mY1 [Y2 [mY2 ->]]]].

theories/lebesgue_stieltjes_measure.v

@@ -177,7 +177,7 @@ HB.instance Definition _ :=
 End itv_semiRingOfSets.
 
 Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
-Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type R))) :
+Notation "R .-ocitv.-measurable" := (measurable : set_system (ocitv_type R)) :
   classical_set_scope.
 
 Local Open Scope measure_display_scope.
@@ -519,9 +519,8 @@ Definition measurableTypeR (R : realType) :=
 Section lebesgue_stieltjes_measure.
 Context {R : realType}.
 
-Definition lebesgue_display : measure_display :=
-  (R.-ocitv.-measurable).-sigma.
-Definition measurableR : set (set R) :=
+Definition lebesgue_display : measure_display := (R.-ocitv.-measurable).-sigma.
+Definition measurableR : set_system R :=
   (R.-ocitv.-measurable).-sigma.-measurable.
 
 HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) :=

theories/measurable_realfun.v

@@ -93,10 +93,10 @@ Qed.
 End ps_infty.
 
 Section salgebra_ereal.
-Variables (R : realType) (G : set (set R)).
-Let measurableR : set (set R) := G.-sigma.-measurable.
+Variables (R : realType) (G : set_system R).
+Let measurableR : set_system R := G.-sigma.-measurable.
 
-Definition emeasurable : set (set \bar R) :=
+Definition emeasurable : set_system (\bar R) :=
   [set EFin @` A `|` B | A in measurableR & B in ps_infty].
 
 Lemma emeasurable0 : emeasurable set0.
@@ -418,7 +418,7 @@ Section rgencinfty.
 Variable R : realType.
 Implicit Types x y z : R.
 
-Definition G : set (set R) := [set A | exists x, A = `[x, +oo[%classic].
+Definition G : set_system R := [set A | exists x, A = `[x, +oo[%classic].
 
 Lemma measurable_itv_bnd_infty b x :
   G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].
@@ -1184,7 +1184,7 @@ Module NGenCInfty.
 Section ngencinfty.
 Implicit Types x y z : nat.
 
-Definition G : set (set nat) := [set A | exists x, A = `[x, +oo[%classic].
+Definition G : set_system nat := [set A | exists x, A = `[x, +oo[%classic].
 
 Lemma measurable_itv_bnd_infty b x :
   G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].