doc, lint, compress

theories/topology.v

@@ -204,6 +204,9 @@ Require Import boolp reals classical_sets posnum.
 (*                          compact == set of compact sets w.r.t. the filter- *)
 (*                                     based definition of compactness.       *)
 (*                     hausdorff T <-> T is a Hausdorff space (T_2).          *)
+(*                evaluator_dep x f == application of f to x, f being a       *)
+(*                                     product topology of a family K         *)
+(*                                     (K : X -> topologicalType)             *)
 (*                    cover_compact == set of compact sets w.r.t. the open    *)
 (*                                     cover-based definition of compactness. *)
 (*                     connected A <-> the only non empty subset of A which   *)
@@ -2773,48 +2776,42 @@ Qed.
 End Tychonoff.
 
 Section DependentEvaluators.
-Context {X : choiceType} {K : forall x:X, topologicalType}.
-Definition evaluator_dep (x : X) (f : product_topologicalType K) := f x.
+Context {X : choiceType} {K : X -> topologicalType}.
+
+Definition evaluator_dep x (f : product_topologicalType K) := f x.
 
 Lemma evaluator_depE x f : evaluator_dep x f = f x.
 Proof. by []. Qed.
 
-Lemma evaluator_dep_continuous x: continuous (evaluator_dep x).
-Proof.
-move=> f; have /cvg_sup/(_ x)/cvg_image : (f --> f) by apply: cvg_id.
-pose xval (x : X) (y : K x) i : K i := 
-  match eqVneq x i return K i with 
-  | EqNotNeq r => @eq_rect X x K y i r
-  | NeqNotEq _ => point
-  end.
-set P := ( x in (x -> _) -> _); have P' : P. 
-  rewrite /P eqEsubset; split => y /=; first by [].
-  move=> _; exists (xval x y) => //; rewrite /xval.
-  case (eqVneq x x); last by move=>/eqP.
-  by move=> e; rewrite eq_axiomK.
-move/(_ P') => Ff; apply: cvg_trans; last exact: Ff.
-rewrite /= /evaluator_dep=> Q /=; rewrite {1}/nbhs /=.
-move=> [W nbdW <-]; rewrite /nbhs /=.
-by (apply: filterS; last exact: nbdW) => g Wg /=; exists g. 
-Qed.
-
-Lemma hausdorff_product : 
+Lemma evaluator_dep_continuous x : continuous (evaluator_dep x).
+Proof.
+move=> f; have /cvg_sup/(_ x)/cvg_image : f --> f by apply: cvg_id.
+move=> h; apply: (cvg_trans _ (h _)) => {h}; last first.
+  pose xval x (y : K x) i : K i :=
+    match eqVneq x i return K i with
+    | EqNotNeq r => @eq_rect X x K y i r
+    | NeqNotEq _ => point
+    end.
+  rewrite eqEsubset; split => y //= _; exists (xval x y) => //; rewrite /xval.
+  by case (eqVneq x x) => [e|/eqP//]; rewrite eq_axiomK.
+by move=> Q /= [W nbdW <-]; apply: filterS nbdW; exact: preimage_image.
+Qed.
+
+Lemma hausdorff_product :
   (forall x, hausdorff (K x)) -> hausdorff (@product_topologicalType X K).
 Proof.
-move=> hsdfV => p q /= clstr; apply: functional_extensionality_dep => x.
-apply: hsdfV; move: clstr; rewrite ?cluster_cvgE /= => [[G PG [GtoQ psubG]]].
-exists (evaluator_dep x @ G); first exact: fmap_proper_filter; split.
+move=> hsdfK p q /= clstr; apply: functional_extensionality_dep => x.
+apply: hsdfK; move: clstr; rewrite ?cluster_cvgE /= => -[G PG [GtoQ psubG]].
+exists (evaluator_dep x @ G); [exact: fmap_proper_filter|split].
   rewrite -(evaluator_depE x).
-  apply: cvg_trans; last apply: (@evaluator_dep_continuous x q).
-  by apply: cvg_app; exact GtoQ.
-move/(cvg_app (evaluator_dep x)):psubG => xpsubxG.
-apply: cvg_trans; first exact: xpsubxG.
-by apply: evaluator_dep_continuous.
+  apply: cvg_trans; last exact: (@evaluator_dep_continuous x q).
+  by apply: cvg_app; exact: GtoQ.
+move/(cvg_app (evaluator_dep x)): psubG => /cvg_trans; apply.
+exact: evaluator_dep_continuous.
 Qed.
 
 End DependentEvaluators.
 
-
 Definition finI (I : choiceType) T (D : set I) (f : I -> set T) :=
   forall D' : {fset I}, {subset D' <= D} ->
   \bigcap_(i in [set i | i \in D']) f i !=set0.