renaming sets_of

CHANGELOG_UNRELEASED.md

@@ -55,8 +55,8 @@
   + globals `subspace_filter`, `subspace_proper_filter`
   + notation `{within ..., continuous ...}`
 - in `topology.v`:
-  + Definition `sets_of`
-  + globals `sets_of_filter`, 
+  + Definition `powerset_filter_from`
+  + globals `powerset_filter_from_filter`, 
   + lemmas `near_small_set`, `small_set_sub`
   + lemmas `withinET`, `closureEcvg`, `entourage_sym`, `fam_nbhs`
   + generalize `cluster_cvgE`, `ptws_cvg_compact_family`

theories/topology.v

@@ -103,7 +103,7 @@ Require Import mathcomp_extra boolp reals classical_sets signed functions.
 (*                                     domain D.                              *)
 (*                subset_filter F D == similar to within D F, but with        *)
 (*                                     dependent types.                       *)
-(*                        sets_of F == The filter of downward closed subsets  *)
+(*           powerset_filter_from F == The filter of downward closed subsets  *)
 (*                                     of F. Enables use of near notation to  *)
 (*                                     pick suitably small members of F       *)
 (*                      in_filter F == interface type for the sets that       *)
@@ -1590,12 +1590,12 @@ Section NearSet.
 Context {T : choiceType} {Y : filteredType T}.
 Context (F : set (set Y)) (PF : ProperFilter F).
 
-Definition sets_of : set (set (set Y)) := filter_from
+Definition powerset_filter_from : set (set (set Y)) := filter_from
   [set M | [/\ M `<=` F,
     (forall E1 E2, M E1 -> F E2 -> E2 `<=` E1 -> M E2) & M !=set0 ] ]
   id.
 
-Global Instance sets_of_filter : ProperFilter sets_of.
+Global Instance powerset_filter_from_filter : ProperFilter powerset_filter_from.
 Proof.
 split.
   rewrite (_ : xpredp0 = set0); last by rewrite eqEsubset; split.
@@ -1615,10 +1615,11 @@ exists [set E | exists P Q, [/\ M P, N Q & E = P `&` Q] ]; first split.
   by split; [apply: (subM _ _ MP) | apply: (subN _ _ MQ)] => // ? [].
 Qed.
 
-Lemma near_small_set : \forall E \near sets_of, F E.
+Lemma near_small_set : \forall E \near powerset_filter_from, F E.
 Proof. by exists F => //; split => //; exists setT; exact: filterT. Qed.
 
-Lemma small_set_sub (E : set Y) : F E -> \forall E' \near sets_of, E' `<=` E.
+Lemma small_set_sub (E : set Y) : F E -> 
+  \forall E' \near powerset_filter_from, E' `<=` E.
 Proof.
 move=> entE; exists [set E' | F E' /\ E' `<=` E]; last by move=> ? [].
 split; [by move=> E' [] | | by exists E; split].
@@ -2713,7 +2714,7 @@ Qed.
 End Compact.
 Arguments hausdorff_space : clear implicits.
 
-Lemma near_compact_covering {X : topologicalType} {Y : topologicalType}
+Lemma near_compact_covering {X : Type} {Y : topologicalType}
     (F : set (set X)) (Q P : X -> Y -> Prop) (K : set Y) :
   Filter F -> compact K ->
   (forall y, K y -> \forall x \near F, Q x y) ->
@@ -6050,7 +6051,7 @@ Qed.
 Definition pointwise_precompact {I} (W : set I) (d : I -> X -> Y) :=
   forall x, precompact [set (d i x) | i in W].
 
-Lemma pointwise_precomact_subset {I} (W V : set I) (fW fV : I -> (X -> Y)):
+Lemma pointwise_precompact_subset {I J} (W : set I) (V : set J) {fW : I -> X -> Y} {fV : J -> X -> Y}:
   fW @` W `<=` fV @` V -> pointwise_precompact V fV -> 
   pointwise_precompact W fW.
 Proof.
@@ -6131,7 +6132,7 @@ apply/fam_cvgP => K ? U /=; rewrite uniform_nbhs => [[E [? EsubU]]].
 suff : \forall g \near within W (nbhs f), forall y, K y -> E (f y, g y).
   rewrite near_withinE; near_simpl => N; apply: (filter_app _ _ FW).
   by apply ptwsF; near=> g => ?; apply EsubU; apply: (near N g).
-near (sets_of (@entourage Y)) => E'.
+near (powerset_filter_from (@entourage Y)) => E'.
 have entE' : entourage E' by exact: (near (near_small_set _)).
 pose Q := fun (h : X -> Y) x => E' (f x, h x).
 apply: (@near_compact_covering _ _ _ Q) => //.
@@ -6178,7 +6179,7 @@ Lemma compact_equicontinuous (W : set {family compact, X -> Y}) :
 Proof.
 move=> lcptX ctsW cptW x E entE.
 have [//|U UWx [cptU clU]] := lcptX x; rewrite withinET in UWx.
-near (sets_of (@entourage Y)) => E'.
+near (powerset_filter_from (@entourage Y)) => E'.
 have entE' : entourage E' by exact: (near (near_small_set _)).
 pose Q := fun (y : X) (f : {family compact, X -> Y}) => E' (f x, f y).
 apply: (@near_compact_covering _ _ _ Q) => // f; rewrite /Q; near_simpl.