nitpicking

CHANGELOG_UNRELEASED.md

@@ -11,11 +11,13 @@
 - in `topology.v`:
   + definitions `compact_near`, `precompact`, `locally_compact`
   + lemmas `precompactE`, `precompact_subset`, `compact_precompact`, 
-      `precompact_closed`
-  + definitions `equicontinuous`, `pointwise_precompact`
+    `precompact_closed`
+  + definitions `singletons`, `equicontinuous`, `pointwise_precompact`
   + lemmas `equicontinuous_subset`, `equicontinuous_cts`
   + lemmas `pointwise_precomact_subset`, `pointwise_precompact_precompact`
-      `uniform_pointwise_compact`, `compact_pointwise_precompact`
+    `uniform_pointwise_compact`, `compact_pointwise_precompact`
+  + lemmas `compact_set1`, `uniform_set1`, `ptws_cvg_family_singleton`,
+    `ptws_cvg_compact_family`
 
 ### Changed
 

theories/topology.v

@@ -339,7 +339,8 @@ Require Import boolp reals classical_sets posnum.
 (*                               inclusion of subspace A into T               *)
 (*                                                                            *)
 (* * Arzela Ascoli' theorem :                                                 *)
-(*  equicontinuous W x     == the set (W : X -> Y) is equicontinuous at x     *)
+(*            singletons T := [set [set x] | x in [set: T]].                  *)
+(*      equicontinuous W x == the set (W : X -> Y) is equicontinuous at x     *)
 (*  pointwise_precompact W == For each (x : X), set of images [f x | f in W]  *)
 (*                            is precompact                                   *)
 (*                                                                            *)
@@ -2712,11 +2713,10 @@ Qed.
 
 Lemma compact_set1 (x : T) : compact [set x].
 Proof.
-  move=> F PF Fx; exists x; split; first by [].
-  move=> P B nbhsB; exists x; split; last by exact: nbhs_singleton.
-  have [y [Py]] : (P `&` [set x] !=set0).
-    by apply: filter_ex; [exact: PF| exact: filterI].
-  by move=> <-.
+move=> F PF Fx; exists x; split; first by [].
+move=> P B nbhsB; exists x; split; last exact: nbhs_singleton.
+suff [y [Py <-//]] : P `&` [set x] !=set0.
+by apply: filter_ex; [exact: PF| exact: filterI].
 Qed.
 
 End Compact.
@@ -2902,42 +2902,40 @@ Context {X : topologicalType}.
 
 (* The closed condition here is neccessary to make this definition work in a  *)
 (* non-hausdorff setting.                                                     *)
-Definition compact_near (F : set (set X)) := 
+Definition compact_near (F : set (set X)) :=
   exists2 U, F U & compact U /\ closed U.
 
 Definition precompact (C : set X) := compact_near (globally C).
 
-Lemma precompactE (C : set X) : 
-  precompact C = compact (closure C).
+Lemma precompactE (C : set X) : precompact C = compact (closure C).
 Proof.
-rewrite propeqE; split; last first.
-  move=> clC; (exists (closure C) => //); first exact: subset_closure.
-  by split => //; apply: closed_closure.
-move=> [B CsubB [cptB cB]]; apply: (subclosed_compact _ cptB). 
-  exact: closed_closure.
+rewrite propeqE; split=> [[B CsubB [cptB cB]]|]; last first.
+  move=> clC; exists (closure C) => //; first exact: subset_closure.
+  by split => //; exact: closed_closure.
+apply: (subclosed_compact _ cptB); first exact: closed_closure.
 by move/closure_id: cB => ->; exact: closure_subset.
 Qed.
 
 Lemma precompact_subset (A B : set X) : A `<=` B -> precompact B -> precompact A.
 Proof.
-by move=> AsubB [B' B'subB cptB']; exists B' => // ? ?; apply/B'subB/AsubB.
+by move=> AsubB [B' B'subB cptB']; exists B' => // ? ?; exact/B'subB/AsubB.
 Qed.
 
-Lemma compact_precompact (A B : set X) : 
+Lemma compact_precompact (A B : set X) :
   hausdorff_space X -> compact A -> precompact A.
 Proof.
-move=> h c; rewrite (@precompactE _) ( _ : closure A = A) //; symmetry. 
-by apply/closure_id; exact : (compact_closed h c).
+move=> h c; rewrite precompactE ( _ : closure A = A)//.
+apply/esym/closure_id; exact: compact_closed.
 Qed.
 
 Lemma precompact_closed (A : set X) : closed A -> precompact A = compact A.
 Proof.
-move=> clA; rewrite propeqE; split.
-  by move=> [B AsubB [ + _ ]] => /subclosed_compact; apply => //?.
-by rewrite {1}(_ : A = closure A) ?precompactE // -closure_id. 
+move=> clA; rewrite propeqE; split=> [[B AsubB [ + _ ]]|].
+  by move=> /subclosed_compact; exact.
+by rewrite {1}(_ : A = closure A) ?precompactE// -closure_id.
 Qed.
 
-Definition locally_compact (A : set X) := [locally precompact A]. 
+Definition locally_compact (A : set X) := [locally precompact A].
 
 End Precompact.
 
@@ -5235,8 +5233,8 @@ Lemma uniform_set1 F (f : U -> V) (x : U) :
 Proof.
 move=> FF; rewrite propeqE; split.
   move=> + W => /(_ [set t | W (t x)]) +; rewrite /filter_of -nbhs_entourageE.
-  rewrite /uniform_fun uniform_nbhs; move=> + [Q entQ subW].
-  by apply; exists Q; split => // h Qf; apply/subW/Qf.
+  rewrite /uniform_fun uniform_nbhs => + [Q entQ subW].
+  by apply; exists Q; split => // h Qf; exact/subW/Qf.
 move=> Ff W; rewrite /filter_of uniform_nbhs /uniform_fun => [[E] [entE subW]].
 apply: (filterS subW); move/(nbhs_entourage (f x))/Ff: entE => //=; near_simpl.
 by apply: filter_app; apply: nearW=> ? ? ? ->.
@@ -5254,8 +5252,7 @@ Lemma uniform_subset_cvg (f : U -> V) (A B : set U) F :
   Filter F -> B `<=` A -> {uniform A, F --> f} -> {uniform B, F --> f}.
 Proof.
 move => FF /uniform_subset_nbhs => /(_ f); rewrite /uniform_fun.
-move=> nbhsF Acvg; apply: cvg_trans; first exact: Acvg.
-exact: nbhsF.
+by move=> nbhsF Acvg; apply: cvg_trans; [exact: Acvg|exact: nbhsF].
 Qed.
 
 Lemma ptws_uniform_cvg  (f : U -> V) (F : set (set (U -> V))) :
@@ -5264,7 +5261,7 @@ Proof.
 move=> FF; rewrite cvg_sup => + i; have isubT : [set i] `<=` setT by move=> ?.
 move=> /(uniform_subset_cvg _ isubT); rewrite /ptws_fun uniform_set1.
 rewrite cvg_image; last by rewrite eqEsubset; split=> v // _; exists (cst v).
-apply: cvg_trans => W /=; rewrite nbhs_simpl; eexists; eauto.
+apply: cvg_trans => W /=; rewrite nbhs_simpl; exists (@^~ i @^-1` W) => //.
 by rewrite image_preimage // eqEsubset; split=> // j _; exists (fun _ => j).
 Qed.
 
@@ -5761,7 +5758,7 @@ Canonical subspace_pseudoMetricType :=
 
 End SubspacePseudoMetric.
 
-Definition singletons {X : Type} := [set [set x] | x in @setT X].
+Definition singletons {T : Type} := [set [set x] | x in @setT T].
 
 Section UniformPointwise.
 Context {U : topologicalType} {V : uniformType}.
@@ -5772,96 +5769,93 @@ Proof.
 move=> FF; rewrite propeqE fam_cvgP cvg_sup /ptws_fun; split.
   move=> + A [x _ <-] => /(_ x); rewrite uniform_set1.
   rewrite cvg_image; last by rewrite eqEsubset; split=> v // _; exists (cst v).
-  apply: cvg_trans => W /=; rewrite ?nbhs_simpl /fmap /= => [[W' + <-]]. 
-  by apply: filterS=> g W'g /=; eexists; eauto.
-move=> + i; (have Si : singletons [set i] by exists i) => /(_ [set i] Si).
-rewrite uniform_set1. 
+  apply: cvg_trans => W /=; rewrite ?nbhs_simpl /fmap /= => [[W' + <-]].
+  by apply: filterS => g W'g /=; exists g.
+move=> + i; have /[swap] /[apply] : singletons [set i] by exists i.
+rewrite uniform_set1.
 rewrite cvg_image; last by rewrite eqEsubset; split=> v // _; exists (cst v).
-move=> + W //=; rewrite ?nbhs_simpl => Q => /Q Q'; eexists; eauto.
-rewrite eqEsubset; split => j; first by case=> ? + <-.
-by move=> Wj; exists (fun _ => j).
+move=> + W //=; rewrite ?nbhs_simpl => Q => /Q Q'; exists (@^~ i @^-1` W) => //.
+by rewrite eqEsubset; split => [j [? + <-//]|j Wj]; exists (fun _ => j).
 Qed.
 
 Lemma ptws_cvg_compact_family F (f : U -> V):
   ProperFilter F -> {family compact, F --> f} -> {ptws, F --> f}.
 Proof.
 move=> PF; rewrite ptws_cvg_family_singleton; apply: family_cvg_subset.
-move=> A [x _ <-]; apply: compact_set1.
+by move=> A [x _ <-]; exact: compact_set1.
 Qed.
 End UniformPointwise.
 
-
 Section ArzelaAscoli.
 Context {X : topologicalType}.
 Context {Y : uniformType}.
 Context {hsdf : hausdorff_space Y}.
 
 (* The key condition in Arzela-Ascoli that, like uniform continuity,
-   moves a quantifier around so all functions have the same 'deltas' *)
+   moves a quantifier around so all functions have the same 'deltas'. *)
 
 Definition equicontinuous (W : set (X -> Y)) :=
-  forall x (E: set (Y * Y)), entourage E -> 
+  forall x (E : set (Y * Y)), entourage E ->
     \forall y \near x, forall f, W f -> E(f x, f y).
 
-Lemma equicontinuous_subset (W V : set (X -> Y)) : 
+Lemma equicontinuous_subset (W V : set (X -> Y)) :
   W `<=` V -> equicontinuous V -> equicontinuous W.
-Proof. 
-move=> WsubV + x E entE => /(_ x E entE); apply: filter_app; apply:nearW.
+Proof.
+move=> WsubV + x E entE => /(_ x E entE); apply: filter_app; apply: nearW.
 by move=> ? Vf ? /WsubV; exact: Vf.
 Qed.
 
-Lemma equicontinuous_cts (W : set (X -> Y)) f: 
+Lemma equicontinuous_cts (W : set (X -> Y)) f :
   equicontinuous W -> W f -> continuous f.
-Proof. 
-move=> ectsW Wf x; apply/cvg_entourageP => E entE; near_simpl; 
-by move: (ectsW x _ entE); apply: filter_app; apply: nearW=> ?; apply.
+Proof.
+move=> ectsW Wf x; apply/cvg_entourageP => E entE; near_simpl;
+by move: (ectsW x _ entE); apply: filter_app; apply: nearW => ?; exact.
 Qed.
 
-(* A convienet notion that is in between compactness in 
-   {family compact, X -> y} and compactness in {ptws X -> y}.*)
+(* A convenient notion that is in between compactness in
+   {family compact, X -> y} and compactness in {ptws X -> y}. *)
 Definition pointwise_precompact (W : set (X -> Y)):=
   forall x, precompact [set (f x) | f in W].
 
-Lemma pointwise_precomact_subset (W V : set (X -> Y)): 
+Lemma pointwise_precomact_subset (W V : set (X -> Y)) :
   W `<=` V -> pointwise_precompact V -> pointwise_precompact W.
-Proof. 
-move=> WsubV + x => /(_ x) pcptV. 
-by apply: precompact_subset; last exact: pcptV; exact: image_subset.
+Proof.
+move=> WsubV + x => /(_ x) pcptV.
+by apply: precompact_subset pcptV; exact: image_subset.
 Qed.
 
 Lemma pointwise_precompact_precompact (W : set {ptws X -> Y}):
   pointwise_precompact W -> precompact W.
 Proof.
-rewrite precompactE => ptwsPreW; set K := fun x => closure [set f x | f in W].
+rewrite precompactE => ptwsPreW; pose K := fun x => closure [set f x | f in W].
 set R := [set f : {ptws X -> Y} | forall x : X, K x (f x)].
-have C : compact R.  
-  by apply: tychonoff => x; rewrite -precompactE; apply: ptwsPreW.
+have C : compact R.
+  by apply: tychonoff => x; rewrite -precompactE; exact: ptwsPreW.
 apply: (subclosed_compact _ C); first exact: closed_closure.
 have WsubR : W `<=` R.
-  by move=> f Wf x; rewrite /R/K closure_limit_point; by left; exists f; tauto.
+  by move=> f Wf x; rewrite /R /K closure_limit_point; left; exists f.
 rewrite closureE => q; apply; split => //; apply: compact_closed=> //.
 exact: hausdorff_product.
 Qed.
 
-Lemma uniform_pointwise_compact (W : set (X -> Y)): 
-  compact (W : set (@fct_UniformFamily X Y compact)) -> 
+Lemma uniform_pointwise_compact (W : set (X -> Y)) :
+  compact (W : set (@fct_UniformFamily X Y compact)) ->
   compact (W : set {ptws X -> Y}).
 Proof.
-rewrite [x in x _ -> _]compact_ultra [x in _ -> x _]compact_ultra. 
+rewrite [x in x _ -> _]compact_ultra [x in _ -> x _]compact_ultra.
 move=> + F UF FW => /(_ F UF FW) [h [Wh Fh]]; exists h; split => //.
-by move=> /= Q Fq; apply: ptws_cvg_compact_family; first exact: Fh.
+by move=> /= Q Fq; apply: (ptws_cvg_compact_family _ Fh).
 Qed.
 
-Lemma compact_pointwise_precompact (W : set(X -> Y)): 
-  compact (W : set {family compact, X -> Y}) -> 
-  pointwise_precompact W.
+Lemma compact_pointwise_precompact (W : set (X -> Y)) :
+  compact (W : set {family compact, X -> Y}) -> pointwise_precompact W.
 Proof.
 move=> cptFamW x; pose V : set Y := prod_topo_apply x @` W.
-rewrite precompactE (_ : [set f x | f in W] = V ) //.
-suff: (compact V) by move=> /[dup]/(compact_closed hsdf)/closure_id <-.
-apply: (continuous_compact (f := prod_topo_apply x)); first move=> y ?.
-  by exact: prod_topo_apply_continuous.
+rewrite precompactE (_ : [set f x | f in W] = V) //.
+suff: compact V by move=> /[dup]/(compact_closed hsdf)/closure_id <-.
+apply: (@continuous_compact _ _ (prod_topo_apply x)).
+  by move=> y ?; exact: prod_topo_apply_continuous.
 exact: uniform_pointwise_compact.
 Qed.
 
-End ArzelaAscoli.
+End ArzelaAscoli.