From 958cc305415f4f3cdc1a51421dcaca30b732458d Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 12 Nov 2021 17:15:45 -0500 Subject: [PATCH 1/3] linting pass fixing lines Update theories/topology.v using a better lemma to eliminate Eqdep_dec.eq_rect_eq_dec Co-authored-by: Cyril Cohen doc, lint, compress --- theories/topology.v | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/theories/topology.v b/theories/topology.v index c3d0a3ddc..87a2aac84 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -208,7 +208,14 @@ Require Import boolp reals classical_sets posnum. (* cluster F == set of cluster points of F. *) (* compact == set of compact sets w.r.t. the filter- *) (* based definition of compactness. *) +<<<<<<< HEAD (* hausdorff_space T <-> T is a Hausdorff space (T_2). *) +======= +(* 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) *) +>>>>>>> 83b8836... doc, lint, compress (* 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 *) @@ -2873,6 +2880,43 @@ Qed. End Tychonoff. +Section DependentEvaluators. +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. +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=> 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 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. From e3ffa87614f7f440320ffafe0b7adc28ea3b6cba Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 19 Jan 2022 19:38:05 -0500 Subject: [PATCH 2/3] renaming and making apply local --- theories/topology.v | 32 ++++++++++++++------------------ 1 file changed, 14 insertions(+), 18 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 87a2aac84..f352701b8 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -208,14 +208,7 @@ Require Import boolp reals classical_sets posnum. (* cluster F == set of cluster points of F. *) (* compact == set of compact sets w.r.t. the filter- *) (* based definition of compactness. *) -<<<<<<< HEAD (* hausdorff_space T <-> T is a Hausdorff space (T_2). *) -======= -(* 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) *) ->>>>>>> 83b8836... doc, lint, compress (* 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 *) @@ -2880,15 +2873,18 @@ Qed. End Tychonoff. -Section DependentEvaluators. +Section Product_Hausdorff. Context {X : choiceType} {K : X -> topologicalType}. -Definition evaluator_dep x (f : product_topologicalType K) := f x. +(* This a helper function to prove products preserve hausdorff. In particular *) +(* we use its continuity turn clustering in `product_topologicalType K` to *) +(* clustering in K x for each X. *) +Let prod_topo_apply x (f : product_topologicalType K) := f x. -Lemma evaluator_depE x f : evaluator_dep x f = f x. +Lemma prod_topo_applyE x f : prod_topo_apply x f = f x. Proof. by []. Qed. -Lemma evaluator_dep_continuous x : continuous (evaluator_dep x). +Lemma prod_topo_apply_continuous x : continuous (prod_topo_apply 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. @@ -2903,19 +2899,19 @@ 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). + (forall x, hausdorff_space (K x)) -> hausdorff_space (@product_topologicalType X K). Proof. 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 exact: (@evaluator_dep_continuous x q). +exists (prod_topo_apply x @ G); [exact: fmap_proper_filter|split]. + rewrite -(prod_topo_applyE x). + apply: cvg_trans; last exact: (@prod_topo_apply_continuous x q). by apply: cvg_app; exact: GtoQ. -move/(cvg_app (evaluator_dep x)): psubG => /cvg_trans; apply. -exact: evaluator_dep_continuous. +move/(cvg_app (prod_topo_apply x)): psubG => /cvg_trans; apply. +exact: prod_topo_apply_continuous. Qed. -End DependentEvaluators. +End Product_Hausdorff. Definition finI (I : choiceType) T (D : set I) (f : I -> set T) := forall D' : {fset I}, {subset D' <= D} -> From 2a20c4c703ac3c949e389af4aefae4f5505ae1a6 Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 19 Jan 2022 19:46:00 -0500 Subject: [PATCH 3/3] restoring docs --- theories/topology.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/theories/topology.v b/theories/topology.v index f352701b8..7afaf1c82 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -209,6 +209,9 @@ Require Import boolp reals classical_sets posnum. (* compact == set of compact sets w.r.t. the filter- *) (* based definition of compactness. *) (* hausdorff_space T <-> T is a Hausdorff space (T_2). *) +(* prod_topo_apply x f == application of f to x, f being in 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 *) @@ -2879,7 +2882,7 @@ Context {X : choiceType} {K : X -> topologicalType}. (* This a helper function to prove products preserve hausdorff. In particular *) (* we use its continuity turn clustering in `product_topologicalType K` to *) (* clustering in K x for each X. *) -Let prod_topo_apply x (f : product_topologicalType K) := f x. +Definition prod_topo_apply x (f : product_topologicalType K) := f x. Lemma prod_topo_applyE x f : prod_topo_apply x f = f x. Proof. by []. Qed.